collocation_minimizes_cost

formal source

  91/-! ## Part 4: Collocation Minimizes Cost -/
  92
  93/-- **COLLOCATION MINIMIZES COST**: Distance 0 beats any nonzero distance. -/
  94theorem collocation_minimizes_cost (d : ℕ) (hd : 0 < d) :
  95    Jcost (phi ^ 0) < Jcost (phi ^ d) :=
  96  Jcost_phi_pow_strictMono hd
  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)