theorem proved term proof

`access_cost_increases_with_distance`

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

formal statement (Lean)

  77theorem access_cost_increases_with_distance (d₁ d₂ : ℕ) (h : d₁ < d₂) :
  78    Jcost (phi ^ d₁) < Jcost (phi ^ d₂) :=

Term-mode proof.

  79  Jcost_phi_pow_strictMono h
  80
  81/-- Zero distance has zero cost. -/

Lean names referenced from this declaration's body.

has in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
Jcost_phi_pow_strictMono in IndisputableMonolith.Papers.GCIC.LocalCacheForcing decl_use