DiscreteModel
plain-language theorem explainer
DiscreteModel supplies the minimal interface for a discrete dynamical system approximating the incompressible Navier-Stokes equations. Researchers constructing Recognition Science bridges to classical fluids cite this structure when specifying discrete approximations that later connect to CPM energy functionals and LNAL execution semantics. The definition is a plain structure declaration that introduces a state type, a discretization tag, and a parameterized step map with no computational content or lemmas.
Claim. A structure encoding a discrete approximation to the Navier-Stokes equations, consisting of a state type, a discretization family (spectral Galerkin or finite differences), and a time-stepping operator that maps parameters, a positive time increment, and the current state to the subsequent state.
background
The module supplies an interface for discrete Navier-Stokes models without committing to a concrete scheme. NSParams records spatial dimension (default 3) and kinematic viscosity (default 1), subject to the validity predicate requiring positive viscosity and dimension at least 2. TimeStep records a positive real increment. DiscretizationKind is the inductive tag distinguishing spectralGalerkin from finiteDifference. This interface is designed to connect later to LNAL spatial semantics and to CPM instantiations supplying defect mass, orthogonal mass, energy gap, and test functionals. Upstream CPM2D.model builds a full Model from a hypothesis bundle that includes such discrete states.
proof idea
The declaration is a structure definition that directly introduces the three required fields: State as a Type, kind drawn from DiscretizationKind, and step of type NSParams → TimeStep → State → State. No lemmas are applied; the construction is purely by field introduction.
why it matters
This structure is consumed by RSNSBridgeSpec, which bundles NSParams, TimeStep, and DiscreteModel into the specification for the Recognition Science to Navier-Stokes bridge. It also supports the optional EnergyFunctional supplying an a priori energy bound. In the framework it provides the discrete side of the classical fluids bridge, allowing later instantiation with concrete models such as Galerkin truncation before relating to the eight-tick octave and phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.