excited_jcost
plain-language theorem explainer
The theorem asserts that J-cost is strictly positive for every positive real r not equal to 1. Modelers of the Recognition Hamiltonian spectrum cite it to separate the vacuum (J = 0) from all excited sectors. The proof is a direct term application of the core positivity lemma for Jcost.
Claim. For every real number $r > 0$ with $r ≠ 1$, the J-cost satisfies $J(r) > 0$.
background
The module defines the spectrum of the Recognition Hamiltonian Ĥ_RS. Ground state corresponds to J = 0 at r = 1; all other sectors are excited with J > 0. The spectral gap on a discretized lattice is the infimum of J(r) over r > 0, r ≠ 1, which is positive once lattice spacing is imposed. J-cost is the function that quantifies deviation from the vacuum fixed point, introduced via the Recognition Composition Law and the forcing chain T5–T8. The upstream lemma Jcost_pos_of_ne_one states that J(x) > 0 for x ≠ 1 and x > 0, proved by rewriting Jcost as a square divided by a positive term.
proof idea
One-line term proof that applies the lemma Jcost_pos_of_ne_one directly to the hypotheses hr and hne.
why it matters
The result supplies the excited field inside the HamiltonianSpectrumCert definition, which certifies the five-sector decomposition (vacuum plus four excited sectors) required by configDim D = 5. It closes the structural claim that the lattice spectrum has a positive gap, consistent with the Recognition Science treatment of the Yang-Mills mass gap. The parent certificate is the only downstream use; no open scaffolding remains for this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.