structure
definition
FRCBridgeCert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NavierStokes.FRCBridge on GitHub at line 153.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
150/-! ## Packaged certificate -/
151
152/-- The full logical closure package for the lattice-to-conditional bridge. -/
153structure FRCBridgeCert where
154 frc_on_lattice :
155 ∀ s : FiniteVolumeProfile, RSLatticeFRC s
156 frc_exists_bound :
157 ∀ s : FiniteVolumeProfile, LatticeFRC s
158 conditional_loop :
159 ∀ (route : ConditionalCompletionRoute FiniteVolumeProfile)
160 (profile : FiniteVolumeProfile),
161 (∀ s : FiniteVolumeProfile, RSLatticeFRC s → route.FRC s) →
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