ym_lattice_gap
plain-language theorem explainer
The theorem establishes that any non-vacuum configuration on the recognition lattice carries strictly positive J-cost, providing the lattice-level mass gap for Yang-Mills theory. Physicists working on the mass gap problem would cite this result as the discrete precursor to the continuum statement. The proof is a direct one-line application of the positivity lemma for the J-cost function away from unity.
Claim. For every real number $r > 0$ with $r ≠ 1$, the J-cost satisfies $Jcost(r) > 0$.
background
Jcost is the recognition cost function on positive reals, vanishing only at the vacuum point r = 1. The module sets up a discrete lattice version of Yang-Mills theory in which any non-trivial field configuration is an excitation above this vacuum. Upstream lemmas establish that Jcost rewrites as a square divided by a positive denominator, hence is positive whenever the argument differs from 1.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_pos_of_ne_one from the Cost module, which establishes positivity of Jcost for positive reals not equal to one by rewriting to a square and using positivity of squares.
why it matters
This result supplies the gap_exists field in the YMLatticeGapCert certificate, confirming the lattice mass gap for the five canonical YM sectors. It realizes the discrete version of the Yang-Mills mass gap problem within Recognition Science, where the vacuum is the unique zero-cost state at r=1. The continuum limit remains open, requiring the S1 bridge program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.