`ExampleCertificate`

definition

show as: view math explainer →

module: IndisputableMonolith.CPM.ConstantsAudit
domain: CPM
line: 140 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.CPM.ConstantsAudit on GitHub at line 140.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 137/-! ## Example Witnesses (Standalone) -/
 138
 139/-- Record of an example where CPM constants/constraints are exercised. -/
 140structure ExampleCertificate where
 141  /-- Example name -/
 142  example : String
 143  /-- K_net value in this example -/
 144  Knet : ℝ
 145  /-- C_proj value in this example -/
 146  Cproj : ℝ
 147  /-- Reference for the implementation -/
 148  reference : String
 149
 150/-- Example certificates included in the standalone CPM audit. -/
 151noncomputable def exampleCertificates : List ExampleCertificate := [
 152  { example := "ToyModel",
 153    Knet := 1,
 154    Cproj := 2.0,
 155    reference := "URCGenerators/CPMMethodCert.lean (toyModel)" }
 156]
 157
 158/-- All examples in `exampleCertificates` use C_proj = 2. -/
 159theorem all_examples_cproj_two_statement :
 160    ∀ e ∈ exampleCertificates, e.Cproj = 2.0 := by
 161  intro e he
 162  simp [exampleCertificates] at he
 163  rcases he with rfl
 164  rfl
 165
 166/-! ## Audit Report Generation -/
 167
 168/-- Summary of the CPM constants audit. -/
 169structure AuditSummary where
 170  /-- Total number of verified constants -/

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.