`exampleCertificates`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.CPM.ConstantsAudit on GitHub at line 151.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 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 -/
 171  numConstants : ℕ
 172  /-- Number of consistency checks passed -/
 173  consistencyChecks : ℕ
 174  /-- Number of examples exercised in this audit -/
 175  numExamples : ℕ
 176  /-- Coincidence probability bound -/
 177  coincidenceProb : ℝ
 178  /-- Overall status -/
 179  status : String
 180
 181/-- Generate the audit summary. -/

papers checked against this theorem

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