FlowRegime
plain-language theorem explainer
FlowRegime enumerates five canonical regimes for fluid states in Recognition Science hydrodynamics. A researcher modeling Navier-Stokes within the RS lattice would cite it to fix the discrete configuration space of dimension 5. The declaration is a direct inductive enumeration that derives decidable equality and finite type structure with no additional proof obligations.
Claim. Let $R$ be the inductive type whose constructors are laminar, turbulent, supersonic, subsonic, and multiphase, equipped with decidable equality, representation, Boolean equality, and finite cardinality.
background
The HydrodynamicsFromRS module models fluid dynamics as a recognition field on the fluid lattice. Uniform flow has J-cost zero; vorticity raises the recognition cost above zero. Five regimes are identified with configuration dimension D=5, and the Reynolds threshold near 2300 is expressed as a product of phi-powers (gap45 times 51).
proof idea
The declaration is a direct inductive definition with empty body. It derives DecidableEq, Repr, BEq, and Fintype automatically.
why it matters
FlowRegime supplies the five_regimes field required by HydrodynamicsCert, which further asserts laminar J-cost equals zero and turbulent J-cost strictly positive for non-unit ratios. It anchors the hydrodynamics certification by setting configDim to 5 and feeds the cardinality theorem flowRegimeCount. The construction aligns with the five-tick octave in the forcing chain while leaving the precise phi-ladder derivation of Reynolds thresholds open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.