def
definition
methodReport
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.URCAdapters.CPMReports on GitHub at line 18.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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