Functionals

formal source

  26abbrev State (N : ℕ) : Type := GalerkinState N
  27
  28/-- The four CPM functionals required by `CPM.LawOfExistence.Model`. -/
  29structure Functionals (N : ℕ) where
  30  defectMass : State N → ℝ
  31  orthoMass  : State N → ℝ
  32  energyGap  : State N → ℝ
  33  tests      : State N → ℝ
  34
  35/-- Hypothesis bundle: a CPM instance for `GalerkinState N`.
  36
  37This is *exactly* the data needed to build a `CPM.LawOfExistence.Model`.
  38-/
  39structure Hypothesis (N : ℕ) where
  40  C : Constants
  41  F : Functionals N
  42  /- Projection-Defect (A): D ≤ K_net · C_proj · ||proj_{S⊥}||² -/
  43  projection_defect : ∀ a : State N, F.defectMass a ≤ C.Knet * C.Cproj * F.orthoMass a
  44  /- Energy control (B): ||proj_{S⊥}||² ≤ C_eng · (E−E₀) -/
  45  energy_control    : ∀ a : State N, F.orthoMass a ≤ C.Ceng * F.energyGap a
  46  /- Dispersion/interface (C): ||proj_{S⊥}||² ≤ C_disp · sup tests -/
  47  dispersion        : ∀ a : State N, F.orthoMass a ≤ C.Cdisp * F.tests a
  48
  49/-- Build a CPM `Model` from the hypothesis bundle. -/
  50noncomputable def model {N : ℕ} (H : Hypothesis N) : Model (State N) :=
  51  { C := H.C
  52    defectMass := H.F.defectMass
  53    orthoMass  := H.F.orthoMass
  54    energyGap  := H.F.energyGap
  55    tests      := H.F.tests
  56    projection_defect := H.projection_defect
  57    energy_control    := H.energy_control
  58    dispersion        := H.dispersion }
  59