access_cost_increases_with_distance

formal source

  74/-! ## Part 3: Access Cost Properties -/
  75
  76/-- Farther access costs more. -/
  77theorem access_cost_increases_with_distance (d₁ d₂ : ℕ) (h : d₁ < d₂) :
  78    Jcost (phi ^ d₁) < Jcost (phi ^ d₂) :=
  79  Jcost_phi_pow_strictMono h
  80
  81/-- Zero distance has zero cost. -/
  82theorem access_cost_zero_at_origin : Jcost (phi ^ 0) = 0 := by
  83  simp [Jcost_unit0]
  84
  85/-- Nonzero distance has positive cost. -/
  86theorem access_cost_pos_of_nonzero (d : ℕ) (hd : 0 < d) :
  87    0 < Jcost (phi ^ d) := by
  88  rw [← access_cost_zero_at_origin]
  89  exact Jcost_phi_pow_strictMono hd
  90
  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