CoincidenceBound
plain-language theorem explainer
CoincidenceBound packages a natural number counting independent constants, another for decimal-place precision of matches to Recognition Science predictions, a real upper bound on coincidental-agreement probability, and a proof that the bound is below 0.01. Researchers auditing CPM constant derivations cite the structure to formalize the statistical unlikelihood of accidental matches between CPM and RS values. The declaration is a bare structure definition whose sole constraint is the embedded inequality on the probability field.
Claim. A record with four components: a natural number $n$ counting the independent constants, a natural number $p$ for the number of matching decimal places, a real number $q$ serving as an upper bound on the coincidence probability, together with a proof that $q < 0.01$.
background
The CPM.ConstantsAudit module supplies machine-checkable verification that constants satisfy required properties derived from Recognition Science invariants, along with consistency checks between constant sets and probability bounds for coincidental agreement. The local setting centers on export of audit reports through the lake executable cpm_constants_audit. Upstream results include the structure of nuclear densities and photon fluxes in phi-tiers from NucleosynthesisTiers.of, the minimal spatial semantics with independent voxel evolution from LNALSemantics.independent, and the Born-rule probability definition from QuantumLedger.probability as the squared norm of state amplitudes.
proof idea
The declaration is a structure definition with an empty proof body. The only obligation is the field probability_small whose type directly encodes the inequality probability < 0.01.
why it matters
The structure is instantiated by the downstream definition cpmCoincidenceBound, which supplies concrete values numConstants = 4, precision = 3, probability = 10^{-12} and verifies the smallness condition via simp. It supplies the formal bound on coincidental agreement required by the constants-audit infrastructure, supporting the Recognition Science claim that observed matches to phi-ladder and forcing-chain predictions are not accidental.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.