UGP-Lean: 보편적 생성 원리의 기계 검증

보편적 생성 원리(UGP)는 정수 능선 R_n = 2^n - 16에 정의된 결정론적 산술 프레임워크로, 초기 원리로부터 자유 매개변수 없이 고유한 정식 시드 (1,73,823)를 생성하며, 이는 생성 삼중 진화(GTE) 맵에 의해 엄격하게 결정됩니다. 본 연구는 UGP/GTE 프레임워크의 기계 검증된 Lean 4 형식화인 ugp-lean을 제시합니다. ugp-lean은 400개 이상의 모듈로 구성되어 있으며, 모든 증명에서 'sorry' 키워드가 사용되지 않았습니다. 특히, 레지스터 머신(Minsky 1967 2-카운터 머신) 시뮬레이션을 통해 진정한 튜링 완전성 경로를 확립하고 기계적으로 인증했습니다. 기존의 불완전한 증명 스텁과 부적절한 대수적 완전성 경로는 제거하고 수정했습니다. 라이브러리 전반에 걸쳐 17개의 모호하거나 동어반복적인 증명을 수정하거나 재조정했습니다. 98개의 명명된 공리 목록을 재현 가능한 방법론으로 감사했으며, 오래된 정리 이름을 수정했습니다. 현재 버전은 435개의 Lean 파일, 98개의 명명된 공리, 그리고 propext/Classical.choice/Quot.sound 외의 표준 Lean/Mathlib 논리 공리를 사용하지 않습니다. 모든 핵심 대수적 고유성, 구조적 풍부성, 계산적 보편성 결과는 기계적으로 완전히 인증되었습니다. 나머지 미해결 형식화 작업(GH 수렴, 얽힘 면적 법칙, Page-Wootters Born 브리지 등)은 논문과 저장소에 명시적으로 미해결로 표시되어 있습니다.