theorem proved term proof

`collocation_minimizes_cost`

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

formal statement (Lean)

  94theorem collocation_minimizes_cost (d : ℕ) (hd : 0 < d) :
  95    Jcost (phi ^ 0) < Jcost (phi ^ d) :=

proof body

Term-mode proof.

  96  Jcost_phi_pow_strictMono hd
  97
  98/-- **CACHING IS FORCED**: Any allocation with a remote pattern has strictly
  99    higher total weighted cost than the fully collocated allocation. -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

brain_holography_fully_forced in IndisputableMonolith.Papers.GCIC.BrainHolography decl_use
caching_is_forced in IndisputableMonolith.Papers.GCIC.LocalCacheForcing decl_use
local_cache_forcing_certificate in IndisputableMonolith.Papers.GCIC.LocalCacheForcing decl_use

depends on (6)

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
total in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use
total in IndisputableMonolith.NumberTheory.RiemannHypothesis.ErrorBudget decl_use
Jcost_phi_pow_strictMono in IndisputableMonolith.Papers.GCIC.LocalCacheForcing decl_use