theorem
proved
tactic proof
phi_series_sum
show as:
view Lean formalization →
formal statement (Lean)
161theorem phi_series_sum : ∑' (n : ℕ), (1/φ)^(n+1) = φ := by
proof body
Tactic-mode proof.
162 -- This is the geometric series: ∑_{n≥0} r^(n+1) = r/(1-r) for |r| < 1
163 -- With r = 1/φ, we get (1/φ)/(1 - 1/φ) = 1/(φ-1) = φ (since 1/φ = φ-1)
164 have h_inv_pos := phi_inv_pos
165 have h_inv_lt_one := phi_inv_lt_one
166 have h_phi_pos := phi_pos
167 have h_phi_gt_one := phi_gt_one
168 -- Rewrite the sum as r * geom_series(r) = r/(1-r)
169 have h_eq : ∑' (n : ℕ), (1/φ)^(n+1) = (1/φ) * ∑' (n : ℕ), (1/φ)^n := by
170 rw [← tsum_mul_left]
171 congr 1
172 ext n
173 ring
174 rw [h_eq]
175 -- Use the geometric series formula: ∑ r^n = 1/(1-r)
176 have h_nonneg : 0 ≤ 1/φ := le_of_lt h_inv_pos
177 rw [tsum_geometric_of_lt_one h_nonneg h_inv_lt_one]
178 -- Goal: (1/φ) * (1 - 1/φ)⁻¹ = φ
179 have h_phi_ne : φ ≠ 0 := ne_of_gt h_phi_pos
180 have h_denom_ne : φ - 1 ≠ 0 := ne_of_gt (by linarith)
181 -- φ(φ-1) = φ² - φ = 1 (from φ² = φ + 1)
182 have h_prod : φ * (φ - 1) = 1 := by
183 have h := phi_is_self_similar
184 unfold IsSelfSimilar at h
185 linarith
186 have h_key : φ - 1 = 1/φ := phi_inv_eq.symm
187 have h_denom_ne' : 1/φ ≠ 0 := by positivity
188 -- The whole expression simplifies to φ
189 field_simp
190 -- Goal becomes φ = φ * (φ - 1) after field_simp... but φ * (φ-1) = 1
191 linarith
192
193/-! ## Stable Positions -/
194
195/-- A position x > 0 is stable if J-cost is locally minimized there.
196
197 For self-similar patterns, stability requires the ratio to satisfy r² = r + 1. -/