constant_ratio

formal source

  64  ∀ ℓ : ℕ, K (ℓ + 2) = K (ℓ + 1) + K ℓ
  65
  66/-- The constant-ratio property: K_{ℓ+1}/K_ℓ = r for all ℓ. -/
  67def constant_ratio (K : ℕ → ℝ) (r : ℝ) : Prop :=
  68  ∀ ℓ : ℕ, K (ℓ + 1) = r * K ℓ
  69
  70/-- **KEY LEMMA**: Fibonacci recurrence + constant positive ratio → r² = r + 1.
  71
  72This is the rigorous replacement for the hand-wavy "self-similar cost" argument. -/
  73theorem fibonacci_ratio_forces_golden (K : ℕ → ℝ) (r : ℝ)
  74    (_hr_pos : 0 < r)
  75    (hK_pos : ∀ ℓ, 0 < K ℓ)
  76    (hfib : fibonacci_recurrence K)
  77    (hratio : constant_ratio K r) :
  78    r ^ 2 = r + 1 := by
  79  -- From constant_ratio: K(ℓ+2) = r * K(ℓ+1) = r * (r * K(ℓ)) = r² * K(ℓ)
  80  have hK2 : ∀ ℓ, K (ℓ + 2) = r ^ 2 * K ℓ := by
  81    intro ℓ
  82    have h1 := hratio (ℓ + 1)  -- K(ℓ+2) = r * K(ℓ+1)
  83    have h2 := hratio ℓ         -- K(ℓ+1) = r * K(ℓ)
  84    rw [h2] at h1
  85    rw [h1]
  86    ring
  87  -- From fibonacci_recurrence: K(ℓ+2) = K(ℓ+1) + K(ℓ)
  88  -- Combined: r² * K(ℓ) = r * K(ℓ) + K(ℓ) = (r + 1) * K(ℓ)
  89  have hcombine : ∀ ℓ, r ^ 2 * K ℓ = (r + 1) * K ℓ := by
  90    intro ℓ
  91    have h1 := hK2 ℓ
  92    have h2 := hfib ℓ
  93    have h3 := hratio ℓ
  94    linarith
  95  -- Since K(0) > 0, we can cancel: r² = r + 1
  96  have hK0 := hK_pos 0
  97  have h_eq := hcombine 0