pith. sign in
module module moderate

IndisputableMonolith.Mathematics.NavierStokesRegimes

show as:
view Lean formalization →

The module defines flow regime classifications and Reynolds number thresholds for the Navier-Stokes equations inside Recognition Science. Fluid dynamicists working in RS-native units would cite it to locate laminar-turbulent transitions on the phi-ladder. The module consists entirely of definitions and short supporting lemmas with no proof obligations.

claimIntroduces an enumeration of fluid flow regimes, a count of those regimes, a threshold function mapping each regime to a real Reynolds number, the associated ratio and positivity statements, and a certification object for the Navier-Stokes regimes.

background

The module sits in the mathematics layer and imports only the RS time quantum τ₀ = 1 tick from Constants together with Mathlib. It supplies the concrete objects needed to classify incompressible flows once the Reynolds number has been expressed in phi-ladder units. The surrounding Recognition Science setting treats fluid motion as a discrete process whose energy cost is measured by the J-functional and whose length scales are fixed by the eight-tick octave.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the regime classification layer that later fluid-dynamics results in Recognition Science are expected to invoke. It directly encodes the thresholds that arise from the phi-ladder and the RS constants, thereby closing the interface between the abstract forcing chain and concrete Navier-Stokes analysis. No downstream uses are recorded yet.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)