toyModel_energy_pos

formal source

  57lemma toyModel_defect_pos : toyModel.defectMass () > 0 := by
  58  simp [toyModel]
  59
  60lemma toyModel_energy_pos : toyModel.energyGap () > 0 := by
  61  simp [toyModel]
  62
  63lemma toyModel_cmin_pos : 0 < cmin toyModel.C := by
  64  have hpos : 0 < toyModel.C.Knet ∧ 0 < toyModel.C.Cproj ∧ 0 < toyModel.C.Ceng := by
  65    simp [toyModel]
  66  simpa using (IndisputableMonolith.CPM.LawOfExistence.cmin_pos (C:=toyModel.C) hpos)
  67
  68/-- Verification predicate for the standalone CPM method certificate.
  69
  70It asserts the generic A/B/C consequences (for any CPM model) and includes a
  71concrete toy model witness to avoid vacuity.
  72-/
  73@[simp] def CPMMethodCert.verified (_c : CPMMethodCert) : Prop :=
  74  (∀ {β : Type} (M : Model β) (a : β),
  75      M.defectMass a ≤ (M.C.Knet * M.C.Cproj * M.C.Ceng) * M.energyGap a)
  76  ∧
  77  (∀ {β : Type} (M : Model β)
  78      (_hpos : 0 < M.C.Knet ∧ 0 < M.C.Cproj ∧ 0 < M.C.Ceng) (a : β),
  79      M.energyGap a ≥ cmin M.C * M.defectMass a)
  80  ∧
  81  (∀ {β : Type} (M : Model β) (a : β),
  82      M.defectMass a ≤ (M.C.Knet * M.C.Cproj * M.C.Cdisp) * M.tests a)
  83  ∧
  84  (∃ toy : Model Unit,
  85      toy.defectMass () > 0 ∧ toy.energyGap () > 0 ∧ 0 < cmin toy.C)
  86
  87/-- The standalone CPM method certificate verifies. -/
  88@[simp] theorem CPMMethodCert.verified_any (c : CPMMethodCert) :
  89    CPMMethodCert.verified c := by
  90  refine And.intro ?_ (And.intro ?_ (And.intro ?_ ?_))