coincidenceProbability
plain-language theorem explainer
The coincidence probability for n independent uniform draws from an interval of length R, all landing inside a window of width τ, is (τ/R)^n. CPM-bridge verification lemmas cite it as the base rate for accidental multi-domain net-radius matches. It is a direct power definition under independence and uniformity, not a derived inequality.
Claim. For $n \in \mathbb{N}$ and real parameters $R$ (range size) and $\tau$ (tolerance), the coincidence probability is $(\tau/R)^n$.
background
This definition lives in the CPM-bridge probability constants module inside Verification. That module supplies explicit numerical false-match rates used when arguing that Recognition Science constant alignments are not accidental numerical fits.
Each "domain" is modeled as an independent uniform draw over a continuous range of length $R$. The tolerance $\tau$ is the acceptance-window radius. Under uniformity the single-draw hit rate is $\tau/R$; under independence the joint rate is that quantity to the power $n$.
Downstream lemmas specialize to four domains, unit range, and $\tau = 0.04$, then fold in auxiliary projection and dyadic-schedule factors to obtain a combined bound below $10^{-9}$.
proof idea
Pure definition: the body is the monomial $(\mathrm{tolerance}/\mathrm{range_size})^{n_\mathrm{domains}}$. No lemmas, no tactics; the formula is the independent-uniform product model stated in the doc-comment.
why it matters
Parent uses are the three sibling lemmas in the same module: the specialization coincidenceProbability 4 1 0.04 = 0.04^4, the bound that this is less than $10^{-5}$, and the combined product with projection ($1/100$) and dyadic ($1/1000$) factors below $10^{-9}$.
Those bounds feed the CPM-bridge verification story: multi-domain net-radius agreement at the stated tolerance is treated as too rare to be chance, once projection constants and dyadic schedules are folded in. The definition itself is the shared base rate those lemmas quote; without it the numerical smallness claims have no common expression.
It does not touch the forcing chain (T0–T8), RCL, or the mass ladder directly. It is infrastructure for the verification layer that audits constant matches after those structural results are in place.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.