Model
plain-language theorem explainer
The Model structure packages the three core CPM inequalities over an arbitrary type β by bundling a constants record with four real-valued functionals and the projection-defect, energy-control, and dispersion bounds. Researchers building fluid or astrophysical models cite it when they need a domain-agnostic container for A/B/C coercivity assumptions before specializing the maps. The declaration is a pure record definition with an empty body and no proof obligations.
Claim. Let β be any type. A CPM model consists of a constants bundle C = (K_net, C_proj, C_eng, C_disp) with all components nonnegative, together with functionals defectMass, orthoMass, energyGap, tests : β → ℝ satisfying, for every a ∈ β: defectMass(a) ≤ K_net ⋅ C_proj ⋅ orthoMass(a), orthoMass(a) ≤ C_eng ⋅ energyGap(a), and orthoMass(a) ≤ C_disp ⋅ tests(a).
background
The module formalizes the Coercive Projection Method in three abstract parts: A encodes the projection-defect inequality, B the energy-gap control of orthogonal mass, and C the dispersion bound via local tests. The sibling Constants structure supplies the four nonnegative scaling parameters Knet, Cproj, Ceng, Cdisp that appear in those inequalities. The four functionals defectMass, orthoMass, energyGap, and tests are interpreted as aggregate squared distance to structure, mass of the orthogonal component, gap above the reference energy, and supremum of dispersion tests, respectively. This level of abstraction lets concrete instances in fluids or nucleosynthesis supply their own maps without importing measure-theoretic scaffolding. Upstream structures such as LedgerFactorization calibrate the underlying J-cost that motivates the constant choices.
proof idea
The declaration is a structure definition whose body is empty; it simply records the three inequalities as named fields of the record. No lemmas are invoked and no tactics are executed.
why it matters
Model is the central interface that downstream modules instantiate: CPMBridge packages it for classical fluids, while CPM2D.model and Hypothesis build concrete 2D Galerkin instances directly from it. It supplies the abstract A/B/C logic required by the Law of Existence module and feeds coercivity arguments used in stellar assembly and dark-energy calculations. Within Recognition Science it closes the generic coercivity step that links phi-ladder constants to existence statements, leaving open only the specialization of the functionals to particular physical systems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.