phi_fibonacci_recursion

formal source

 304/-- **QG-004**: φ^(n+2) = φ^(n+1) + φ^n. Fibonacci recursion for φ-powers.
 305
 306    Proof: φ^(n+2) = φ²·φⁿ = (φ+1)·φⁿ = φ^(n+1) + φⁿ. Uses φ² = φ+1 only. -/
 307theorem phi_fibonacci_recursion (n : ℕ) :
 308    phi ^ (n + 2) = phi ^ (n + 1) + phi ^ n := by
 309  calc phi ^ (n + 2)
 310      = phi ^ 2 * phi ^ n       := by ring
 311    _ = (phi + 1) * phi ^ n     := by rw [phi_sq_eq]
 312    _ = phi ^ (n + 1) + phi ^ n := by ring
 313
 314/-- Fermion mass ladder is Fibonacci: m_{r+2} = m_{r+1} + m_r.
 315
 316    For any yardstick y and rung n:
 317      y · φ^(n+2) = y · φ^(n+1) + y · φ^n
 318
 319    **The particle mass spectrum is a Fibonacci sequence.** -/
 320theorem fibonacci_mass_recursion (y : ℝ) (n : ℕ) :
 321    y * phi ^ (n + 2) = y * phi ^ (n + 1) + y * phi ^ n := by
 322  rw [phi_fibonacci_recursion]; ring
 323
 324/-- The ratio of consecutive masses = φ. -/
 325theorem mass_ratio_is_phi (y : ℝ) (hy : 0 < y) (n : ℕ) :
 326    (y * phi ^ (n + 1)) / (y * phi ^ n) = phi := by
 327  have hphin : (0 : ℝ) < phi ^ n := pow_pos phi_pos n
 328  field_simp [ne_of_gt hy, ne_of_gt hphin]; ring
 329
 330/-- Fibonacci triple: m_r + m_{r+1} = m_{r+2} (inverse Fibonacci form). -/
 331theorem fibonacci_triple_sum (y : ℝ) (n : ℕ) :
 332    y * phi ^ n + y * phi ^ (n + 1) = y * phi ^ (n + 2) := by
 333  linarith [fibonacci_mass_recursion y n]
 334
 335/-- Mass ladder is strictly increasing: φ > 1 implies each rung is heavier. -/
 336theorem mass_ladder_strictly_increasing (y : ℝ) (hy : 0 < y) (n : ℕ) :
 337    y * phi ^ n < y * phi ^ (n + 1) := by