lattice_gap_witness
plain-language theorem explainer
The lattice gap witness shows that a positive lattice spacing a forces the Recognition Hamiltonian spectral gap to be strictly positive and bounded above by Jcost(1+a). Lattice gauge theorists or Recognition Science researchers modeling the Yang-Mills mass gap would cite it to certify a non-vanishing gap on any discrete lattice. The proof supplies the explicit witness Jcost(1+a)/2 and verifies the two required inequalities by direct appeal to the J-cost positivity lemma plus linear arithmetic.
Claim. For every positive real number $a$, there exists a positive real number $Δ$ such that $Δ < J(1+a)$, where $J$ is the J-cost function.
background
The Recognition Hamiltonian spectrum module isolates the spectral gap Δ_RS on a discretized lattice. The definition latticeSpacingGap asserts existence of a positive Δ strictly below Jcost(1+a). The upstream lemma Jcost_pos_of_ne_one states that J(x) > 0 whenever x > 0 and x ≠ 1, supplying the positivity engine for the witness.
proof idea
The term proof unfolds latticeSpacingGap and refines to the pair consisting of Jcost(1+a)/2 together with two subgoals. The first subgoal applies div_pos to the numerator Jcost(1+a) (via Jcost_pos_of_ne_one with the facts 0 < 1+a and 1+a ≠ 1) and the denominator 2. The second subgoal follows by linarith from the same positivity fact.
why it matters
The witness is inserted verbatim into the HamiltonianSpectrumCert record that certifies the five-sector spectrum. It supplies the concrete positivity step required for the mass-gap claim (S7) inside the Recognition framework and closes the discretization step before any continuum limit. The result participates in the T5–T8 forcing chain that derives three spatial dimensions from the J-uniqueness equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.