cpmCoincidenceBound
plain-language theorem explainer
Four independent constants each agreeing with Recognition Science predictions to three decimal places produce a coincidence probability bounded above by 10^{-12} according to the CoincidenceBound record supplied here. An auditor preparing a verification report for the CPM constants would invoke this definition to populate the probability field of the audit summary. The construction is a literal structure whose probability_small obligation reduces immediately via exponent rewriting and numerical normalization.
Claim. The CoincidenceBound structure consists of a natural number of independent constants, a natural number recording decimal precision, a real upper bound on coincidence probability, and a proof that this bound is less than 0.01. The present definition instantiates the structure with four constants, three decimal places of agreement, and probability $10^{-12}$.
background
The CPM Constants Audit module supplies machine-checkable verification that constants derived from Recognition Science invariants satisfy required numerical properties. CoincidenceBound is the structure that packages the number of independent constants, the precision of each match, an upper bound on the probability of accidental agreement, and a proof that the bound lies below 0.01. The module also exports consistency checks between cone and eight-tick constant sets together with example certificates.
proof idea
The definition is a direct structure literal. The probability_small field is proved by rewriting the negative exponent via zpow_neg and then applying norm_num to confirm the resulting real number is less than 0.01.
why it matters
This definition supplies the concrete probability bound that feeds the theorem coincidence_negligible, which strengthens the bound to 10^{-10}, and the generateAuditSummary function that assembles the full verification report. It closes one step in the audit pipeline that checks whether the four CPM constants lie inside the Recognition Science alpha band and phi-ladder predictions. The construction thereby contributes to the machine-checked claim that the numerical coincidences are not accidental.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.