theorem proved term proof

`minimum_rest_mass_is_gap`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

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.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
Time in IndisputableMonolith.Constants.RSNativeUnits decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
Octave in IndisputableMonolith.RRF.Core.Octave decl_use
massGap in IndisputableMonolith.Unification.YangMillsMassGap decl_use
massGap_pos in IndisputableMonolith.Unification.YangMillsMassGap decl_use