verifiedConstants
plain-language theorem explainer
This definition assembles the explicit list of verified constants for the CPM audit, recording K_net for cone and eight-tick cases, C_proj, C_eng, C_disp, the two c_min values, alphaLock, and phi together with their sources and exact flags. A researcher auditing Recognition Science derivations against self-similarity and fixed-point conditions would cite the list for provenance tracking. The definition proceeds by direct enumeration of each record using referenced constants such as alphaLock and phi.
Claim. The verified constants comprise the list of records: VerifiedConstant with name $K_{net}$ (cone), value 1, source ``Intrinsic cone projection'', exact true; $K_{net}$ (eight-tick) with value $(9/7)^2$; $C_{proj}$ with value 2; $C_{eng}$ with value 1; $C_{disp}$ with value 1; $c_{min}$ (cone) with value $1/2$; $c_{min}$ (eight-tick) with value $49/162$; the ILG exponent with value $(1-1/phi)/2$; and phi with value phi, each carrying its derivation source and exactness flag.
background
The CPM Constants Audit module supplies machine-checkable verification of constants derived from Recognition Science invariants. VerifiedConstant is the structure that records a constant by its string name, real value, derivation source string, and boolean exact flag. The module enables audit reports and consistency checks between projection methods. Upstream results supply alphaLock defined as $(1-1/phi)/2$ from self-similarity, the tick as the fundamental time quantum equal to 1, nucleosynthesis tiers that place densities on discrete phi-ladders, and ledger factorization that calibrates the J-cost function.
proof idea
This is a direct definition that enumerates the list of nine VerifiedConstant records. Each record hard-codes the name, the numerical value (computed from referenced constants such as alphaLock and phi), the source string, and the exact flag set to true. Numerical entries for c_min follow the product formula 1/(K_net · C_proj · C_eng). No lemmas or tactics beyond the structure constructor are applied.
why it matters
This definition supplies the data consumed by the audit_passes theorem, which asserts that generateAuditSummary reports verified status together with positive counts for constants and checks. It also feeds generateAuditSummary. Within the Recognition Science framework the list concretizes constants arising from the eight-tick octave and the self-similar fixed point phi, supporting verification inside the alpha band. It leaves open the quantitative coincidence probability addressed by the sibling cpmCoincidenceBound result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.