Proof of `Removing nonpositive weights` (1st 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
The empty independent set is optimal when all weights are nonpositive.
Proof strategy
Every comparison set has nonpositive total weight. Multiplication by the nonnegative approximation factor preserves this upper bound by zero.