module module high

`IndisputableMonolith.CPM.LawOfExistence`

This module supplies the abstract constants and inequality scaffolding for the Coercive Projection Model. Fluids and gravitational modelers cite it when they need a domain-agnostic interface before supplying concrete defectMass, orthoMass and energyGap functionals. The module consists of definitions and short lemmas that package the minimal requirements without proving analytic estimates.

claimBundle of CPM constants $c_0, c_1, c_2$ together with the abstract Model type and the inequalities defectMass$(x) le c_0 cdot$ energyGap$(x)$ and orthoMass$(x) le c_1 cdot$ energyGap$(x)$ for all states $x$.

background

The module imports the Cost namespace, which supplies the J-cost functional $J(x) = (x + x^{-1})/2 - 1$ and the associated defect and orthogonality measures. CPM abstracts the Law of Existence by requiring a state space equipped with three functionals (defectMass, orthoMass, energyGap) and a finite set of tests that certify the projection property. The sibling declarations Constants, cmin and Model encode the numerical bounds and the abstract carrier type; the lemmas defect_le_constants_mul_energyGap and energyGap_ge_cmin_mul_defect state the two-sided coercivity relations that downstream instantiations must verify.

proof idea

This is a definition module, no proofs. It assembles named constants and inequality statements whose bodies are either direct definitions or one-line wrappers around the imported Cost primitives.

why it matters in Recognition Science

The module is the single source of truth for the abstract CPM interface that every concrete bridge (ClassicalBridge.Fluids.CPM, CPM2D, ILG.CPMInstance) must import and instantiate. It supplies the constant framework referenced by CostUniqueness (T5) and by the ConstantsAudit verification. The structure therefore closes the gap between the Recognition Science forcing chain and domain-specific applications without embedding any particular physics.

scope and limits

Does not prove the analytic inequalities required for any concrete Navier-Stokes or gravitational model.
Does not derive the numerical values of the constants from the phi-ladder or Recognition Science axioms.
Does not contain numerical checks or example data.
Does not define a state type or the concrete functionals defectMass and energyGap.

used by (7)

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

IndisputableMonolith.ClassicalBridge.Fluids.CPM module_import
IndisputableMonolith.ClassicalBridge.Fluids.CPM2D module_import
IndisputableMonolith.CostUniqueness module_import
IndisputableMonolith.CPM.ConstantsAudit module_import
IndisputableMonolith.CPM.Examples module_import
IndisputableMonolith.ILG.CPMInstance module_import
IndisputableMonolith.URCGenerators.CPMMethodCert module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import

declarations in this module (29)

structure Constants L31
def cmin L44
lemma cmin_pos L47
structure Model L69
theorem defect_le_constants_mul_energyGap L91
theorem energyGap_ge_cmin_mul_defect L111
theorem defect_le_constants_mul_tests L136
lemma defect_le_ortho_of_Knet_one_Cproj_one L162
lemma defect_eq_ortho_of_subspace_case L171
def coneConstants L206
lemma cone_Knet_eq_one L217
lemma cone_Cproj_eq_two L218
lemma cone_Ceng_eq_one L219
lemma cone_Cdisp_eq_one L220
lemma Jcost_log_second_deriv_normalized L224
theorem cproj_eq_two_from_J_normalization L280
theorem cproj_from_J_second_deriv L300
theorem knet_from_cone_projection L312
def knet_from_covering L320
theorem knet_eight_tick L324
def knet_eight_tick_refined L329
theorem knet_eight_tick_refined_value L331
def eightTickConstants L336
theorem c_value_eight_tick L348
theorem c_value_derivation L354
theorem c_value_cone L359
structure CPMConstantsRecord L371
def rsConeRecord L390
def eightTickRecord L402