Proof of `An induced almost-embedding from a good route sample`
groundedproofs/Lax263307Proofs/SampledAlmostEmbeddings.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
Enumerate source edges and apply the good-sample theorem to their endpoint maps. Positive probability fixes shared endpoint images and makes every route a simple graph walk. Disjoint source edges have four distinct endpoints, so the good event forbids both route intersection and host adjacency. Reindex the total route-size sum back to unordered source edges.