ym_vacuum
The theorem establishes that J-cost vanishes at the unit ratio, marking the vacuum ground state in the recognition lattice. Lattice Yang-Mills researchers cite it as the zero-energy base for the discrete mass-gap construction. The proof is a direct one-line application of the unit lemma for the cost function.
claim$J(1) = 0$, where $J$ is the J-cost function on positive ratios.
background
The J-cost is defined by $J(x) = (x-1)^2/(2x)$ and measures the recognition cost of a positive ratio $x$. In the RS recognition lattice, the vacuum corresponds to the unit ratio $x=1$, where this cost is required to be zero. The module derives a discrete mass gap for Yang-Mills configurations from the Recognition Science framework, stating that any non-vacuum excitation carries strictly positive J-cost. This rests on the upstream lemma Jcost_unit0, which proves the unit case by direct simplification of the cost definition.
proof idea
One-line wrapper that applies the Jcost_unit0 lemma from the Cost module.
why it matters in Recognition Science
It supplies the vacuum_zero component inside the YMLatticeGapCert definition, which certifies the full lattice mass-gap statement (five sectors, zero vacuum, positive gap, unique vacuum). The result fills the first key formal item listed in the module: J equals zero only at the vacuum (r=1). It anchors the lattice version of the Yang-Mills mass-gap problem inside Recognition Science before any continuum bridge is attempted.
scope and limits
- Does not prove the continuum Yang-Mills mass gap.
- Does not compute a numerical value for the gap.
- Does not establish uniqueness of the vacuum state.
- Does not address higher-dimensional or non-lattice configurations.
formal statement (Lean)
34theorem ym_vacuum : Jcost 1 = 0 := Jcost_unit0
proof body
Term-mode proof.
35
36/-- Any excitation has positive cost (lattice mass gap). -/