Sobre o projeto

A Formalização AIQ DKPS contém formalizações em Lean 4 para embeddings baseados em resposta de modelos generativos de caixa-preta, centradas no data kernel perspective space (DKPS) e na infraestrutura de multidimensional-scaling / spectral-perturbation. A biblioteca de produto principal é a ForTauCeti, acompanhada por pacotes de formalização dedicados, como DavisKahan, YuWangSamworth2015, RoadmapBridge, Acharyya2024, Acharyya2025, DkpsQuench2026 e Helm2025. Essas bibliotecas formalizam a teoria de operadores, multidimensional scaling de raw-stress, double-centering de MDS clássico, perturbação espectral, bookkeeping de alinhamento ortogonal, ideais de operadores, concentração de média amostral, propagação de eventos de alta probabilidade e transferência de consistência.