CPMBridge
plain-language theorem explainer
CPMBridge packages a Model instance for a given state type together with traceability strings for defect, energy, and test interpretations. Researchers bridging Recognition Science to discrete Navier-Stokes would cite it when instantiating the domain-agnostic CPM core with Galerkin states. The definition is a direct record constructor that takes a Model and supplies empty-string defaults for the annotation fields.
Claim. A structure $CPMBridge(β)$ consisting of a field $model : Model(β)$ together with optional string annotations $defectMeaning$, $energyMeaning$, and $testsMeaning$ (defaulting to the empty string).
background
The CPM core (from LawOfExistence) supplies a domain-agnostic structure Model(β) that bundles constants C with four functionals: defectMass, orthoMass, energyGap, and tests on states of type β. This module provides a minimal carrier for Navier-Stokes instantiations, where the state type is the discrete 2D GalerkinState N from CPM2D. Upstream, CPM2D.model constructs such a Model from a Hypothesis bundle, while the local module doc states that the CPM core must be instantiated with concrete functionals and the A/B/C inequality proofs for fluid use.
proof idea
The declaration is a structure definition that directly assembles the record: the model field is supplied by an upstream Model construction and the three meaning fields receive default empty strings. No lemmas or tactics are invoked; it functions as a packaging wrapper for traceability.
why it matters
It supplies the reusable carrier needed by downstream bridge specifications such as RSNSBridgeSpec and the concrete bridge and bridgeNormSq definitions in CPM2D. The structure closes the interface gap between the domain-agnostic LawOfExistence.Model and the discrete fluid setting, supporting the Recognition framework's passage from universal forcing to classical Navier-Stokes via the eight-tick octave and phi-ladder mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.