combined_probability_small
plain-language theorem explainer
Conservative product bound: net coincidence probability for four unit-range selections at tolerance 0.04, times fixed projection (1/100) and dyadic (1/1000) factors, is strictly less than 10^{-9}. Verification authors cite it when arguing that CPM constant alignments are negligible under independent-selection models. The proof is a direct numerical discharge after unfolding the power formula.
Claim. Let $p_{\mathrm{net}}=(0.04/1)^{4}$ be the probability that four independent selections from a unit range all fall in a window of radius $0.04$, and set $p_{\mathrm{proj}}=1/100$, $p_{\mathrm{dyadic}}=1/1000$. Then $p_{\mathrm{net}}\,p_{\mathrm{proj}}\,p_{\mathrm{dyadic}}<10^{-9}$.
background
The module treats coincidence under independent draws: the probability that n_domains selections from a continuum of size range_size all land inside a window of radius tolerance is modeled as $({\mathrm{tolerance}}/{\mathrm{range_size}})^{n}$. That quantity is the definition of the local coincidence probability.
Here the net factor uses four domains, unit range, and tolerance $0.04$, so it collapses to $0.04^{4}$. Two auxiliary conservative factors are then multiplied in: a projection-constant bound $1/100$ and a dyadic-schedule bound $1/1000$. These stand in for coarser estimates on projection and scheduling constants from the CPM constants bundle (Knet, Cproj, and related nonnegativity data), without needing the full structure fields in the inequality itself.
The local setting is verification of the CPM bridge: showing that stacked independent-coincidence contributions remain tiny under fixed numerical proxies.
proof idea
Introduce the three let-bound factors. Reduce the goal to the concrete real inequality $0.04^{4}/100/1000 < 10^{-9}$ by unfolding the coincidence definition (tolerance over range, raised to four). Discharge that numerical claim with norm_num, then transport back with simpa using the let-bindings and the coincidence formula. No external lemmas beyond the definition and arithmetic normalization.
why it matters
Sits in the CPM-bridge constants/probability layer of Verification. It packages a conservative combined coincidence estimate (net window match times projection and dyadic proxies) as a single proved bound below one part in a billion.
No recorded downstream consumers yet; the lemma is a leaf ready for bridge arguments that need a uniform smallness certificate on stacked selection probabilities. In the broader Recognition stack it supports the verification side of the CPM Law-of-Existence constants bundle, where one must argue that apparent numerical alignments of bridge constants are not accidental under independent-draw models. It does not itself touch the forcing chain (T5–T8), RCL, or the mass ladder; it is bookkeeping for verification numerics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.