aiq-dkps-formalization

AIQ DKPS Formalization contient des formalisations Lean 4 pour les plongements basés sur les réponses de modèles génératifs boîte noire, centrées sur le data kernel perspective space (DKPS) et l'infrastructure de mise à l'échelle multidimensionnelle / perturbation spectrale. La bibliothèque produit principale est ForTauCeti, accompagnée de packages de formalisation dédiés tels que DavisKahan, YuWangSamworth2015, RoadmapBridge, Acharyya2024, Acharyya2025, DkpsQuench2026 et Helm2025. Ces bibliothèques formalisent la théorie des opérateurs, la mise à l'échelle multidimensionnelle raw-stress, le double centrage MDS classique, la perturbation spectrale, la tenue de livres de l'alignement orthogonal, les idéaux d'opérateurs, la concentration de la moyenne échantillonnée, la propagation d'événements à haute probabilité et le transfert de cohérence.