Counting disagreements using even delta-matroid exchange

A forbidden two-coordinate move at a feasible base tuple bounds disagreements on one set of coordinates by disagreements on another. The proof uses one-sided exchange at a specified coordinate and induction on Hamming distance; it requires neither simultaneous exchange nor matching realizability. Common parity may be either even or odd.

Main results

• IsEvenDeltaMatroid.card_disagree_le: a local counting bound from forbidden base moves.

theorem Cslib.BitString.IsEvenDeltaMatroid.card_disagree_le {ι : Type u_1} [DecidableEq ι] [Fintype ι] {R : Set (ι → Bool)} {x y : ι → Bool} (hR : IsEvenDeltaMatroid R) (hx : x ∈ R) (hy : y ∈ R) (I O : Finset ι) (hIO : Disjoint I O) (hmove : ∀ i ∈ I, ∀ j ∉ O, j ≠ i → flipOn {i, j} x ∉ R) : {i ∈ I | x i ≠ y i}.card ≤ {i ∈ O | x i ≠ y i}.card

If every feasible two-coordinate move from x entering I must also enter O, then any feasible tuple disagrees with x on at most as many coordinates of I as of O. The sets must be disjoint. This is a counting consequence of one-sided even exchange.