Proof of `Assignment moves, pass moves, and deviations` (2nd statement)

groundedproofs/Lax689614Proofs/ExceptionalMove.lean · lax-689614

What this proof establishes

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

After playing the central-clause edge, omit that clause vertex from the biclique and place it in the independent set. Its literal neighbors are absent. The biclique formula and the disjoint pass edges give value (r+k)mod2(r + k) mod 2.