cmin

formal source

  41/-- Coercivity constant `c_min = 1 / (K_net · C_proj · C_eng)`.
  42
  43We keep it as a definition (not a field) to avoid duplication. -/
  44@[simp] noncomputable def cmin (C : Constants) : ℝ := (C.Knet * C.Cproj * C.Ceng)⁻¹
  45
  46/-- If all three constants are strictly positive, then `cmin > 0`. -/
  47lemma cmin_pos (C : Constants)
  48  (hpos : 0 < C.Knet ∧ 0 < C.Cproj ∧ 0 < C.Ceng) :
  49  0 < cmin C := by
  50  have hprodpos : 0 < (C.Knet * C.Cproj * C.Ceng) := by
  51    have := mul_pos (mul_pos hpos.1 hpos.2.1) hpos.2.2
  52    simpa [mul_assoc] using this
  53  have : 0 < (C.Knet * C.Cproj * C.Ceng)⁻¹ := by
  54    exact inv_pos.mpr hprodpos
  55  simpa [cmin] using this
  56
  57/-! ## Abstract CPM model (aggregate, domain-agnostic)
  58
  59We work with an abstract "state" type `β` (e.g., a field, a function,
  60or a configuration) and three nonnegative functionals:
  61
  62  - `defectMass : β → ℝ`  -- aggregate squared distance to structure
  63  - `orthoMass  : β → ℝ`  -- aggregate mass of the orthogonal component
  64  - `energyGap  : β → ℝ`  -- gap above the structured reference
  65  - `tests      : β → ℝ`  -- supremum over local/dispersion tests
  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      : β → ℝ