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)
70theorem Jcost_phi_pow_strictMono {m n : ℕ} (hmn : m < n) :
71 Jcost (phi ^ m) < Jcost (phi ^ n) :=
proof body
Term-mode proof.
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. -/
used by (5)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (5)
Lean names referenced from this declaration's body.
-
phi_pow_ge_one
in IndisputableMonolith.Mathematics.RamanujanBridge.PhiLadderStability
decl_use
-
Cost
in IndisputableMonolith.Measurement.RSNative.Core
decl_use
-
Jcost_strictMono_on_Ici_one
in IndisputableMonolith.Papers.GCIC.LocalCacheForcing
decl_use
-
phi_pow_ge_one
in IndisputableMonolith.Papers.GCIC.LocalCacheForcing
decl_use
-
phi_pow_strictMono
in IndisputableMonolith.Papers.GCIC.LocalCacheForcing
decl_use