hydrodynamicsCert
plain-language theorem explainer
hydrodynamicsCert assembles the HydrodynamicsCert record by wiring the five-regime cardinality, the zero J-cost at unit flow, and the strict positivity of J-cost away from unity. Physicists working on recognition-field derivations of Navier-Stokes would cite it to fix the canonical regime count at five. The construction is a direct structure literal that composes three upstream lemmas with no additional steps.
Claim. A certificate asserting that the number of flow regimes equals five, that the J-cost of uniform flow satisfies $J(1)=0$, and that the J-cost is strictly positive for every positive flow ratio $r$ with $r≠1$.
background
Recognition Science treats fluid flow through the J-cost functional on flow ratios. The HydrodynamicsCert structure encodes three properties: the cardinality of FlowRegime equals five (laminar, turbulent, supersonic, subsonic, multiphase), J-cost vanishes for uniform laminar flow, and J-cost is positive whenever vorticity is present. The module sets the local setting by identifying the Navier-Stokes equation with the recognition field on the fluid lattice and locating the Reynolds threshold near 2300 as gap45 times 51, or equivalently phi^8 times phi^2 in native units.
proof idea
The definition is a direct record construction that supplies the three fields of HydrodynamicsCert. It pulls the regime count from flowRegimeCount, the laminar zero from laminar_equilibrium (itself Jcost_unit0), and the turbulent positivity from turbulent_cost (itself Jcost_pos_of_ne_one). No tactics beyond the literal are required.
why it matters
This definition supplies the concrete witness for the hydrodynamics certificate required by the Recognition Science derivation of fluid regimes from the J-functional. It closes the B12/B11 depth by confirming that five regimes match the configDim D=5 count and that the sign properties of J-cost hold. No downstream uses are recorded, leaving open the question of how the certificate feeds into explicit Reynolds-number calculations or multiphase extensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.