bridgeNormSq
plain-language theorem explainer
bridgeNormSq supplies a concrete CPMBridge instance for the discrete 2D Galerkin state at truncation level N. Researchers modeling incompressible flows with spectral truncations would cite it when embedding a finite-dimensional system into the CPM framework without introducing axioms. The definition is a one-line wrapper applying the general bridge constructor to the norm-squared hypothesis instance.
Claim. For each natural number $N$, let State$(N)$ be the discrete 2D Galerkin state space at truncation level $N$. Then bridgeNormSq$(N)$ is the CPMBridge instance obtained by packaging the model derived from the norm-squared hypothesis into the CPMBridge structure.
background
The CPM2D module instantiates the core CPM model from LawOfExistence for the finite-dimensional 2D Galerkin model. State is the abbrev for GalerkinState N, the discrete state type at truncation level N. CPMBridge is the structure containing a full Model (with A/B/C inequality proofs) together with defectMeaning and energyMeaning strings for traceability.
proof idea
This is a one-line wrapper that applies the bridge constructor to the hypothesisNormSq instance for the given N.
why it matters
This definition supplies a minimal concrete CPM bridge for the 2D Galerkin truncation in the ClassicalBridge.Fluids.CPM2D module (milestone M4). It packages the model from hypothesisNormSq so that downstream theorems can state explicit dependencies without axioms or sorry. The module doc notes that nontrivial analytic inequalities for fluids remain unproved here and are instead packaged in the Hypothesis structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.