theorem
proved
local_cache_forcing_certificate
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 153.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
150 2. J(φ^0) = 0 (collocated access is free)
151 3. d > 0 ⟹ J(φ^0) < J(φ^d) (collocation beats remote)
152 4. r² = r + 1, r > 0 ⟹ r = φ (Fibonacci forces φ) -/
153theorem local_cache_forcing_certificate :
154 (∀ m n : ℕ, m < n → Jcost (phi ^ m) < Jcost (phi ^ n))
155 ∧ (Jcost (phi ^ 0) = 0)
156 ∧ (∀ d : ℕ, 0 < d → Jcost (phi ^ 0) < Jcost (phi ^ d))
157 ∧ (∀ r : ℝ, 0 < r → r ^ 2 = r + 1 → r = phi) := by
158 exact ⟨fun m n hmn => Jcost_phi_pow_strictMono hmn,
159 access_cost_zero_at_origin,
160 fun d hd => collocation_minimizes_cost d hd,
161 fun r hr hfib => phi_from_fibonacci_ratio r hr hfib⟩
162
163end
164
165end IndisputableMonolith.Papers.GCIC.LocalCacheForcing