latticeSpacingGap
plain-language theorem explainer
latticeSpacingGap defines the property that a positive spectral gap Δ exists below the J-cost evaluated at the shifted point 1+a whenever the lattice spacing a is positive. Physicists studying discretized QFT models or the mass gap in Recognition Science would cite this structural predicate when certifying spectra. The definition is realized directly as an existential statement whose witness is supplied separately by positivity of Jcost away from unity.
Claim. For any real $a > 0$, the lattice spacing gap property asserts that there exists a real number $Δ > 0$ satisfying $Δ < J(1 + a)$, where $J$ is the J-cost function with $J(1) = 0$ and $J(r) > 0$ for $r ≠ 1$.
background
The Recognition Hamiltonian Spectrum module treats the Recognition Hamiltonian Ĥ_RS whose spectrum consists of a vacuum ground state at J = 0 and excited states with J > 0. The continuous spectral gap Δ_RS is defined as the infimum of J(r) over r > 0, r ≠ 1, but this infimum vanishes; discretization on a lattice of spacing a forces a strictly positive gap Δ_RS(a) > 0. Jcost is the cost function imported from the Cost module and satisfies the positivity and normalization properties used throughout the Recognition framework.
proof idea
The declaration is a definition, not a theorem. Its companion witness lattice_gap_witness unfolds the existential predicate and supplies the concrete witness Δ = Jcost(1 + a)/2, invoking Jcost_pos_of_ne_one to obtain strict positivity together with the elementary inequality Jcost(1 + a)/2 < Jcost(1 + a).
why it matters
The definition supplies the lattice_gap field required by the HamiltonianSpectrumCert structure that certifies the five-sector spectrum (vacuum, Goldstone, massive scalar, vector, tensor) together with the positive lattice gap. It directly addresses the mass-gap question for Yang-Mills (S7) by showing that lattice discretization yields Δ_RS(a) > 0, consistent with the J-uniqueness and phi-ladder constructions of the Recognition framework. No open scaffolding remains for this structural claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.