A Lean 4 Proof Architecture for a Normalized 4D Mass Gap Theorem Phase 3 Spectral Gap Formalization and External-Audit Boundary
Fuente:
Zenodo
Saved in:
| Main Author: | |
|---|---|
| Format: | Recurso digital |
| Language: | English |
| Published: |
Zenodo
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866901786218987520 |
|---|---|
| author | Itakura, Hidetoshi |
| author_facet | Itakura, Hidetoshi |
| contents | <p>This record provides a technical preprint describing the MGAP4D Lean 4 proof architecture for a normalized four-dimensional mass gap theorem. It accompanies the public GitHub repository itakura-hidetoshi/4d-mass-gap.</p> <p>The repository is organized as a GitHub-native Lean project with MGAP4D.lean as the active root. The current main branch has reached a Phase 3 spectral gap formalization CI-green checkpoint through the global Phase3ReleaseGate root. The current Lean surfaces include the spectral module entrypoint, structural spectral gap formalization checkpoint, spectral gap formalization gate, and global Phase 3 release/replay/source-tree/external-audit gate.</p> <p>The formalized normalized value surface currently records:</p> <p>normalizedGapValue.value = 33 / 20</p> <p>This release should be read as a proof-architecture and external-audit preparation paper, not as a final externally certified theorem release. The repository preserves this boundary: R1--R7 theorem completions are not claimed, final theorem release is not unlocked, Mathlib adoption on the main branch remains on hold, and the public theorem boundary remains review-gated pending independent replay and external audit.</p> <p>The purpose of this record is to provide a citable, DOI-backed snapshot of the proof architecture, CI status, theorem-surface organization, replay protocol, and external-audit boundary.</p> |
| format | Recurso digital |
| id | zenodo_https___doi_org_10_5281_zenodo_20181046 |
| institution | Zenodo |
| language | eng |
| publishDate | 2026 |
| publisher | Zenodo |
| record_format | zenodo |
| spellingShingle | A Lean 4 Proof Architecture for a Normalized 4D Mass Gap Theorem Phase 3 Spectral Gap Formalization and External-Audit Boundary Itakura, Hidetoshi 4D mass gap Yang–Mills Lean 4 formal verification spectral gap machine-checked mathematics proof architecture normalized mass gap external audit MGAP4D <p>This record provides a technical preprint describing the MGAP4D Lean 4 proof architecture for a normalized four-dimensional mass gap theorem. It accompanies the public GitHub repository itakura-hidetoshi/4d-mass-gap.</p> <p>The repository is organized as a GitHub-native Lean project with MGAP4D.lean as the active root. The current main branch has reached a Phase 3 spectral gap formalization CI-green checkpoint through the global Phase3ReleaseGate root. The current Lean surfaces include the spectral module entrypoint, structural spectral gap formalization checkpoint, spectral gap formalization gate, and global Phase 3 release/replay/source-tree/external-audit gate.</p> <p>The formalized normalized value surface currently records:</p> <p>normalizedGapValue.value = 33 / 20</p> <p>This release should be read as a proof-architecture and external-audit preparation paper, not as a final externally certified theorem release. The repository preserves this boundary: R1--R7 theorem completions are not claimed, final theorem release is not unlocked, Mathlib adoption on the main branch remains on hold, and the public theorem boundary remains review-gated pending independent replay and external audit.</p> <p>The purpose of this record is to provide a citable, DOI-backed snapshot of the proof architecture, CI status, theorem-surface organization, replay protocol, and external-audit boundary.</p> |
| title | A Lean 4 Proof Architecture for a Normalized 4D Mass Gap Theorem Phase 3 Spectral Gap Formalization and External-Audit Boundary |
| topic | 4D mass gap Yang–Mills Lean 4 formal verification spectral gap machine-checked mathematics proof architecture normalized mass gap external audit MGAP4D |
| url | https://doi.org/10.5281/zenodo.20181046 |