vacuum_jcost
plain-language theorem explainer
Vacuum sector of the Recognition Hamiltonian has J-cost zero. Mass-gap derivations cite this to fix the ground-state energy in the spectrum. Proof is a direct one-line application of the Jcost unit lemma.
Claim. $J(1) = 0$, where $J(x) = (x-1)^2 / (2x)$.
background
The Recognition Hamiltonian Spectrum module treats the spectrum of Ĥ_RS on H_RS. Ground state is the vacuum with J = 0; excited states satisfy J > 0. The J-cost function is defined in the Cost module. Upstream lemma Jcost_unit0 states: J(x) expressed as a squared ratio: J(x) = (x-1)²/(2x). It proves the value at unity by simplification.
proof idea
One-line wrapper that applies the lemma Jcost_unit0 from the Cost module.
why it matters
Supplies the vacuum field to hamiltonianSpectrumCert, which assembles the five-sector certification. It anchors the ground state in the Recognition framework, consistent with J-uniqueness from the forcing chain. The result closes the vacuum sector; the lattice gap witness remains open for the discrete case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.