`Model`

definition

show as: view math explainer →

module: IndisputableMonolith.CPM.LawOfExistence
domain: CPM
line: 69 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.CPM.LawOfExistence on GitHub at line 69.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  66
  67The CPM assumptions are encoded as inequalities between these. -/
  68
  69structure Model (β : Type) where
  70  C          : Constants
  71  defectMass : β → ℝ
  72  orthoMass  : β → ℝ
  73  energyGap  : β → ℝ
  74  tests      : β → ℝ
  75  /- Projection-Defect (A): D ≤ K_net · C_proj · ||proj_{S⊥}||^2 -/
  76  projection_defect : ∀ a : β, defectMass a ≤ C.Knet * C.Cproj * orthoMass a
  77  /- Energy control: ||proj_{S⊥}||^2 ≤ C_eng · (E-E_0) -/
  78  energy_control    : ∀ a : β, orthoMass a ≤ C.Ceng * energyGap a
  79  /- Dispersion/interface: ||proj_{S⊥}||^2 ≤ C_disp · sup tests -/
  80  dispersion        : ∀ a : β, orthoMass a ≤ C.Cdisp * tests a
  81
  82namespace Model
  83
  84variable {β : Type}
  85
  86/-- (AB) Coercivity link: `D ≤ (K_net·C_proj·C_eng) · (E−E_0)`.
  87
  88This is the forward direction combining A + energy control.
  89We deliberately avoid dividing by the product, to keep sign issues out
  90of the core inequality. -/
  91theorem defect_le_constants_mul_energyGap
  92  (M : Model β) (a : β) :
  93  M.defectMass a ≤ (M.C.Knet * M.C.Cproj * M.C.Ceng) * M.energyGap a := by
  94  have hA : M.defectMass a ≤ M.C.Knet * M.C.Cproj * M.orthoMass a :=
  95    M.projection_defect a
  96  have hB : M.orthoMass a ≤ M.C.Ceng * M.energyGap a :=
  97    M.energy_control a
  98  calc M.defectMass a
  99      ≤ M.C.Knet * M.C.Cproj * M.orthoMass a := hA

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.