access_cost_pos_of_nonzero

formal source

  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
 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 -/