spectral_gap_pos_rung
plain-language theorem explainer
The theorem shows that J-cost attains its minimum positive value at the first positive rung of the phi-ladder, so J(phi) is less than or equal to J(phi^n) for every integer n at least 1. Workers deriving the Yang-Mills mass gap inside Recognition Science cite the result to bound the lowest excitation energy above the vacuum. The proof is a direct term application of the monotonicity lemma Jcost_mono_gt_one to the three facts that the ladder element exceeds 1, phi exceeds 1, and the ladder element is at least phi.
Claim. For every integer $n$ with $ngeq 1$, $J(phi)leq J(phi^n)$, where $J(x)=frac12(x+x^{-1})-1$ and $phi^n$ is the element at rung $n$ on the phi-ladder.
background
The module derives the Yang-Mills mass gap from the single functional J(x) = 1/2 (x + x^{-1}) - 1 evaluated on the discrete phi-lattice. PhiLadder n is defined as phi^n, the n-th power of the golden ratio. The surrounding text states that this J-cost is the unique cost functional forced by T5 and that the phi-lattice itself is forced by T2 plus T6, yielding a strict gap Delta = J(phi) between the vacuum and every non-trivial gauge excitation. Upstream lemmas supply one_lt_phi (phi > 1) and the positivity and ordering properties of the ladder elements.
proof idea
The term proof applies Jcost_mono_gt_one to the three supplied facts phiLadder_gt_one hn, one_lt_phi, and phiLadder_ge_phi hn. Monotonicity of Jcost on (1, infinity) then immediately gives the desired inequality between the rung-n cost and the rung-1 cost.
why it matters
The result supplies the positive-rung half of the parent theorem spectral_gap, which asserts massGap <= Jcost (PhiLadder n) for all nonzero integers n. It thereby completes the claim that every non-vacuum phi-ladder configuration costs at least Delta, the exact value forced by the Recognition Composition Law together with the eight-tick octave and D = 3. The declaration closes one case in the spectral-gap section of the module that resolves the Millennium problem inside the RS framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.