def definition def or abbrev

`phiLadderCutoff`

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

formal statement (Lean)

 240def phiLadderCutoff : PhiLadderCutoffCert where
 241  Jcost_nonneg_cert := Jcost_nonneg

proof body

Definition body.

 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

depends on (14)

Lean names referenced from this declaration's body.

Jcost_eq_zero_iff in IndisputableMonolith.Cost decl_use
Jcost_nonneg in IndisputableMonolith.Cost decl_use
Jcost_nonneg in IndisputableMonolith.Cost.JcostCore decl_use
Jcost_nonneg in IndisputableMonolith.Gravity.CoherenceCollapse decl_use
Jcost_nonneg in IndisputableMonolith.Gravity.EnergyProcessingBridge decl_use
bounded_Jcost_bounded_max in IndisputableMonolith.NavierStokes.PhiLadderCutoff decl_use
cascadeDepth_finite in IndisputableMonolith.NavierStokes.PhiLadderCutoff decl_use
cascadeDepth_mono in IndisputableMonolith.NavierStokes.PhiLadderCutoff decl_use
finitely_many_rungs_below in IndisputableMonolith.NavierStokes.PhiLadderCutoff decl_use
Jcost_eq_zero_iff in IndisputableMonolith.NavierStokes.PhiLadderCutoff decl_use
Jcost_nonneg in IndisputableMonolith.NavierStokes.PhiLadderCutoff decl_use
PhiLadderCutoffCert in IndisputableMonolith.NavierStokes.PhiLadderCutoff decl_use
subDissipationDecayFactor_lt_one in IndisputableMonolith.NavierStokes.PhiLadderCutoff decl_use
sub_dissipation_decay_to_zero in IndisputableMonolith.NavierStokes.PhiLadderCutoff decl_use