Proof of `Choosing a collision-free outcome with bounded total path length` (1st statement)
groundedproofs/Lax263307Proofs/SamplingOutcomes.lean · lax-263307
What this proof establishes
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
Markov bounds the probability of cost exceeding by one quarter. Union with the bad event has probability at most one half, so its complement has positive probability. A positive summand supplies the desired outcome.
Attribution
Bonnet–Chang, choice of the sampled routes in Lemma 11.