audit_passes
plain-language theorem explainer
The theorem confirms that the generated audit summary for CPM constants reports VERIFIED status together with strictly positive counts for both the number of constants and the consistency checks. A researcher auditing Recognition Science derivations would cite this result to close the machine-checked verification of constants against the invariants. The proof is a short term-mode reduction that applies simplification to the audit summary definition and the verified constants list, then resolves the inequalities by numerical normalization.
Claim. Let $S$ be the audit summary constructed from the list of verified CPM constants. Then $S$ has status equal to VERIFIED, the number of constants in $S$ is positive, and the number of consistency checks in $S$ is positive.
background
The CPM Constants Audit module supplies machine-checkable verification that constants satisfy the required properties derived from Recognition Science invariants, including consistency checks between cone and eight-tick sets and export of audit reports. VerifiedConstant is the structure that records each constant by name, numerical value, derivation source, and exactness flag. The list verifiedConstants enumerates the concrete entries, among them K_net for the cone projection and K_net for the eight-tick case. Upstream, RSNativeUnits.status records the base units with $c=1$, coherence quantum $φ^{-5}$, action quantum $ħ=φ^{-5}$, and the $φ$-ladder. The definition generateAuditSummary assembles the summary by taking the length of verifiedConstants for the constant count, fixing two consistency checks, and setting status to VERIFIED.
proof idea
The term-mode proof opens with a refine that splits the conjunction into three goals. The first goal is closed by reflexivity. The remaining two goals are discharged by simp on the definitions of generateAuditSummary and verifiedConstants, followed by norm_num to evaluate the list lengths and the fixed consistency-check count.
why it matters
This proved result closes the audit verification for constants derived from Recognition Science, confirming that the summary meets the stated criteria. It supports the broader CPM audit infrastructure that checks agreement with the eight-tick octave and cone projections. Within the framework it aligns with the forcing chain steps that fix $D=3$ and the $φ$-ladder mass formula, though it does not itself derive new constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.