Cpm Law Of Existence Defect Le Constants Mul Energy Gap

The defect-energy bound

The Coercive Projection Method (CPM) is a general scheme for turning a local test into a global membership statement. The framework models a system as a ledger, a discrete record of events, and asks how much a candidate state deviates from the set of valid states. That deviation is the defect mass, a nonnegative real number assigned to each element of the model. The energy gap is the difference between the energy of a candidate state and the ground-state energy, also a nonnegative real number. The theorem defect_le_constants_mul_energyGap states that for any model and any element, the defect mass is at most the product of three constants (Knet, Cproj, Ceng) and the energy gap.

The proof is a composition of two inequalities that are part of the model structure. The first, projection_defect, bounds the defect mass by Knet times Cproj times the orthogonal mass, the mass of the component of the state that lies outside the valid subspace. The second, energy_control, bounds that orthogonal mass by Ceng times the energy gap. Multiplying these two bounds gives the theorem. The constants are part of the model definition, not derived in this file. The structure Constants records four nonnegative constants, and the theorem uses three of them. The fourth constant, Cdisp, appears in a companion inequality that bounds the orthogonal mass by a dispersion term instead of an energy gap.

The theorem is a formal statement in the machine-checked library of formal theorems. Its proof is a direct combination of the two axioms of the model structure, so it is a theorem in the strict sense: it follows from the definitions and the model axioms. The theorem does not fix the values of the constants. It holds for any choice of nonnegative constants. The specific values, such as Knet = 1 and Cproj = 2 for the cone model, or Knet = (9/7)^2 for the eight-tick model, are recorded in separate definitions and theorems. The theorem also does not say that the energy gap is positive; it only says that the defect mass is bounded above by a multiple of the energy gap. If the energy gap is zero, the bound forces the defect mass to be zero when the constants are positive.

In Recognition Science, the theorem is one of three parts of the Law of Existence. Part A is the projection-defect inequality, part B is the coercivity factorization that the energy gap controls the defect, and part C is the aggregation principle that local tests imply membership. The theorem is part B. It is a structural statement about the model, not a physical law by itself. It becomes physical when a concrete model supplies the constants and the energy function. The theorem guarantees that, in any such model, the defect cannot grow without bound relative to the energy gap, which is the sense in which the energy gap controls the defect.

/-- (AB) Coercivity link: `D ≤ (K_net·C_proj·C_eng) · (E−E_0)`.

This is the forward direction combining A + energy control.
We deliberately avoid dividing by the product, to keep sign issues out
of the core inequality. -/
theorem defect_le_constants_mul_energyGap
  (M : Model β) (a : β) :
  M.defectMass a ≤ (M.C.Knet * M.C.Cproj * M.C.Ceng) * M.energyGap a := by
  have hA : M.defectMass a ≤ M.C.Knet * M.C.Cproj * M.orthoMass a :=
    M.projection_defect a
  have hB : M.orthoMass a ≤ M.C.Ceng * M.energyGap a :=
    M.energy_control a
  calc M.defectMass a
      ≤ M.C.Knet * M.C.Cproj * M.orthoMass a := hA
    _ ≤ M.C.Knet * M.C.Cproj * (M.C.Ceng * M.energyGap a) := by
        apply mul_le_mul_of_nonneg_left hB
        have h₁ : 0 ≤ M.C.Knet := M.C.Knet_nonneg
        have h₂ : 0 ≤ M.C.Cproj := M.C.Cproj_nonneg
        exact mul_nonneg h₁ h₂
    _ = (M.C.Knet * M.C.Cproj * M.C.Ceng) * M.energyGap a := by ring

/-- (AB) Coercivity link: `D ≤ (K_net·C_proj·C_eng) · (E−E_0)`.

This is the forward direction combining A + energy control.
We deliberately avoid dividing by the product, to keep sign issues out
of the core inequality. -/
theorem defect_le_constants_mul_energyGap
  (M : Model β) (a : β) :
  M.defectMass a ≤ (M.C.Knet * M.C.Cproj * M.C.Ceng) * M.energyGap a := by
  have hA : M.defectMass a ≤ M.C.Knet * M.C.Cproj * M.orthoMass a :=
    M.projection_defect a
  have hB : M.orthoMass a ≤ M.C.Ceng * M.energyGap a :=
    M.energy_control a
  calc M.defectMass a
      ≤ M.C.Knet * M.C.Cproj * M.orthoMass a := hA
    _ ≤ M.C.Knet * M.C.Cproj * (M.C.Ceng * M.energyGap a) := by
        apply mul_le_mul_of_nonneg_left hB
        have h₁ : 0 ≤ M.C.Knet := M.C.Knet_nonneg
        have h₂ : 0 ≤ M.C.Cproj := M.C.Cproj_nonneg
        exact mul_nonneg h₁ h₂
    _ = (M.C.Knet * M.C.Cproj * M.C.Ceng) * M.energyGap a := by ring

structure Model (β : Type) where
  C          : Constants
  defectMass : β → ℝ
  orthoMass  : β → ℝ
  energyGap  : β → ℝ
  tests      : β → ℝ
  /- Projection-Defect (A): D ≤ K_net · C_proj · ||proj_{S⊥}||^2 -/
  projection_defect : ∀ a : β, defectMass a ≤ C.Knet * C.Cproj * orthoMass a
  /- Energy control: ||proj_{S⊥}||^2 ≤ C_eng · (E-E_0) -/
  energy_control    : ∀ a : β, orthoMass a ≤ C.Ceng * energyGap a
  /- Dispersion/interface: ||proj_{S⊥}||^2 ≤ C_disp · sup tests -/
  dispersion        : ∀ a : β, orthoMass a ≤ C.Cdisp * tests a

What this page does not claim

The theorem does not fix the numerical values of the constants Knet, Cproj, and Ceng. The theorem does not assert that the energy gap is positive. The theorem does not establish any physical law without a concrete model supplying the constants and energy function.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/CPM/LawOfExistence.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: