aiq-dkps-formalization

AIQ DKPS Formalizationは、データカーネル視点空間（DKPS）および多次元尺度構成法（MDS）/スペクトル摂動インフラを中心とした、ブラックボックス生成モデルの応答ベース埋め込みに関するLean 4形式化を提供します。コア製品ライブラリはForTauCetiであり、DavisKahan、YuWangSamworth2015、RoadmapBridge、Acharyya2024、Acharyya2025、DkpsQuench2026、Helm2025などの専用形式化パッケージが付属しています。これらのライブラリは、作用素論、raw-stress多次元尺度構成法、古典的MDSのダブルセンタリング、スペクトル摂動、直交アライメントの記帳処理、作用素イデアル、標本平均の集中、高確率イベントの伝播、および一貫性の転送を形式化しています。