flowRegime_count
plain-language theorem explainer
The declaration fixes the cardinality of the flow-regime type at five, matching the five canonical regimes used in hydrodynamic classification inside Recognition Science. Modelers working on Reynolds-number ladders and regime transitions cite this count when assembling the NavierStokesRegimesCert structure. The proof is a single decide tactic that evaluates the Fintype instance generated automatically from the five-constructor inductive definition.
Claim. Let FlowRegime be the inductive type whose constructors are laminar, transitional, fullyTurbulent, inertialRange and dissipativeSubrange. Then its cardinality satisfies $|FlowRegime| = 5$.
background
The module supplies a structural enumeration of turbulent-flow regimes, each separated by Reynolds-number rungs on a φ-ladder. FlowRegime is defined inductively with exactly the five constructors laminar, transitional, fullyTurbulent, inertialRange and dissipativeSubrange, and it derives DecidableEq, Repr, BEq and Fintype. The module document states that this enumeration corresponds to configDim D = 5 and is offered only as a classification device; it makes no claim about global regularity of the Navier-Stokes equations. An upstream inductive definition in HydrodynamicsFromRS supplies a different five-element regime list (laminar, turbulent, supersonic, subsonic, multiphase) that is referenced but not used for the cardinality computation here.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the goal Fintype.card FlowRegime = 5. The tactic succeeds because the inductive definition of FlowRegime automatically generates a Fintype instance whose cardinality is the number of listed constructors.
why it matters
The result populates the five_regimes field of the downstream navierStokesRegimesCert definition. It supplies the concrete count required by the Recognition Science framework for hydrodynamic regime classification, consistent with the five-regime count tied to configDim D = 5 and the φ-ladder separation of regimes. The module document explicitly notes that the enumeration does not address the Clay Millennium problem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.