A Lean 4 Proof Architecture for a Normalized 4D Mass Gap Theorem Phase 3 Spectral Gap Formalization and External-Audit Boundary

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. 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. The formalized normalized value surface currently records: normalizedGapValue.value = 33 / 20 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. 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.