hypothesisNormSq
plain-language theorem explainer
Supplies a concrete CPM hypothesis for the N-point 2D Galerkin discretization by taking the all-ones constant bundle and squared-norm functionals. Numerical analysts working with discrete fluid models cite it to instantiate the Law of Existence without extra hypotheses. The definition assembles the record directly and discharges the three field conditions by simplification.
Claim. Define $H_N$ as the hypothesis structure for the Galerkin state space of dimension $N$, with constant bundle $C=(K_{net}=1,C_{proj}=1,C_{eng}=1,C_{disp}=1)$, functionals given by squared Euclidean norm for defect mass, orthogonal mass, energy gap and tests, and the three inequalities holding by direct substitution.
background
The CPM2D module instantiates the core CPM structure from LawOfExistence for the finite-dimensional 2D Galerkin model. The Hypothesis structure bundles a Constants tuple and a Functionals map together with three inequalities: projection defect bounds the defect mass by net and proj constants times ortho mass; energy control bounds ortho mass by eng constant times energy gap; dispersion bounds ortho mass by disp constant times test supremum. This file packages the nontrivial analytic inequalities explicitly so downstream theorems avoid axioms. Upstream, constantsOne provides the unit constants and functionalsNormSq defines all measurements via the squared norm on the state space.
proof idea
The definition constructs the Hypothesis record by assigning constantsOne to the C field and functionalsNormSq N to the F field. Each of the three required properties is discharged by a tactic that introduces the state variable and simplifies using the definitions of constantsOne and functionalsNormSq.
why it matters
This supplies the minimal hypothesis instance that feeds the bridgeNormSq construction, which in turn packages the Model for the CPM bridge. It fills the placeholder role in the M4 milestone for CPM2D, allowing traceability without proving the full fluid inequalities. In the Recognition framework it connects the discrete Galerkin setting to the Law of Existence, though the actual analytic bounds remain open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.