aiq-dkps-formalization

AIQ DKPS Formalization contiene formalizaciones en Lean 4 para incrustaciones basadas en respuestas de modelos generativos de caja negra, centradas en el data kernel perspective space (DKPS) y la infraestructura de multidimensional-scaling / spectral-perturbation. La biblioteca de productos principal es ForTauCeti, acompañada de paquetes de formalización dedicados como DavisKahan, YuWangSamworth2015, RoadmapBridge, Acharyya2024, Acharyya2025, DkpsQuench2026 y Helm2025. Estas bibliotecas formalizan la teoría de operadores, el escalado multidimensional de estrés bruto, el doble centrado de MDS clásico, la perturbación espectral, el registro de alineación ortogonal, los ideales de operadores, la concentración de la media muestral, la propagación de eventos de alta probabilidad y la transferencia de consistencia.