State
plain-language theorem explainer
State aliases the discrete 2D Galerkin velocity space at truncation N as the Euclidean space over modes times two components. Spectral fluid modelers and Recognition Science users instantiating CPM.LawOfExistence.Model for 2D flows cite this alias when building bridges. The definition is a direct one-line type abbreviation with no added structure or obligations.
Claim. Let $S_N$ denote the finite-dimensional space of discrete 2D velocity fields at Galerkin truncation level $N$, realized as the Euclidean space over the product of the mode index set and two vector components.
background
The CPM2D module instantiates the CPM core (LawOfExistence.Model) for the finite-dimensional 2D Galerkin model. GalerkinState supplies the underlying type: EuclideanSpace ℝ ((modes N) × Fin 2), the space of velocity coefficients per truncated mode and component. The module explicitly packages required analytic inequalities into a separate Hypothesis structure rather than using axioms.
proof idea
One-line type abbreviation that directly re-exports GalerkinState N.
why it matters
This alias supplies the concrete state type for the CPMBridge, model, and bridgeNormSq definitions inside CPM2D, which in turn feed the OctaveLoop structure in CoherenceTechnology and the RSNSBridgeSpec. It advances milestone M4 by providing a traceable state for the LawOfExistence.Model without embedding full fluids inequalities. The construction supports the Recognition framework's discrete approximation path while keeping analytic gaps explicit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.