Transport and feasible moves in delta-matroids

Twists and coordinate equivalences preserve the one-sided exchange contract and evenness. Feasible tuples of an even delta-matroid are connected by two-coordinate flips; each move toward a fixed feasible target reduces the Hamming distance by exactly two.

The four-coordinate consequences isolate the exchange arguments in the proof of Lemma 35, p. 17 of arXiv:1602.03124v6 [KKR18], reused in Lemma 37, pp. 18–19. They are statements about one relation, not the paper's full DAG lemmas. The four coordinates are pairwise distinct and the relation is even. The transport and connectivity proofs here are direct arguments, not claims to formalize additional named results of that paper.

Main results

• IsDeltaMatroid.twist, IsDeltaMatroid.reindex: transport of exchange.
• IsEvenDeltaMatroid.twist, IsEvenDeltaMatroid.reindex: transport of evenness.
• IsEvenDeltaMatroid.exists_exchange_hammingDist: a feasible move exactly two closer.
• IsEvenDeltaMatroid.connected: connectivity by feasible two-coordinate flips.
• IsEvenDeltaMatroid.mem_flipOn_four_of_not_mem_cross: a forced four-coordinate flip.
• IsEvenDeltaMatroid.mem_pair_or_mem_cross_of_mem_flipOn_four: a feasible pair alternative.

theorem Cslib.BitString.flipOn_comm {ι : Type u_1} [DecidableEq ι] (S T : Finset ι) (x : ι → Bool) : flipOn S (flipOn T x) = flipOn T (flipOn S x)

Flips at two sets commute, even when the sets overlap.

theorem Cslib.BitString.IsDeltaMatroid.twist {ι : Type u_1} [DecidableEq ι] {R : Set (ι → Bool)} (hR : IsDeltaMatroid R) (S : Finset ι) : IsDeltaMatroid (flipOn S ⁻¹' R)

Twisting a relation by a fixed set of coordinates preserves delta-matroid exchange.

theorem Cslib.BitString.IsDeltaMatroid.reindex {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] [DecidableEq κ] {R : Set (ι → Bool)} (hR : IsDeltaMatroid R) (e : ι ≃ κ) : IsDeltaMatroid {y : κ → Bool | (fun (i : ι) => y (e i)) ∈ R}

Renaming coordinates by an equivalence preserves delta-matroid exchange.

theorem Cslib.BitString.parityOn_univ_flipOn {ι : Type u_1} [DecidableEq ι] [Fintype ι] (S : Finset ι) (x : ι → Bool) : parityOn Finset.univ (flipOn S x) = (parityOn Finset.univ x ^^ decide (S.card % 2 = 1))

The parity change caused by a twist is independent of the tuple.

theorem Cslib.BitString.IsEvenDeltaMatroid.twist {ι : Type u_1} [DecidableEq ι] {R : Set (ι → Bool)} [Fintype ι] (hR : IsEvenDeltaMatroid R) (S : Finset ι) : IsEvenDeltaMatroid (flipOn S ⁻¹' R)

Twists preserve evenness; they may interchange the two parity classes.

theorem Cslib.BitString.parityOn_univ_reindex {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (e : ι ≃ κ) (x : κ → Bool) : (parityOn Finset.univ fun (i : ι) => x (e i)) = parityOn Finset.univ x

Total parity is unchanged by a bijective renaming of coordinates.

theorem Cslib.BitString.IsEvenDeltaMatroid.reindex {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] [DecidableEq κ] {R : Set (ι → Bool)} [Fintype ι] [Fintype κ] (hR : IsEvenDeltaMatroid R) (e : ι ≃ κ) : IsEvenDeltaMatroid {y : κ → Bool | (fun (i : ι) => y (e i)) ∈ R}

Renaming coordinates by an equivalence preserves evenness.

theorem Cslib.BitString.hammingDist_flipOn_pair_add_two {ι : Type u_1} [DecidableEq ι] {x y : ι → Bool} [Fintype ι] {i j : ι} (hij : i ≠ j) (hi : x i ≠ y i) (hj : x j ≠ y j) : hammingDist (flipOn {i, j} x) y + 2 = hammingDist x y

Correcting two distinct disagreeing coordinates reduces the distance by exactly two.

theorem Cslib.BitString.IsEvenDeltaMatroid.exists_exchange_hammingDist {ι : Type u_1} [DecidableEq ι] {R : Set (ι → Bool)} {x y : ι → Bool} [Fintype ι] (hR : IsEvenDeltaMatroid R) (hx : x ∈ R) (hy : y ∈ R) (hne : x ≠ y) : ∃ (i : ι) (j : ι), i ≠ j ∧ x i ≠ y i ∧ x j ≠ y j ∧ flipOn {i, j} x ∈ R ∧ hammingDist (flipOn {i, j} x) y + 2 = hammingDist x y

Exchange makes a feasible step exactly two coordinates closer to a feasible target.

theorem Cslib.BitString.IsEvenDeltaMatroid.connected {ι : Type u_1} [DecidableEq ι] {R : Set (ι → Bool)} {x y : ι → Bool} [Fintype ι] (hR : IsEvenDeltaMatroid R) (hx : x ∈ R) (hy : y ∈ R) : Relation.ReflTransGen (fun (u v : ι → Bool) => u ∈ R ∧ v ∈ R ∧ ∃ (i : ι) (j : ι), i ≠ j ∧ v = flipOn {i, j} u) x y

Any two feasible tuples are joined by feasible two-coordinate flips. Both endpoints of every step lie in the relation.

theorem Cslib.BitString.IsEvenDeltaMatroid.mem_flipOn_four_of_not_mem_cross {ι : Type u_1} [DecidableEq ι] {R : Set (ι → Bool)} {x : ι → Bool} [Fintype ι] (hR : IsEvenDeltaMatroid R) {a b c d : ι} (hab : a ≠ b) (hac : a ≠ c) (had : a ≠ d) (hbc : b ≠ c) (hbd : b ≠ d) (hcd : c ≠ d) (habx : flipOn {a, b} x ∈ R) (hcdx : flipOn {c, d} x ∈ R) (hacx : flipOn {a, c} x ∉ R) (hadx : flipOn {a, d} x ∉ R) : flipOn {a, b, c, d} x ∈ R

The four-coordinate exchange consequence used for property (5) in the proof of Lemma 35 of [KKR18], p. 17, and reused in Lemma 37. Here a,b,c,d correspond to the paper's u,v,x,y. The two forbidden cross-pairs force the four-coordinate flip. The feasible base tuple is not needed for this local consequence.

theorem Cslib.BitString.IsEvenDeltaMatroid.mem_pair_or_mem_cross_of_mem_flipOn_four {ι : Type u_1} [DecidableEq ι] {R : Set (ι → Bool)} {x : ι → Bool} [Fintype ι] (hR : IsEvenDeltaMatroid R) {a b c d : ι} (hab : a ≠ b) (hac : a ≠ c) (had : a ≠ d) (hbc : b ≠ c) (hbd : b ≠ d) (hcd : c ≠ d) (hx : x ∈ R) (hf : flipOn {a, b, c, d} x ∈ R) : flipOn {c, d} x ∈ R ∨ flipOn {a, c} x ∈ R ∨ flipOn {a, d} x ∈ R

The four-coordinate exchange alternative used for the no-shortcuts argument in the proof of Lemma 35 of [KKR18], p. 17, and reused in Lemma 37. Exchange at b from the four-coordinate flip toward the feasible base gives one of these three pairs; no simultaneous exchange conclusion is asserted.