fibonacci_partition_forces_phi

formal source

 1053. r > 0, all K_ℓ > 0
 106
 107Then r = φ = (1+√5)/2. -/
 108theorem fibonacci_partition_forces_phi (K : ℕ → ℝ) (r : ℝ)
 109    (hr_pos : 0 < r)
 110    (hK_pos : ∀ ℓ, 0 < K ℓ)
 111    (hfib : fibonacci_recurrence K)
 112    (hratio : constant_ratio K r) :
 113    r = phi := by
 114  have hgolden := fibonacci_ratio_forces_golden K r hr_pos hK_pos hfib hratio
 115  -- r > 0 and r² = r + 1 implies r = φ (by uniqueness of positive root)
 116  -- Use the fact that φ is the unique positive solution to x² = x + 1
 117  have h_eq : r ^ 2 - r - 1 = 0 := by linarith
 118  -- Both r and φ satisfy x² - x - 1 = 0
 119  have h_phi_eq : phi ^ 2 - phi - 1 = 0 := by
 120    have := Constants.phi_sq_eq
 121    linarith
 122  -- The product of roots = -1 (Vieta's), so the other root is negative.
 123  -- Since r > 0 and φ > 0, they must be the same root.
 124  nlinarith [sq_nonneg (r - phi), sq_nonneg (r + phi - 1),
 125             Constants.phi_pos, sq_nonneg (Real.sqrt 5 - 2),
 126             Real.sq_sqrt (show (5 : ℝ) ≥ 0 by norm_num)]
 127
 128/-! ## §3  Why Fibonacci Partition? (Derivation from J-cost symmetry) -/
 129
 130/-- **LEMMA (Optimal Partition)**:
 131For J-cost with symmetry J(x) = J(1/x), the optimal boundary between
 132cache levels balances the "overshoot" cost J(d/D_ℓ) against the
 133"undershoot" cost J(D_{ℓ-1}/d). By symmetry, the optimal point
 134is where d/D_ℓ = D_{ℓ-1}/d, i.e., d² = D_ℓ · D_{ℓ-1}.
 135
 136This geometric-mean boundary gives the partition:
 137  K_{ℓ+1} - K_ℓ = K_{ℓ-1}  (the Fibonacci recurrence). -/
 138theorem Jcost_symmetry_forces_geometric_boundary