`phiLadderCutoff`

definition

show as: view math explainer →

module: IndisputableMonolith.NavierStokes.PhiLadderCutoff
domain: NavierStokes
line: 240 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NavierStokes.PhiLadderCutoff on GitHub at line 240.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 237    Jcost (max_val / ref_val) ≤ B → max_val ≤ (2 * B + 2) * ref_val
 238
 239/-- The main certificate: all results assembled. Zero sorry. -/
 240def phiLadderCutoff : PhiLadderCutoffCert where
 241  Jcost_nonneg_cert := Jcost_nonneg
 242  Jcost_zero_iff_cert := Jcost_eq_zero_iff
 243  cascade_finite_cert := cascadeDepth_finite
 244  cascade_mono_cert := cascadeDepth_mono
 245  decay_lt_one := subDissipationDecayFactor_lt_one
 246  decay_to_zero := sub_dissipation_decay_to_zero
 247  finitely_many_rungs := finitely_many_rungs_below
 248  blowup_excluded := bounded_Jcost_bounded_max
 249
 250end
 251
 252end PhiLadderCutoff
 253end NavierStokes
 254end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.