pith. machine review for the scientific record. sign in
structure definition def or abbrev

Model

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  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. -/

used by (40)

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

… and 10 more

depends on (24)

Lean names referenced from this declaration's body.