mass_gap_is_spatial_minimum
plain-language theorem explainer
The theorem states that the mass gap is bounded above by the J-cost at every nonzero position on the phi-ladder. Workers deriving spatial minima from recognition cost in unification models would cite the bound when linking mass gap to J-cost minimization. The proof is a direct term application of the spectral gap lemma.
Claim. For every integer $n$ with $n ≠ 0$, the mass gap satisfies massGap ≤ Jcost(φ^n), where φ^n runs over the nonzero rungs of the phi-ladder and Jcost is the recognition cost functional.
background
The Spacetime Emergence module derives 4D Lorentzian geometry from the J-cost functional and the T0–T8 forcing chain. J-cost is defined via the Recognition Composition Law as J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y), with J(x) = (x + x^{-1})/2 − 1. The phi-ladder collects all stable positions as φ^n for integer n, per the PhiEmergence definition. The mass gap is the minimum spatial excitation energy, as noted in the declaration comment. Upstream results supply the gap as the product of closure and Fibonacci factors and the anchor policy that maps charges to ladder rungs.
proof idea
Term-mode proof that applies the spectral_gap lemma in one step to obtain the inequality for all nonzero integer rungs.
why it matters
The result supplies the spatial minimum required by the spacetime emergence derivation, confirming that the mass gap equals the J-cost floor on the phi-ladder. It advances the module's central claim that the Lorentzian metric signature (−,+,+,+) is forced by J-cost minimization together with T7 (eight-tick octave) and T8 (D = 3). No downstream theorems are recorded, leaving open its integration into the full Yang-Mills mass gap construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.