adjacent_collapses
plain-language theorem explainer
Adjacent positions on the φ-ladder collapse according to the golden recurrence. Researchers in partition theory cite this to ground the differ-by-at-least-two rule in Rogers-Ramanujan identities. The short tactic proof reduces the statement to the defining equation of φ via exponent arithmetic and ring simplification.
Claim. For the golden ratio φ satisfying φ² = φ + 1, the φ-ladder positions satisfy φⁿ + φ^{n+1} = φ^{n+2} for every integer n.
background
The φ-ladder stability module treats positions as integer powers of the golden ratio φ. Adjacent occupation is unstable because the recurrence forces collapse into a single higher rung, as stated in the module documentation: φⁿ + φⁿ⁺¹ = φⁿ(1 + φ) = φⁿ · φ² = φⁿ⁺². This supplies the J-cost admissibility constraint that enforces the Rogers-Ramanujan gap rule of at least 2.
proof idea
The tactic proof first applies simp to unfold the definition of phiLadderPosition into explicit powers of φ. It obtains φ² = φ + 1 directly from phi_sq_eq, then derives the shifted exponents via zpow_add₀ using phi_ne_zero. Substitution followed by the ring tactic completes the verification.
why it matters
This result is invoked by adjacent_absorptive to exhibit explicit collapse to a higher rung and by zeckendorf_rogers_ramanujan_same_constraint to equate the Fibonacci non-consecutive condition with the Rogers-Ramanujan gap rule. It supplies the concrete algebraic step showing that J-cost structure on the φ-ladder forces minimal separation of 2, consistent with the self-similar fixed point φ in the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.