DiscretizationKind
DiscretizationKind enumerates the two primary families of spatial discretizations for building discrete approximations to the Navier-Stokes equations. Workers on the fluids interface cite it when tagging a model as spectral Galerkin versus finite-difference. The declaration is a plain inductive definition with two constructors and an automatic DecidableEq instance.
claimLet $K$ be the inductive type whose constructors are the spectral Galerkin method and the finite-difference method.
background
The module supplies a minimal interface for discrete Navier-Stokes models that can later be related to LNAL spatial execution semantics and to CPM instantiations (defect, energy, tests). It deliberately postpones the choice between Galerkin and grid-based schemes so that downstream files can supply concrete realizations on, for example, the 2-torus. The four upstream declarations supply supporting constants and model builders: the CPM2D model constructor, the active-edge count A from IntegrationGap, the coherence unit A from Masses.Anchor, and the actualization operator A from Modal.Actualization.
proof idea
One-line inductive definition that introduces two constructors and derives DecidableEq from Mathlib.
why it matters in Recognition Science
The declaration supplies the tag field inside the DiscreteModel structure, allowing the fluids bridge to remain agnostic about discretization while still exposing a uniform interface for state, kind, and one-step evolution. It therefore sits at the entry point of the classical-to-discrete transition that the module doc-comment links to LNAL and CPM. No open question is closed here; the choice remains open for later specialization.
scope and limits
- Does not define any concrete state space or basis functions.
- Does not supply time-stepping rules or stability criteria.
- Does not encode error estimates or convergence statements.
- Does not restrict the underlying spatial domain.
formal statement (Lean)
38inductive DiscretizationKind where
39 | spectralGalerkin
40 | finiteDifference
41deriving DecidableEq
42
43/-- A discrete dynamical model intended to approximate NS. -/