IndisputableMonolith.URCAdapters.CPMReports

   1import Mathlib
   2import IndisputableMonolith.URCGenerators.CPMMethodCert
   3
   4/-!
   5# URC Adapters: CPM Method Reports (Standalone)
   6
   7This module provides simple, machine-readable checks and pretty printers
   8to audit the standalone CPM method certificate (generic A/B/C + toy-model witness).
   9-/
  10
  11namespace IndisputableMonolith
  12namespace URCAdapters
  13namespace CPMReports
  14
  15open IndisputableMonolith.URCGenerators
  16
  17/-- A #eval-friendly report confirming the standalone CPM method certificate. -/
  18noncomputable def methodReport : String :=
  19  let cert : URCGenerators.CPMMethodCert := {}
  20  have _ : URCGenerators.CPMMethodCert.verified cert :=
  21    URCGenerators.CPMMethodCert.verified_any cert
  22  -- Also force evaluation of the toy witness facts.
  23  let _ := URCGenerators.toyModel_defect_pos
  24  let _ := URCGenerators.toyModel_energy_pos
  25  let _ := URCGenerators.toyModel_cmin_pos
  26  "CPM Method Report: OK"
  27
  28@[simp] noncomputable def methodReport_ok : String := methodReport
  29
  30end CPMReports
  31end URCAdapters
  32end IndisputableMonolith
  33