Proof of `Collision and length bounds for independently sampled paths` (1st statement)
groundedproofs/Lax263307Proofs/PathSampling.lean · lax-263307
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
An ordered adjacent pair witnesses every edge joining two outcomes. Sum these witness indicators, then factor the two independent outcome probabilities into the corresponding endpoint loads. Ordered pairs account for both edge orientations.