aiq-dkps-formalization

AIQ DKPS Formalization 包含用于黑盒生成模型响应式嵌入的 Lean 4 形式化工作，核心围绕数据核透视空间（DKPS）以及多维缩放（MDS）和谱摄动基础设施。核心产品库为 ForTauCeti，并辅以多个专用的形式化程序包，包括 DavisKahan、YuWangSamworth2015、RoadmapBridge、Acharyya2024、Acharyya2025、DkpsQuench2026 和 Helm2025。这些库对算子理论、原始应力多维缩放、经典 MDS 双中心化、谱摄动、正交对齐簿记、算子理想、样本均值浓度、高概率事件传播以及一致性传递进行了形式化。