theorem proved term proof

`access_cost_pos_of_nonzero`

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

formal statement (Lean)

  86theorem access_cost_pos_of_nonzero (d : ℕ) (hd : 0 < d) :
  87    0 < Jcost (phi ^ d) := by

proof body

Term-mode proof.

  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. -/

depends on (5)

Lean names referenced from this declaration's body.

beats in IndisputableMonolith.Gap45 decl_use
beats in IndisputableMonolith.Gap45.Beat decl_use
Cost in IndisputableMonolith.Measurement.RSNative.Core decl_use
access_cost_zero_at_origin in IndisputableMonolith.Papers.GCIC.LocalCacheForcing decl_use
Jcost_phi_pow_strictMono in IndisputableMonolith.Papers.GCIC.LocalCacheForcing decl_use