fibonacci_recurrence

formal source

  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
  79/-- The thermal eigenvalue of the recognition-lattice RG fixed point.
  80
  81    **Why this value is forced:**
  82    1. The φ-ladder is the unique geometric scaling sequence in the
  83       recognition lattice (PhiForcing: r² = r + 1 ↔ r = φ).
  84    2. Consecutive rungs satisfy the Fibonacci recurrence
  85       (`fibonacci_recurrence`), whose characteristic polynomial
  86       is λ² − λ − 1.
  87    3. φ is the unique positive root of this polynomial
  88       (`fibonacci_char_poly_unique_pos_root`).
  89    4. The thermal growth rate per ladder step is therefore φ and
  90       nothing else. -/
  91def thermal_eigenvalue : ℝ := phi
  92
  93theorem thermal_eigenvalue_eq_phi : thermal_eigenvalue = phi := rfl
  94