aiq-dkps-formalization

AIQ DKPS Formalization contains Lean 4 formalizations for response-based embeddings of black-box generative models, centered on the data kernel perspective space (DKPS) and the multidimensional-scaling / spectral-perturbation infrastructure. The core product library is ForTauCeti, accompanied by dedicated formalization packages such as DavisKahan, YuWangSamworth2015, RoadmapBridge, Acharyya2024, Acharyya2025, DkpsQuench2026, and Helm2025. These libraries formalize operator theory, raw-stress multidimensional scaling, classical MDS double-centering, spectral perturbation, orthogonal-alignment bookkeeping, operator ideals, sample-mean concentration, high-probability event propagation, and consistency transfer.