Pith. sign in
module module high

IndisputableMonolith.CPM.LawOfExistence

show as:
view Lean formalization →

The LawOfExistence module bundles abstract constants and inequalities for the Coercive Projection Method core. Fluids and gravity bridge modules cite it to supply the domain-agnostic interface before adding state types and functionals. It is a definition module whose structure is fixed by sibling declarations for cmin, Model, and defect bounds.

claimThe abstract CPM model supplies constants satisfying $c_{\min}>0$ together with the inequalities defect $\le$ constants $\times$ energyGap and energyGap $\ge c_{\min}\times$ defect, plus cone projections $K_{\rm net}=1$, $C_{\rm proj}=2$.

background

The module imports IndisputableMonolith.Cost, whose J-cost functional supplies the underlying symmetry and convexity axioms. It introduces the Model structure together with coneConstants, cmin, and the defect-energyGap inequalities listed among its siblings. The local setting is the domain-agnostic CPM core that downstream files instantiate with concrete defectMass, orthoMass, and test functionals.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

This module is the CPM core that feeds IndisputableMonolith.ClassicalBridge.Fluids.CPM and CPM2D for Navier-Stokes and 2D Galerkin models, CostUniqueness for the T5 uniqueness theorem, ConstantsAudit for invariant verification, and ILG.CPMInstance for gravitational modifications. It supplies the abstract constants required by the Recognition Science forcing chain before domain-specific hypotheses are added.

scope and limits

used by (7)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (29)