fibonacci_char_poly

formal source

  45
  46/-- Characteristic polynomial of the recurrence a(n+2) = a(n+1) + a(n).
  47    Its positive root determines the asymptotic growth rate. -/
  48def fibonacci_char_poly (x : ℝ) : ℝ := x ^ 2 - x - 1
  49
  50/-- φ is a root of the Fibonacci characteristic polynomial. -/
  51theorem fibonacci_char_poly_root : fibonacci_char_poly phi = 0 := by
  52  unfold fibonacci_char_poly; linarith [phi_sq_eq]
  53
  54/-- φ is the unique positive root of the Fibonacci characteristic polynomial. -/
  55theorem fibonacci_char_poly_unique_pos_root (r : ℝ) (hr : 0 < r)
  56    (h : fibonacci_char_poly r = 0) : r = phi := by
  57  unfold fibonacci_char_poly at h
  58  have : r ^ 2 = r + 1 := by linarith
  59  exact IndisputableMonolith.Foundation.PhiForcing.phi_forced r hr this
  60
  61/-! ## 2. The Fibonacci Cascade on the φ-Ladder -/
  62
  63/-- The φ-ladder satisfies the Fibonacci recurrence (natural exponents). -/
  64theorem fibonacci_recurrence (n : ℕ) :
  65    phi ^ (n + 2) = phi ^ (n + 1) + phi ^ n := by
  66  calc phi ^ (n + 2) = phi ^ n * phi ^ 2 := by ring
  67    _ = phi ^ n * (phi + 1) := by rw [phi_sq_eq]
  68    _ = phi ^ (n + 1) + phi ^ n := by ring
  69
  70/-- Consecutive φ-ladder rungs have ratio exactly φ. -/
  71theorem phi_ladder_growth (n : ℕ) :
  72    phi ^ (n + 1) / phi ^ n = phi := by
  73  have h : phi ^ n ≠ 0 := pow_ne_zero _ phi_ne_zero
  74  field_simp
  75  ring
  76
  77/-! ## 3. The Forced Thermal Eigenvalue -/
  78