FlowRegime
plain-language theorem explainer
This inductive type enumerates the five canonical regimes of fluid flow in the Recognition Science hydrodynamics model. A researcher partitioning the Reynolds-number axis on the phi-ladder into laminar, transitional, fully developed turbulent, inertial-range, and dissipative-subrange intervals would cite it when labeling flow states. The definition proceeds by direct inductive construction of the five cases, from which the Fintype instance of cardinality five follows automatically.
Claim. The flow regimes form the inductive type generated by the five constructors laminar, transitional, fully developed turbulent, inertial range, and dissipative subrange, with consecutive regimes separated by Reynolds-number rungs on the $phi$-ladder.
background
The Navier-Stokes Regimes module supplies a structural enumeration of turbulent flow regimes, identified with configDim D = 5. The five regimes are laminar flow, transitional flow, fully developed turbulence, the inertial range, and the dissipative subrange. Reynolds-number thresholds arranged on the phi-ladder separate these regimes, as stated in the module documentation: 'Reynolds number rungs on a φ-ladder separate the regimes.' The module is explicitly not a closure of the Clay Millennium Navier-Stokes problem and advances no claim about global regularity.
proof idea
The declaration is the inductive definition of the five constructors. The derived Fintype, DecidableEq, and related instances follow immediately from the finite list of cases with no additional lemmas or tactics applied.
why it matters
This definition supplies the five_regimes field required by NavierStokesRegimesCert, which further asserts that consecutive Reynolds thresholds satisfy the phi ratio. It likewise feeds the HydrodynamicsCert structure in the parent hydrodynamics module. Within the Recognition Science framework it realizes configDim D = 5 for flow regimes, consistent with the phi-ladder structure from the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.