GaugeSectorMassGap
plain-language theorem explainer
GaugeSectorMassGap is a structure that holds the three real-valued mass gaps for the SU(3) color, SU(2) weak, and U(1) hypercharge sectors. A researcher comparing Recognition Science predictions to lattice gauge data would cite it when stating the sector-resolved gaps. It is introduced as a plain structure definition with no computational body.
Claim. A record with fields color_gap : ℝ (SU(3) glueball gap), weak_gap : ℝ (SU(2) W/Z gap), and hyper_gap : ℝ (U(1) photon gap).
background
The module treats the Yang-Mills mass gap as emerging from the J-cost functional J(x) = ½(x + x⁻¹) − 1 on the golden-ratio lattice. The central claim is that the minimum non-vacuum excitation costs exactly Δ = J(φ) = (√5 − 2)/2 > 0, which is universal across gauge sectors on the Q₃ lattice. Upstream, RSNativeUnits.U fixes c = 1 and the native scale, while Gap45.Derivation.gap supplies the integer gap factor used in mass anchoring.
proof idea
This is a structure definition that declares the three real fields. No lemmas or tactics are applied; the definition serves only as a typed container.
why it matters
The structure feeds directly into RS_gauge_mass_gaps, which populates the non-abelian fields with massGap and sets the abelian field to zero. It realizes the module's central theorem that the J-cost spectral gap on the phi-ladder resolves the Millennium problem for all three sectors. It rests on T5 J-uniqueness and T6 phi fixed point from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.