sequential_optimization_forces_phi_strong

formal source

 268
 269    This is exactly the content of `fibonacci_partition_forces_phi`
 270    from the Local Cache theorem, applied to continued fractions. -/
 271theorem sequential_optimization_forces_phi_strong :
 272    ∀ r : ℝ, 0 < r → r = 1 + 1 / r → r = phi := by
 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_∞ = φ.