flowRegimeCount
plain-language theorem explainer
The theorem establishes that the inductive type enumerating canonical flow regimes in Recognition Science hydrodynamics has cardinality exactly five. Researchers deriving fluid dynamics from the J-cost functional on the fluid lattice would cite this to confirm the discrete regime count equals the configuration dimension. The proof is a one-line decision procedure that succeeds via the automatically derived Fintype instance on the five-constructor inductive.
Claim. The set of flow regimes has cardinality five: $|$laminar, turbulent, supersonic, subsonic, multiphase$| = 5$.
background
In the Hydrodynamics from RS module, fluid dynamics is obtained by applying the recognition functional J to a fluid lattice. The local FlowRegime inductive lists five states: laminar (J = 0 for uniform flow), turbulent (J > 0 from vorticity recognition cost), supersonic, subsonic, and multiphase. The module states that this count equals configDim D = 5 and that the Navier-Stokes equation appears in RS as a recognition field on the lattice, with the Reynolds threshold near 2300 identified as gap45 × 51 ≈ φ^8 × φ^2. The upstream NavierStokesRegimes module supplies a different five-regime partition (laminar, transitional, fullyTurbulent, inertialRange, dissipativeSubrange) focused on turbulence stages, while the RS version aligns regimes to equilibrium and cost distinctions.
proof idea
The proof is a one-line wrapper that applies the decide tactic. It succeeds because the inductive definition of FlowRegime derives DecidableEq, Repr, BEq, and Fintype instances, allowing direct computation and verification of the cardinality as 5.
why it matters
This theorem supplies the five_regimes field inside the hydrodynamicsCert definition that certifies the overall hydrodynamics model. It realizes the module claim that five regimes correspond to configDim D = 5, closing the discrete counting step that links fluid regimes to the Recognition Science forcing chain (T0-T8) and the phi-ladder structures. The result anchors the B12/B11 depth analysis without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.