gauge_mass_gap
plain-language theorem explainer
Gauge mass gap theorem states that any non-trivial gauge bond configuration on the twelve edges of Q3 carries strictly positive total J-cost. Researchers addressing the Yang-Mills mass gap would cite it as the Recognition Science resolution of Millennium Problem QG-005. The proof is a term-mode extraction of a non-zero rung witness followed by the strict spectral gap inequality composed with the single-bond-to-total cost bound.
Claim. Let $cfg$ assign an integer rung index to each of the twelve edges of the cube $Q_3$. If at least one rung differs from zero, then the total recognition cost satisfies $0 < totalGaugeCost(cfg)$, where $totalGaugeCost(cfg) = sum_e J(phi^{r_e})$ and $J(x) = 1/2(x + x^{-1}) - 1$.
background
The module derives the Yang-Mills mass gap from the J-cost functional on the golden-ratio lattice. GaugeBondConfig is the structure that assigns to each of the twelve edges of Q3 an integer rung index, with the vacuum defined by all rungs at zero. isNonTrivial asserts that at least one rung is nonzero. totalGaugeCost sums the individual bond costs J(PhiLadder(r_e)). The module states that the gap Delta equals J(phi) = (sqrt(5)-2)/2 and separates vacuum from every non-trivial excitation.
proof idea
The term proof destructures the non-triviality witness h to obtain an edge e with nonzero rung. It applies the strict spectral gap lemma to the bond at e, then composes with the upstream bond_le_total lemma (a single bond cost is at most the total) to conclude strict positivity of totalGaugeCost.
why it matters
This is the central quantitative lower bound for the RS resolution of the Yang-Mills mass gap (registry QG-005). It rests on the phi-forcing chain (T5 J-uniqueness and T6 self-similar fixed point) together with the Recognition Composition Law. The module doc describes the result as exact, universal across SU(3), SU(2), U(1) sectors on Q3, topological, and falsifiable by any sub-Delta excitation. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.