pith. machine review for the scientific record. sign in
theorem proved term proof

local_cache_forcing_certificate

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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

proof body

Term-mode proof.

 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

depends on (4)

Lean names referenced from this declaration's body.