module module moderate

`IndisputableMonolith.Unification.YangMillsMassGap`

Identifies the Yang–Mills mass gap with the J-cost of the golden ratio, Δ = J(φ) = φ − 1/2, and records the elementary φ-identities and positivity facts that make that identification usable. Unification and gauge-sector work cites it for a concrete positive lower bound on glueball mass in RS units. The module is mostly exact algebraic identities plus monotonicity of J on (1,∞).

claimSet $\varphi=(1+\sqrt{5})/2$ and $J(x)=(x+x^{-1})/2-1$. Define the RS mass gap by $\Delta:=J(\varphi)$. The module proves $\varphi^{-1}=\varphi-1$, $J(\varphi)=\varphi-1/2=\Delta>0$, monotonicity of $J$ on $(1,\infty)$, and introduces the $\varphi$-ladder $n\mapsto\varphi^n$ as the discrete mass scale.

background

Recognition Science forces the cost functional $J(x)=(x+x^{-1})/2-1$ (T5) and the self-similar fixed point $\varphi$ of the discrete ledger (T6, PhiForcing). In RS-native units the same $J$ supplies dimensionless energy defects; a strictly positive lower bound on non-abelian flux energy is therefore a candidate mass gap.

Upstream, DimensionForcing fixes $D=3$, GaugeFromCube extracts $\mathrm{SU}(3)\times\mathrm{SU}(2)\times\mathrm{U}(1)$ from the 3-cube, and WindingCharges / ParticleGenerations supply the charge and generation structure that sit on the same ledger. Cost and Constants give the native $J$ and the tick $\tau_0$.

This module packages the elementary $\varphi$–$J$ calculus needed to name that lower bound: the inverse identity $\varphi^{-1}=\varphi-1$, the exact evaluation $J(\varphi)=\varphi-1/2$, and the positive $\varphi$-ladder used later as a mass yardstick.

proof idea

Algebraic core, not a long derivation. From $\varphi^2=\varphi+1$ one gets $\varphi(\varphi-1)=1$, hence $\varphi^{-1}=\varphi-1$ and $\varphi+\varphi^{-1}=\sqrt{5}$ (or $2\varphi-1$). Substituting into $J$ yields $J(\varphi)=\varphi-1/2$ exactly; that common value is defined as $\mathrm{massGap}$. Positivity is $\sqrt{5}>2$ (or $\varphi>1$) plus $J>0$ on $(1,\infty)$. Monotonicity of $J$ above 1 is the standard derivative/ordering fact for the cost. The $\varphi$-ladder is the geometric sequence $\varphi^n$ with a one-line positivity proof. No analytic continuum limit or lattice YM estimate appears here.

why it matters in Recognition Science

Gives Unification a named, strictly positive scalar $\Delta=J(\varphi)$ that can stand in for the Yang–Mills mass gap inside RS, tied directly to T5–T6 rather than to a separate non-perturbative postulate. Downstream, SpacetimeEmergence imports the module while forcing 4D Lorentzian geometry from $J$-cost (registry SE-001–SE-010); a positive gap is part of the rigid energetic structure that spacetime and gauge sectors must accommodate. The $\varphi$-ladder also aligns with the global mass formula (yardstick $\times\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$) and with the Berry threshold $\varphi^{-1}$. The module does not claim a Clay-problem solution in continuum QFT; it supplies the RS-native gap constant those later theorems quote.

scope and limits

Does not prove the Clay Yang–Mills mass gap in continuum QFT or constructive field theory.
Does not derive a lattice or continuum glueball spectrum; only the RS scalar Δ = J(φ).
Does not treat running couplings, confinement proofs, or non-perturbative path integrals.
Does not force D = 3 or the SM gauge group; those live in DimensionForcing and GaugeFromCube.
Does not establish the full particle mass ladder numerics beyond the φ-scale definition.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Unification.SpacetimeEmergence module_import

depends on (7)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import
IndisputableMonolith.Foundation.DimensionForcing module_import
IndisputableMonolith.Foundation.GaugeFromCube module_import
IndisputableMonolith.Foundation.ParticleGenerations module_import
IndisputableMonolith.Foundation.PhiForcing module_import
IndisputableMonolith.Foundation.WindingCharges module_import

declarations in this module (48)

theorem phi_inv_eq L79
theorem phi_plus_inv L87
theorem Jcost_phi_exact L93
theorem Jcost_phi_eq_phi_minus_half L99
def massGap L105
theorem Jcost_phi_eq_massGap L108
lemma sqrt5_gt_two L113
theorem massGap_pos L120
theorem Jcost_phi_pos L124
theorem Jcost_mono_gt_one L132
def PhiLadder L150
theorem phiLadder_pos L153
theorem Jcost_phiLadder_zero L157
theorem Jcost_phiLadder_symm L161
theorem phiLadder_ge_phi L167
theorem phiLadder_gt_one L174
theorem spectral_gap_pos_rung L178
theorem spectral_gap L184
theorem spectral_gap_strict L194
structure GaugeBondConfig L202
def vacuum L206
def totalGaugeCost L210
lemma bond_cost_nonneg L214
lemma bond_le_total L219
theorem vacuum_cost_zero L225
def isNonTrivial L229
theorem gauge_mass_gap L234
theorem gauge_cost_ge_gap L240
theorem vacuum_unique_zero_cost L246
def IsContractible L257
theorem contractible_bond_zero_cost L260
theorem noncontractible_bond_gapped L265
theorem gap_separates_sectors L269
theorem gap_topologically_protected L278
theorem gap_rigidity L285
structure GaugeSectorMassGap L301
def RS_gauge_mass_gaps L307
theorem U1_gapless L313
theorem SU2_SU3_gapped L316
theorem mass_gap_asymmetry L321
theorem massGap_numerical_bound L330
def massGap_falsifier L347
theorem massGap_unfalsified L351
structure YMGapCertificate L367
theorem yang_mills_gap_cert L382
theorem yang_mills_gap_cert_nonempty L393
theorem mass_gap_from_forcing_chain L402
theorem yang_mills_mass_gap_complete L417