bridge
plain-language theorem explainer
The declaration constructs a CPMBridge instance by packaging a Hypothesis bundle for the N-level Galerkin state into the model with attached interpretation strings. Researchers working on 2D fluid approximations in Recognition Science would cite this to instantiate the CPM core without carrying open hypotheses downstream. The construction is a direct record update that applies the model function to H and populates the meaning fields for traceability.
Claim. Given a hypothesis bundle $H$ consisting of constants $C$, functionals $F$, and the three inequalities (projection defect, energy control, dispersion) for the Galerkin state at level $N$, define bridge$(H)$ to be the CPMBridge structure whose model component is the packaged Model from $H$, with defectMeaning, energyMeaning, and testsMeaning set to descriptive strings about Galerkin2D quantities.
background
In the CPM2D module the Hypothesis structure bundles the data needed to build a Model from CPM.LawOfExistence: constants $C$, functionals $F$ for the GalerkinState $N$, and the three inequalities A/B/C that control projection defects, energy gaps, and dispersion. The State is simply the GalerkinState $N$. The CPMBridge structure from the CPM module holds the Model together with human-readable notes for traceability. This setup allows the nontrivial analytic inequalities for fluids to be stated explicitly as hypotheses rather than axioms.
proof idea
The definition is a direct record constructor that sets model to the result of applying model to H, and populates the three meaning strings with descriptions of the Galerkin2D defectMass, energyGap, and tests.
why it matters
This definition provides a concrete instantiation of the CPMBridge that downstream modules such as Action.EulerLagrange.geodesic_iff_hessianEnergy_EL and Action.QuadraticLimit.newton_first_law can use without depending on the Hypothesis structure. It fills the role of a base instance in the classical bridge for fluids, as noted in the module documentation, enabling reduction of the hypothesis layer for minimal models. It touches the open question of proving the full A/B/C inequalities for physically meaningful fluid CPM.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.