Guardat en:
| Autor principal: | |
|---|---|
| Format: | Recurso digital |
| Idioma: | anglès |
| Publicat: |
Zenodo
2026
|
| Matèries: | |
| Accés en línia: | https://doi.org/10.5281/zenodo.20181046 |
| Etiquetes: |
Afegir etiqueta
Sense etiquetes, Sigues el primer a etiquetar aquest registre!
|
Taula de continguts:
- <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>