coincidenceProbability_net_radius
plain-language theorem explainer
The coincidence probability for four independent draws from a unit-length range, each required to land in a window of radius 0.04, equals 0.04 to the fourth power. Authors checking CPM-bridge constant bounds or net-radius probability estimates would cite this specialization. The proof is a one-line simp unfolding of the general coincidence-probability definition.
Claim. The probability that four independent selections from a range of size $1$ all land within a window of radius $0.04$ equals $0.04^{4}$.
background
The module fixes a simple model of accidental agreement: the coincidence probability that n_domains independent selections from a continuum of length range_size all fall inside a tolerance window of radius tolerance. Concretely it is defined as
$$(\mathrm{tolerance}/\mathrm{range_size})^{n_\mathrm{domains}}.$$
Here the parameters are specialized to four domains, unit range, and tolerance $0.04$. The definition is noncomputable only because it lives in $\mathbb{R}$; the expression itself is elementary. Sibling lemmas in the same file bound this quantity and combine it with other small probabilities used in the CPM-bridge constant checks.
proof idea
One-line wrapper. Unfolding the definition of coincidence probability with simp immediately yields $(0.04/1)^4$, which simplifies to $0.04^4$.
why it matters
The lemma pins a concrete numerical instance used when verifying that net-radius and combined coincidence probabilities stay small in the CPM-bridge constant layer. Downstream siblings such as net_radius_probability_small and combined_probability_small rely on this exact evaluation (or the same definition) to argue that accidental four-way agreement inside a $0.04$ window is negligible. In the broader Recognition verification stack this supports claims that reported constant matches are not chance alignments of independent domain selections. No forcing-chain landmark (T5–T8) is touched directly; the result is pure numerical hygiene for the bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.