theorem
proved
all_examples_cproj_two_statement
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.CPM.ConstantsAudit on GitHub at line 159.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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. -/
182noncomputable def generateAuditSummary : AuditSummary := {
183 numConstants := verifiedConstants.length,
184 consistencyChecks := 2, -- cone and eight-tick
185 numExamples := exampleCertificates.length,
186 coincidenceProb := cpmCoincidenceBound.probability,
187 status := "VERIFIED"
188}
189