minimum_rest_mass_is_gap
plain-language theorem explainer
The minimum rest mass equals the Yang-Mills mass gap Δ = J(φ) and equals (√5 − 2)/2 while remaining strictly positive. Researchers linking Recognition Science to the QCD mass gap would cite this identification. The proof is a one-line term that pairs the established positivity of the gap with reflexivity on the closed-form expression.
Claim. The minimum rest mass satisfies $0 < Δ$ and $Δ = (√5 − 2)/2$, where $Δ = J(φ)$ is the Yang-Mills mass gap and $φ$ is the golden-ratio fixed point of the J-cost functional.
background
The Spacetime Emergence module derives four-dimensional Lorentzian geometry from the J-cost functional and the T0–T8 forcing chain. J(x) = (x + x^{-1})/2 − 1 fixes spatial curvature via J''(1) = 1 and selects the eight-tick temporal direction via the octave operator. Upstream results supply the J-cost structure (PhiForcingDerived.of), the ledger factorization (DAlembert.LedgerFactorization.of), and the spectral emergence of gauge content (SpectralEmergence.of).
proof idea
The proof is a one-line term that applies the positivity lemma massGap_pos together with reflexivity on the algebraic identity for J(φ).
why it matters
This theorem identifies the minimum rest mass with the Yang-Mills mass gap Δ = J(φ), closing the link between the phi-ladder mass formula and the QCD gap inside the spacetime-emergence chain (SE-001 to SE-010). It rests on T5 (J-uniqueness) and T6 (phi fixed point) and supports the later arrow-of-time section. The result supplies the mass scale that enters the Lorentzian metric and proper-time definitions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.