printSummary
plain-language theorem explainer
This definition outputs a fixed formatted report summarizing the CPM constants audit, stating nine verified constants, four consistency checks passed, one example witness, and coincidence probability below 10^{-12}, ending with a verified status banner. It is invoked by the main CLI entry point to display results when running the audit tool. The implementation is a direct sequence of IO.println statements emitting the hardcoded text with no runtime computation or external calls.
Claim. The procedure that emits to standard output the audit summary block containing the counts of verified constants (9), passed consistency checks (4), example witnesses (1), and coincidence probability bound ($<10^{-12}$), followed by the verification status banner.
background
The module implements a command-line interface for auditing CPM constants derived from the Recognition Science framework. Upstream results supply probability definitions: QuantumLedger.probability computes the Born-rule probability as the squared norm of quantum state amplitudes; SMatrixUnitarity.probability gives the transition probability as the squared modulus of S-matrix elements; BoltzmannDistribution.probability yields the normalized Boltzmann factor for system levels. The local setting is the CPM audit CLI invoked via lake exe cpm_audit, which prints summaries of verified constants, consistency checks, and probability bounds for coincidental agreement.
proof idea
The definition is a direct do-block containing sequential IO.println calls that emit the header, the four summary lines with hardcoded numeric values, the status banner, and trailing newlines. No lemmas or upstream probability functions are invoked; the output strings are literal.
why it matters
This definition supplies the terminal summary output for the CPM audit CLI and is invoked from the main entry point. It reports the verification status of constants obtained from the forcing chain (T5 J-uniqueness, T6 phi fixed point, T7 eight-tick octave) and the Recognition Composition Law, closing the audit with the low coincidence probability bound. It thereby documents the framework's claim that the functional equation reproduces the observed constants without external tuning.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.