exampleCertificates
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.