sequential_optimization_forces_phi

formal source

 251
 252/-- The sequential fixed-point core:
 253    the continued-fraction update has φ as fixed point. -/
 254theorem sequential_optimization_forces_phi :
 255    cfracIteration phi = phi := phi_is_cfrac_fixed_point
 256
 257/-- Strong fixed-point form: any positive fixed point of `x ↦ 1 + 1/x` is `φ`.
 258
 259    (Interpretation) Any sequential optimization with:
 260    (1) Self-similarity (same cost at every level)
 261    (2) Strict convexity of cost functional
 262    (3) Discrete (integer) choices at each level
 263
 264    converges to φ. This is because:
 265    - Self-similarity → scale ratio r
 266    - Optimality → r satisfies the Fibonacci recurrence
 267    - Convexity → unique positive solution r² = r + 1 → r = φ
 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