Proof of `Collision bound for finite random keys`
groundedproofs/Lax235315Proofs/ComponentProofs.lean · lax-235315
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
The noninjective key assignments satisfy the stated finite collision bound.
Proof strategy
Identify noninjectivity with the union of equality events over distinct coordinate pairs. Fixing equality removes one independent key choice; the finite union bound then gives the result.
Attribution
The elementary collision estimate is used to implement the paper's ideal sampler with finite random keys. The component proof is ported from the local Welzl development at commit 44a44623.