`frcBridgeCert`

definition

show as: view math explainer →

module: IndisputableMonolith.NavierStokes.FRCBridge
domain: NavierStokes
line: 165 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.NavierStokes.FRCBridge on GitHub at line 165.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 162      route.Regularity profile
 163
 164/-- The lattice FRC bridge certificate. -/
 165def frcBridgeCert : FRCBridgeCert where
 166  frc_on_lattice := frc_holds_on_RS_lattice
 167  frc_exists_bound := frc_holds_on_RS_lattice_exists
 168  conditional_loop := fun route profile hFRCBridge =>
 169    lattice_regular_via_direction_constancy route profile hFRCBridge
 170
 171end
 172
 173end FRCBridge
 174end NavierStokes
 175end IndisputableMonolith

papers checked against this theorem

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