Proof of `Discarding long almost-embedding routes` (2nd statement)
groundedproofs/Lax263307Proofs/RoutePruning.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
Restrict the edge routes to the graph obtained by deleting long source edges. Their connectivity, endpoints, and induced noninteraction remain valid. A remaining edge cannot have a long route by its deletion predicate.