phiLadderPosition

formal source

 122/-! ## §1. The φ-Ladder: Positions and Ratios -/
 123
 124/-- A position on the φ-ladder is φⁿ for integer n. -/
 125def phiLadderPosition (n : ℤ) : ℝ := phi ^ n
 126
 127/-- φ-ladder positions are always positive. -/
 128theorem phiLadderPosition_pos (n : ℤ) : 0 < phiLadderPosition n :=
 129  zpow_pos phi_pos n
 130
 131/-- Adjacent φ-ladder positions have ratio φ. -/
 132theorem adjacent_phi_ratio (n : ℤ) :
 133    phiLadderPosition (n + 1) / phiLadderPosition n = phi := by
 134  simp only [phiLadderPosition]
 135  have hphin : phi ^ n ≠ 0 := zpow_ne_zero n phi_ne_zero
 136  have h1 : phi ^ (n + 1) = phi ^ n * phi := by
 137    rw [zpow_add₀ phi_ne_zero, zpow_one]
 138  rw [h1]
 139  field_simp [hphin]
 140
 141/-- The golden recurrence on the φ-ladder: adjacent positions collapse.
 142    φⁿ + φⁿ⁺¹ = φⁿ⁺² (from φ² = φ + 1). -/
 143theorem adjacent_collapses (n : ℤ) :
 144    phiLadderPosition n + phiLadderPosition (n + 1) = phiLadderPosition (n + 2) := by
 145  simp only [phiLadderPosition]
 146  have hsq : phi ^ 2 = phi + 1 := phi_sq_eq
 147  have h1 : phi ^ (n + 1) = phi ^ n * phi := by
 148    rw [zpow_add₀ phi_ne_zero, zpow_one]
 149  have h2 : phi ^ (n + 2) = phi ^ n * phi ^ 2 := by
 150    rw [show n + 2 = n + (2 : ℤ) from rfl, zpow_add₀ phi_ne_zero,
 151        show (2 : ℤ) = ((2 : ℕ) : ℤ) from rfl, zpow_natCast]
 152  rw [h1, h2, hsq]; ring
 153
 154/-! ## §2. J-Cost of Adjacent Occupation -/
 155