Proof of `Removing nonpositive weights` (2nd statement)
groundedproofs/Lax263307Proofs/PositiveWeights.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
Clipping negative weights and removing nonpositive returned vertices preserves the requested approximation factor.
Proof strategy
The filtered output has exactly the clipped weight of the original output. Clipping can only increase a comparison set's weight, and filtering preserves independence. Multiply the comparison by the nonnegative approximation factor.