phi_eleventh_eq

formal source

 206    _ = 55 * phi + 34 := by ring
 207
 208/-- Key identity: φ¹¹ = 89φ + 55 (Fibonacci recurrence). -/
 209lemma phi_eleventh_eq : phi^11 = 89 * phi + 55 := by
 210  calc phi^11 = phi * phi^10 := by ring
 211    _ = phi * (55 * phi + 34) := by rw [phi_tenth_eq]
 212    _ = 55 * phi^2 + 34 * phi := by ring
 213    _ = 55 * (phi + 1) + 34 * phi := by rw [phi_sq_eq]
 214    _ = 89 * phi + 55 := by ring
 215
 216/-! ### Canonical constants derived from φ -/
 217
 218/-- Canonical locked fine-structure constant: α_lock = (1 − 1/φ)/2. -/
 219@[simp] noncomputable def alphaLock : ℝ := (1 - 1 / phi) / 2
 220
 221/-- Useful bridge identity: the “acceleration-parameterized” exponent is `2·alphaLock`.
 222
 223This is purely algebraic (no physics): it just clears the `/2` in the definition. -/
 224lemma two_mul_alphaLock : 2 * alphaLock = 1 - 1 / phi := by
 225  unfold alphaLock
 226  ring_nf
 227
 228lemma alphaLock_pos : 0 < alphaLock := by
 229  have hphi := one_lt_phi
 230  unfold alphaLock
 231  have : 1 / phi < 1 := (div_lt_one phi_pos).mpr hphi
 232  linarith
 233
 234lemma alphaLock_lt_one : alphaLock < 1 := by
 235  have hpos : 0 < phi := phi_pos
 236  unfold alphaLock
 237  have : 1 / phi > 0 := one_div_pos.mpr hpos
 238  linarith
 239