net_radius_probability_small
plain-language theorem explainer
Four independent domain selections inside a net-radius window of 0.04 have coincidence probability strictly below 10^{-5}. Authors of CPM-bridge constant checks cite this as a concrete false-match bound. The proof is pure arithmetic: the probability equals 1/390625, which is less than 1/100000.
Claim. The probability that four independent selections from a range of size $1$ all land inside a window of radius $0.04$ is strictly less than $1/100000$.
background
The CPM bridge constants probability module defines a coincidence model: the chance that n_domains independent selections from a range of size range_size all fall inside a window of radius tolerance. That quantity is the local coincidenceProbability definition; siblings specialize it to net-radius parameters and combine it with auxiliary projection and schedule bounds.
Here the parameters are fixed at four domains, unit range, and tolerance $0.04$. The numerical content is elementary: relative window size $0.04$ raised to the fourth power. Related probability vocabulary elsewhere in the monolith (Born-rule configuration weights on the quantum ledger, Boltzmann level weights) is not used; this lemma is a self-contained numerical inequality for the combinatorial coincidence model.
proof idea
Unfold the coincidence definition and evaluate by norm_num to obtain the exact value $1/390625$, i.e. $(0.04)^4$. A second norm_num step proves $1/390625 < 1/100000$. Rewrite the goal through the equality and finish. No external lemmas beyond the definition and arithmetic normalization.
why it matters
Lives in Verification.CPMBridge.Constants.Probability and pins a concrete false-coincidence ceiling for four-domain net-radius matching. The natural consumer is the sibling combined bound (doc: "Conservative combined coincidence probability using auxiliary bounds for projection constants and dyadic schedules"), even though the current use-graph lists no downstream edges yet.
This is verification hygiene for CPM bridge constants, not a step in the forcing chain (T0–T8) or a derivation from the Recognition Composition Law. Its role is to keep a numerical claim machine-checked rather than informal, so later combined probability statements can quote a proved $10^{-5}$ ceiling instead of a hand estimate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.