module module

`IndisputableMonolith.NavierStokes.FRCBridge`

show as: view Lean formalization →

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

generate prose now

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.NavierStokes.PhiLadderCutoff module_import

declarations in this module (17)

structure FiniteVolumeProfile L39
def normalizedRatio L49
theorem normalizedRatio_pos L52
theorem normalizedRatio_ge_one L56
theorem normalizedRatio_le_sqrt_siteCount L60
theorem Jcost_le_self_of_one_le L72
theorem finiteVolume_Jcost_bound L79
def RSLatticeFRC L88
def LatticeFRC L92
theorem frc_holds_on_RS_lattice L95
theorem frc_holds_on_RS_lattice_exists L98
structure ConditionalCompletionRoute L107
theorem close_conditional_loop L119
structure LatticeRegularityCertificate L130
theorem lattice_regular_via_direction_constancy L142
structure FRCBridgeCert L153
def frcBridgeCert L165