theorem
proved
Jcost_phi_pow_strictMono
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Papers.GCIC.LocalCacheForcing on GitHub at line 70.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
67 exact pow_lt_pow_right₀ one_lt_phi hmn
68
69/-- **J(φ^m) < J(φ^n) FOR m < n**. -/
70theorem Jcost_phi_pow_strictMono {m n : ℕ} (hmn : m < n) :
71 Jcost (phi ^ m) < Jcost (phi ^ n) :=
72 Jcost_strictMono_on_Ici_one (phi_pow_ge_one m) (phi_pow_strictMono hmn)
73
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