toyModel_cmin_pos

proof body

Tactic-mode proof.

  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 ?_ ?_))
  91  · intro β M a
  92    exact IndisputableMonolith.CPM.LawOfExistence.Model.defect_le_constants_mul_energyGap (M:=M) a
  93  · intro β M hpos a
  94    exact IndisputableMonolith.CPM.LawOfExistence.Model.energyGap_ge_cmin_mul_defect (M:=M) hpos a
  95  · intro β M a
  96    exact IndisputableMonolith.CPM.LawOfExistence.Model.defect_le_constants_mul_tests (M:=M) a
  97  · refine ⟨toyModel, toyModel_defect_pos, toyModel_energy_pos, toyModel_cmin_pos⟩
  98
  99end URCGenerators
 100end IndisputableMonolith