gap_rigidity
plain-language theorem explainer
The gap rigidity theorem shows that no sequence of non-zero integers can drive the recognition cost of φ-ladder elements to zero at infinity. Researchers resolving the Yang-Mills mass gap in the Recognition Science setting cite it to confirm the gap remains strictly positive under all lattice excitations. The proof proceeds by contradiction, rewriting the tendsto assumption, extracting a term below half the gap value, and deriving an immediate contradiction with the strict spectral gap lower bound via linarith.
Claim. Let $J(x) = (x + x^{-1})/2 - 1$ be the recognition cost on the golden-ratio lattice. Let $m > 0$ be the mass gap value. There exists no sequence of non-zero integers $(n_k)$ such that $J(m^{n_k}) → 0$ as $k → ∞$.
background
Recognition Science defines the recognition cost functional $J(x) = ½(x + x^{-1}) − 1$ on the φ-lattice of all φ^n for n ∈ ℤ. The PhiLadder construction supplies exactly these elements, with φ the golden ratio fixed by the self-similar point of the forcing chain. The module derives the Yang-Mills mass gap Δ = J(φ) = (√5 − 2)/2 directly from the Recognition Composition Law together with the J-uniqueness and phi-forcing steps (T5–T6).
proof idea
Assume for contradiction a sequence seq of non-zero integers whose Jcost(PhiLadder(seq k)) tends to zero. Rewrite the tendsto condition with Metric.tendsto_atTop, obtain N such that the distance to zero is less than massGap/2, apply spectral_gap_strict to obtain strict positivity at that term, then close with linarith against the spectral_gap lower bound.
why it matters
This supplies the gap_rigid field of the yang_mills_gap_cert theorem, completing the zero-sorry certificate for QG-005. It directly implements the topological gap claim in the module documentation, showing the minimum excitation cost is rigid under the eight-tick octave and D = 3 forcing. The result closes the final rigidity step needed to embed the mass gap into the broader unification of gauge sectors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.