all_examples_cproj_two_statement
plain-language theorem explainer
The theorem asserts that every entry in the exampleCertificates list has projection constant exactly 2. Auditors verifying CPM constants against Recognition Science invariants would cite this to confirm the toy model satisfies the required projection. The proof is a direct case analysis that unfolds the singleton list definition and matches the constant value by reflexivity.
Claim. For every example certificate $e$ in the list of verified examples, the projection constant $C_ {proj}(e) = 2$.
background
The CPM Constants Audit module supplies machine-checkable verification of constants derived from Recognition Science invariants, including consistency checks between constant sets and export of audit reports. The exampleCertificates definition supplies a concrete list containing one toy-model entry with Knet = 1 and Cproj = 2.0, referenced from URCGenerators. Upstream results such as the nuclear-density tiers in NucleosynthesisTiers and the J-cost structure in LedgerFactorization supply the physical context in which these projection constants appear.
proof idea
The term proof binds the element and membership hypothesis, simplifies the list definition to expose the single constructor, performs case analysis that yields reflexivity, and concludes by reflexivity.
why it matters
The result is invoked by generateJSONReport to guarantee the projection value appears in the exported audit output. It completes the toy-model verification step inside the CPM audit, consistent with the framework's requirement that constants satisfy the eight-tick octave and phi-ladder relations. No open scaffolding questions are addressed by this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.