프로젝트 소개

AIQ DKPS Formalization은 데이터 커널 관점 공간(DKPS) 및 다차원 척도법(multidimensional-scaling) / 스펙트럼 섭동(spectral-perturbation) 인프라를 중심으로 한 블랙박스 생성 모델의 응답 기반 임베딩에 대한 Lean 4 형식화를 포함합니다. 핵심 제품 라이브러리는 ForTauCeti이며, DavisKahan, YuWangSamworth2015, RoadmapBridge, Acharyya2024, Acharyya2025, DkpsQuench2026, Helm2025와 같은 전용 형식화 패키지가 수반됩니다. 이러한 라이브러리들은 연산자 이론, raw-stress 다차원 척도법, 고전적 MDS 이중 중심화, 스펙트럼 섭동, 직교 정렬 장부 기록, 연산자 이데알, 표본 평균 집중, 고확률 사건 전파 및 일관성 전이를 형식화합니다.