gap_topologically_protected
plain-language theorem explainer
The declaration shows that the mass gap remains a strict lower bound for the J-cost of every non-trivial phi-ladder rung in any integer sequence. Workers on the Yang-Mills mass gap problem in discrete lattice models would reference this for protection against gap closure. The argument is a direct term application of the spectral gap lemma to each term.
Claim. Let $(n_k)_{k}$ be any sequence of nonzero integers. Then the mass gap satisfies $Δ ≤ J(φ^{n_k})$ for every $k$, where $J(x) = ½(x + x^{-1}) - 1$.
background
The module derives the Yang-Mills mass gap from the recognition cost functional on the golden-ratio lattice. The phi-ladder consists of all powers φ^n for integer n, each carrying a positive J-cost, with the gap Δ defined as the minimal positive value J(φ) = (√5 - 2)/2. Upstream results include the PhiLadder definition ensuring positivity for all integer exponents and the gap derivation supplying the exact closed-form value from closure and Fibonacci factors.
proof idea
The proof is a one-line term wrapper that applies the spectral_gap lemma pointwise: it maps the sequence and the nonzero hypothesis directly to the inequality at each rung seq k.
why it matters
This result secures the topological protection of the mass gap against closure by any sequence of lattice excitations, completing a required step in the RS resolution of the Yang-Mills mass gap. It rests on J-uniqueness from the forcing chain T5 together with the phi fixed point T6 and the eight-tick octave structure. The module documentation lists it among the exact, universal, and topological properties that make the gap falsifiable on the RS scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.