printProbability
plain-language theorem explainer
The printProbability definition renders a CLI section declaring an upper bound of 10^{-12} on the probability that four independent CPM constants match RS predictions to three decimal places. Audit users running the cpm_audit executable reference this output to surface the negligible-coincidence result. The implementation is a fixed sequence of IO.println statements that embed the bound and verification marker.
Claim. The IO action that prints the probability bounds section, stating that the coincidence probability for four independent constants at three decimal places satisfies $p < 10^{-12}$, with the marker confirming coincidence_negligible.
background
The CPM.AuditMain module supplies a command-line interface for auditing CPM constants against Recognition Science predictions. Its module documentation states that the tool prints a summary of verified constants, consistency checks, and probability bounds for coincidental agreement. The section relies on the upstream theorem coincidence_negligible, which proves cpmCoincidenceBound.probability < 10^{-10} by direct simplification and norm_num.
proof idea
The definition executes thirteen lines of sequential IO.println calls. It first outputs a boxed header, then states the setup (four constants, three decimal places), gives the explicit upper bound 10^{-12}, and closes with the verification marker for coincidence_negligible. No lemmas are applied beyond the hardcoded text.
why it matters
This definition completes the output pipeline invoked by the main entry point in the same module. It surfaces the probability bound that supports the claim of negligible coincidence, linking directly to the Born-rule probability definition in QuantumLedger and the phi-tier structures in NucleosynthesisTiers.of. Within the Recognition framework it displays how constant matches align with the T0-T8 forcing chain without touching open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.