exampleCertificates
The definition supplies a list of ExampleCertificate records for the standalone CPM constants audit in Recognition Science. It contains one entry drawn from the toyModel, recording K_net = 1 and C_proj = 2.0 together with its provenance string. Researchers running the audit executable or citing the projection bound would reference this list to populate summary reports. The construction is a direct noncomputable list literal with no further reduction.
claimLet $E$ be the list containing the single record with fields example = ``ToyModel'', $K_{net} = 1$, $C_{proj} = 2.0$, and reference = ``URCGenerators/CPMMethodCert.lean (toyModel)''. Each record is an instance of the structure whose fields are a string name, real values for $K_{net}$ and $C_{proj}$, and a provenance string.
background
The CPM Constants Audit module supplies machine-checkable verification that constants derived from Recognition Science invariants satisfy the required properties, including consistency between different constant sets and probability bounds for coincidental agreement. ExampleCertificate is the structure that records an example name, the value of $K_{net}$, the value of $C_{proj}$, and a reference string to the source implementation. Upstream, $C_{proj}$ is the rational constant 2 that bounds the operator norm of the ILG projection kernel, while toyModel is the small consistency witness in which all functionals are set to the constant 1 and the inequalities hold numerically with $K_{net}=1$, $C_{proj}=2$.
proof idea
The definition is a direct list literal that constructs a single ExampleCertificate by hard-coding the four fields from the toyModel witness. No lemmas are invoked and no tactics are used; the body is simply the list containing the record with example := ``ToyModel'', Knet := 1, Cproj := 2.0, and the given reference string.
why it matters in Recognition Science
This definition supplies the data consumed by the theorem all_examples_cproj_two_statement, which asserts that every entry satisfies $C_{proj}=2.0$, and by generateAuditSummary, which reports the number of examples together with the coincidence probability. It forms part of the export infrastructure for audit reports that verify CPM constants against Recognition Science invariants, in particular the projection bound $C_{proj}=2$ and the eight-tick octave structure. It touches the open question of how many nontrivial examples are required to strengthen the overall audit.
scope and limits
- Does not establish physical validity of the toy model values.
- Does not include certificates drawn from actual physical derivations.
- Does not verify the underlying functional inequalities inside the model.
- Does not extend the list to other constant sets beyond the single entry.
Lean usage
theorem all_cproj_two : ∀ e ∈ exampleCertificates, e.Cproj = 2.0 := by intro e he; simp [exampleCertificates] at he; rcases he with rfl; rflformal statement (Lean)
151noncomputable def exampleCertificates : List ExampleCertificate := [
proof body
Definition body.
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. -/