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). -/
used by (5)
From the project-wide theorem graph. These declarations reference this one in their body.