minimum_rest_mass_is_gap
plain-language theorem explainer
The minimum rest mass equals the Yang-Mills mass gap Δ = J(φ) = (√5 − 2)/2 > 0. Unification and mass-gap researchers cite this equality to close the rest-mass identification. The proof is a one-line term pairing a positivity witness with reflexivity.
Claim. $0 < m_0$ and $m_0 = J(φ) = (√5 − 2)/2$, where $J(x) = (x + x^{-1})/2 − 1$ is the Recognition cost function and $φ$ is the self-similar fixed point.
background
The module derives 4D Lorentzian geometry from the J-cost functional and the T0–T8 forcing chain. J satisfies the Recognition Composition Law and is unique by T5; φ is forced as the fixed point by T6. massGap is the minimum rest mass, identified with the Yang-Mills gap Δ = J(φ) in the imported YangMillsMassGap structure. Upstream results supply the J-cost structure (PhiForcingDerived.of), the ledger factorization (DAlembert.LedgerFactorization.of), and the spectral emergence that fixes gauge content and generations (SpectralEmergence.of).
proof idea
The proof is the term ⟨massGap_pos, rfl⟩. It applies the positivity lemma massGap_pos together with reflexivity to discharge the conjunction.
why it matters
The declaration supplies the explicit numerical value of the minimum rest mass inside the spacetime-emergence registry (SE-001 to SE-010). It links the J-cost minimum directly to the Yang-Mills gap, completing the mass identification required by the T5–T6 steps of the forcing chain. No downstream uses are recorded; the result stands as a terminal equality in the unification layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.