Hypothesis
plain-language theorem explainer
The Hypothesis structure for truncation level N bundles CPM constants C with four functionals F on Galerkin states and asserts three inequalities that bound defect mass by a multiple of orthogonal mass, orthogonal mass by energy gap, and orthogonal mass by test values. Researchers constructing continuum limits from 2D Galerkin approximations cite this bundle to record the precise analytic assumptions required by the CPM model. The declaration is a pure structure definition containing no proof obligations or computational content.
Claim. Let $C$ be a tuple of CPM constants and let $F$ map each Galerkin state $a$ at level $N$ to four real values (defect mass, orthogonal mass, energy gap, and test supremum). The structure asserts the three inequalities $F(a)_.defectMass ≤ C.Knet · C.Cproj · F(a)_.orthoMass$, $F(a)_.orthoMass ≤ C.Ceng · F(a)_.energyGap$, and $F(a)_.orthoMass ≤ C.Cdisp · F(a)_.tests$ for every state $a$.
background
The CPM2D module equips the finite-dimensional 2D Galerkin truncation of the Navier-Stokes equations with the abstract CPM framework. State is defined as the abbreviation GalerkinState N. Functionals supplies the four maps defectMass, orthoMass, energyGap and tests that are required by the Model structure imported from LawOfExistence. The local theoretical setting is the M4 milestone that packages the nontrivial analytic inequalities explicitly inside a Hypothesis structure so that downstream theorems can state their dependence without axioms or sorry. Upstream, the Constants structure from LawOfExistence supplies the four real parameters Knet, Cproj, Ceng and Cdisp together with the non-negativity of Knet.
proof idea
This declaration is a structure definition. It introduces the three fields projection_defect, energy_control and dispersion directly as the required inequalities on the functionals; no tactics or lemmas are applied.
why it matters
The Hypothesis structure supplies the exact data required to construct a CPM.Model via the model function and the CPMBridge via the bridge function in the same module. It is used downstream by ConvergenceHypothesis and several norm and Duhamel lemmas in ContinuumLimit2D, allowing those results to state their dependence on the three inequalities without axioms. Within the Recognition framework it realizes the packaging step of the CPM core for the 2D fluids bridge, keeping the analytic content of the continuum limit explicit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.