Proof of `Independent-set encodings satisfy the relaxation` (2nd statement)
groundedproofs/Lax263307Proofs/RelaxationFeasibility.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
Every independent-set indicator satisfies the relaxation constraints.
Proof strategy
Inclusion indicators are monotone, and every subset of an independent set is independent. The mass equation counts the vertices of the selected set when the conditioning set is included, and is zero otherwise.
Attribution
Bonnet–Chang, Section 4, equation (13).