271theorem sequential_optimization_forces_phi_strong : 272 ∀ r : ℝ, 0 < r → r = 1 + 1 / r → r = phi := by
proof body
Tactic-mode proof.
273 intro r hr hfix 274 have hr_ne : r ≠ 0 := ne_of_gt hr 275 have hquad : r ^ 2 = r + 1 := by 276 have hrr : r * r = r * (1 + 1 / r) := by 277 exact congrArg (fun t : ℝ => r * t) hfix 278 have hmul : r * r = r + 1 := by 279 calc 280 r * r = r * (1 + 1 / r) := hrr 281 _ = r + 1 := by 282 field_simp [hr_ne] 283 simpa [pow_two] using hmul 284 have hphi : phi ^ 2 = phi + 1 := phi_sq_eq 285 have hprod : (r - phi) * (r + phi - 1) = 0 := by 286 nlinarith [hquad, hphi] 287 have hsecond_pos : 0 < r + phi - 1 := by 288 linarith [hr, one_lt_phi] 289 have hsecond_ne : r + phi - 1 ≠ 0 := ne_of_gt hsecond_pos 290 have hfirst : r - phi = 0 := by 291 exact (mul_eq_zero.mp hprod).resolve_right hsecond_ne 292 linarith 293 294/-- The connection between continued fractions and J-cost: 295 296 A continued fraction [a₀; a₁, a₂, ...] represents a sequence of 297 choices. Each partial quotient aₖ determines a local ratio. 298 The J-cost of the k-th level is J(aₖ + 1/x_{k+1}). 299 300 For the optimal (minimum total J-cost) continued fraction with 301 self-similar structure, all aₖ = 1 and x_∞ = φ. 302 303 This is why Ramanujan's deepest continued fractions always involve φ: 304 they are computing the ground state of sequential J-cost minimization. -/
depends on (28)
Lean names referenced from this declaration's body.