DiscretizationKind
plain-language theorem explainer
DiscretizationKind enumerates the two families of spatial discretization available for discrete Navier-Stokes approximations. Researchers building the fluids bridge cite it when tagging a DiscreteModel instance. The declaration is a plain inductive definition with two constructors that derives decidable equality.
Claim. An inductive type whose constructors are the spectral Galerkin method and the finite difference method, equipped with decidable equality.
background
The module supplies a minimal interface for discrete Navier-Stokes models that later connect to LNAL execution semantics and CPM defect/energy structures. It explicitly postpones any choice between Galerkin and grid discretizations. Upstream definitions include the model constructor from a hypothesis bundle in CPM2D and the active-edge count A appearing in integration-gap and mass-anchor files.
proof idea
The declaration is an inductive definition introducing two constructors and deriving DecidableEq; no lemmas are applied.
why it matters
It supplies the kind field inside the DiscreteModel structure, allowing downstream files to instantiate concrete approximations while remaining compatible with the Recognition framework's CPM and modal actualization components. The module doc-comment states the intent to relate such models to LNAL and CPM without committing to one discretization family.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.