pith. machine review for the scientific record. sign in
theorem proved term proof high

minimum_rest_mass_is_gap

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 308theorem minimum_rest_mass_is_gap :
 309    0 < massGap ∧ massGap = (Real.sqrt 5 - 2) / 2 :=

proof body

Term-mode proof.

 310  ⟨massGap_pos, rfl⟩
 311
 312/-! ## §9  The Arrow of Time from the Octave -/
 313
 314/-- **SE-009: The arrow of time**. Recognition advances monotonically. -/

depends on (10)

Lean names referenced from this declaration's body.