adjacent_phi_ratio
plain-language theorem explainer
Adjacent positions on the φ-ladder satisfy a constant ratio equal to the golden ratio φ. Partition theorists and Recognition Science modelers cite this when deriving the minimal rung separation from the golden recurrence. The proof is a short algebraic reduction that substitutes the ladder definition, invokes non-vanishing of φ, and cancels powers via field simplification.
Claim. For every integer $n$, $φ^{n+1}/φ^n = φ$.
background
The φ-ladder is defined by phiLadderPosition n := φ^n for integer n. This places positions at successive powers of the golden ratio. The module establishes that adjacent occupations are unstable because φ^n + φ^{n+1} collapses to φ^{n+2} via the identity φ² = φ + 1. Upstream results include phi_ne_zero, which asserts φ ≠ 0 and is used to justify exponent rules and division. The PrimitiveDistinction theorem provides the foundational axioms leading to these structural conditions.
proof idea
The tactic proof first simplifies the definition of phiLadderPosition. It then establishes that φ^n is nonzero using phi_ne_zero. A rewriting step applies the exponent addition rule φ^{n+1} = φ^n * φ. Finally, field_simp cancels the common factor to yield the ratio φ.
why it matters
This result underpins the J-cost argument for why adjacent rungs on the φ-ladder are unstable, directly supporting the 'differ by ≥ 2' constraint in the Rogers-Ramanujan decipherment. It connects to the self-similar fixed point property of φ in the Recognition framework. It closes the algebraic step needed for collapse lemmas in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.