HydrodynamicsCert
plain-language theorem explainer
HydrodynamicsCert encodes the assertions that Recognition Science fluid dynamics has exactly five flow regimes, zero J-cost at uniform flow, and positive J-cost for all other positive flow ratios. A researcher deriving Navier-Stokes regimes from the recognition field would reference this certificate when connecting J-cost signs to turbulence onset. The declaration is a bare structure whose fields are filled by a downstream one-line assembly of regime cardinality and cost lemmas.
Claim. The hydrodynamics certificate requires that the cardinality of the set of flow regimes equals 5, that the recognition cost function satisfies $J(1)=0$, and that $J(r)>0$ for every real $r>0$ with $r≠1$.
background
In the Hydrodynamics from RS module, fluid dynamics emerges from the recognition cost J applied to a fluid lattice. The FlowRegime inductive type defines the five regimes (laminar, turbulent, supersonic, subsonic, multiphase) whose count equals configDim D=5. At equilibrium uniform flow the cost vanishes, while vorticity in turbulence incurs positive cost. The upstream NavierStokesRegimes module supplies a related but distinct enumeration of flow regimes used in the broader Navier-Stokes analysis.
proof idea
The declaration introduces a structure with three fields. No proof body exists; the structure is instantiated downstream by applying flowRegimeCount to establish the cardinality, laminar_equilibrium for the zero at unit ratio, and turbulent_cost for the positivity condition.
why it matters
This certificate supports the hydrodynamicsCert construction and anchors the claim that Navier-Stokes regimes arise directly from the J-cost in Recognition Science. It realizes the five-regime count as configDim D=5 and connects to the forcing chain landmarks where costs and dimensions are derived. The structure closes the interface between the Cost module and fluid-specific assertions without introducing new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.