PhiLadder
plain-language theorem explainer
PhiLadder(n) supplies the nth element of the golden-ratio lattice used to discretize stable positions in the J-cost functional. Researchers deriving the Yang-Mills mass gap from Recognition Science cite it when indexing excitations on the φ-lattice. The definition is a direct abbreviation applying real exponentiation to the constant φ.
Claim. The element of the golden-ratio ladder at integer index $n$ is given by $phi^n$, where $phi$ satisfies $phi^2 = phi + 1$.
background
The φ-ladder consists of all stable positions forced by self-similar J-cost minimization. Upstream result states: 'The φ-ladder: all stable positions are φ^n for integer n.' In this module the indexed form allows direct reference to individual rungs when computing costs. The local theoretical setting is the exact derivation of the Yang-Mills mass gap Δ = J(φ) = (√5 - 2)/2 from the J-cost functional on this lattice, as stated in the module documentation.
proof idea
This declaration is a one-line definition that applies the real power operation to the golden ratio constant φ.
why it matters
It supplies the indexed elements used in H_StableIffPhiLadder to equate stable positions with the φ-ladder and in mass_gap_is_spatial_minimum to bound the gap by Jcost(PhiLadder n) for n ≠ 0. The definition realizes the discrete substrate required by the T6 phi-forcing step in the unified forcing chain. It supports the claim that the spectral gap is exactly J(φ) with no free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.