caching_is_forced

formal source

  97
  98/-- **CACHING IS FORCED**: Any allocation with a remote pattern has strictly
  99    higher total weighted cost than the fully collocated allocation. -/
 100theorem caching_is_forced
 101    (n : ℕ) (freq : Fin n → ℝ) (dist_alloc : Fin n → ℕ)
 102    (hfreq_pos : ∀ i, 0 < freq i)
 103    (hremote : ∃ i, 0 < dist_alloc i) :
 104    (∑ i : Fin n, freq i * Jcost (phi ^ 0)) <
 105    (∑ i : Fin n, freq i * Jcost (phi ^ (dist_alloc i))) := by
 106  obtain ⟨j, hj⟩ := hremote
 107  apply Finset.sum_lt_sum
 108  · intro i _
 109    apply mul_le_mul_of_nonneg_left _ (le_of_lt (hfreq_pos i))
 110    rw [access_cost_zero_at_origin]
 111    exact Jcost_nonneg (pow_pos phi_pos _)
 112  · exact ⟨j, Finset.mem_univ j, by
 113      apply mul_lt_mul_of_pos_left _ (hfreq_pos j)
 114      exact collocation_minimizes_cost _ hj⟩
 115
 116/-! ## Part 5: φ from Fibonacci -/
 117
 118/-- **φ FROM FIBONACCI**: If r > 0 satisfies r² = r + 1, then r = φ. -/
 119theorem phi_from_fibonacci_ratio (r : ℝ) (hr_pos : 0 < r)
 120    (hfib : r ^ 2 = r + 1) : r = phi := by
 121  have hsq5 : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 5)
 122  have hsqrt5_gt1 : Real.sqrt 5 > 1 := by
 123    have : Real.sqrt 5 > Real.sqrt 1 :=
 124      Real.sqrt_lt_sqrt (by norm_num) (by norm_num : (1 : ℝ) < 5)
 125    simpa [Real.sqrt_one] using this
 126  have hdisc : (r - (1 + Real.sqrt 5) / 2) * (r - (1 - Real.sqrt 5) / 2) = 0 := by
 127    nlinarith [hsq5]
 128  rcases mul_eq_zero.mp hdisc with h | h
 129  · unfold phi; linarith
 130  · exfalso