spectral_gap_strict
plain-language theorem explainer
The strict spectral gap theorem establishes that the recognition cost of any nonzero rung on the golden-ratio lattice is strictly positive. Researchers addressing the Yang-Mills mass gap in discrete lattice models would cite this result for its exact lower bound derived solely from the J-cost functional. The proof proceeds by a direct comparison of the general spectral gap inequality against the positivity of the minimal gap value.
Claim. For every integer $n$ with $n ≠ 0$, let $φ$ denote the golden ratio and $J(x) = ½(x + x^{-1}) - 1$. Then $J(φ^n) > 0$.
background
In the Recognition Science treatment of the Yang-Mills mass gap, the substrate is the discrete φ-lattice consisting of all powers φ^n for n ∈ ℤ. The recognition cost functional is defined by J(x) = ½(x + x^{-1}) - 1, which satisfies the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). The module establishes that this functional has a strict spectral gap separating the vacuum configuration (at rung zero, where J = 0) from all nontrivial excitations. The local setting is the resolution of the Millennium Prize problem for Yang-Mills theory within the RS framework, where the gap emerges from the J-cost on the forced lattice rather than being postulated.
proof idea
The proof is a one-line wrapper that applies the positivity of the minimal gap to the general spectral gap inequality via the ordering lt_of_lt_of_le. It concludes strict positivity for any nonzero rung by direct comparison.
why it matters
This theorem supplies the strict positivity needed for the gauge mass gap theorem and the separation of contractible and non-contractible sectors. It fills the §4 spectral gap step in the module's structure, which resolves the mass gap from the J-cost functional alone as described in the central theorem. It connects to the T5 J-uniqueness and T6 phi fixed point in the forcing chain, providing the exact Δ = J(φ) ≈ 0.1180 that is universal across gauge sectors. Downstream results such as gap_rigidity rely on it to show the gap cannot close under sequences of excitations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.