Proof of `Discarding long almost-embedding routes` (1st 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
The discarded source edges are a filtered subset of the unordered edge set. Each has route size at least L. Sum this bound over the filtered subset and compare with the full nonnegative sum.