theorem
proved
access_cost_zero_at_origin
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Papers.GCIC.LocalCacheForcing on GitHub at line 82.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
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