Relational delta-matroids on Boolean tuples

IsDeltaMatroid R is the nonempty, one-sided symmetric exchange axiom of Kazda, Kolmogorov and Rolínek, Definition 5, p. 4 (arXiv:1602.03124v6). Coordinates are arbitrary types; Fin n gives the usual tuples. The set {i, j} is a singleton when i = j, allowing a one-coordinate exchange. No simultaneous exchange at both feasible tuples is assumed.

IsEvenDeltaMatroid R additionally requires common parity, of either value, over a finite coordinate type. Empty relations are excluded, including on the empty coordinate type.

Main definitions

• IsDeltaMatroid: nonempty one-sided symmetric exchange.
• IsEvenDeltaMatroid: a delta-matroid with common parity of either value.

Main results

• IsEvenDeltaMatroid.not_mem_flipOn_singleton: a one-coordinate flip is infeasible.
• IsEvenDeltaMatroid.exchange: exchange uses two distinct disagreeing coordinates.

structure Cslib.BitString.IsDeltaMatroid {ι : Type u_1} [DecidableEq ι] (R : Set (ι → Bool)) : Prop

A nonempty Boolean relation satisfying one-sided symmetric exchange. This is Definition 5 of [KKR18], with set flips as in Definition 4.

• nonempty : R.Nonempty
• exchange ⦃x y : ι → Bool⦄ : x ∈ R → y ∈ R → ∀ ⦃i : ι⦄, x i ≠ y i → ∃ (j : ι), x j ≠ y j ∧ flipOn {i, j} x ∈ R

structure Cslib.BitString.IsEvenDeltaMatroid {ι : Type u_1} [DecidableEq ι] [Fintype ι] (R : Set (ι → Bool)) : Prop

A delta-matroid whose feasible tuples have common parity (possibly odd). This is the evenness condition in Definition 5 of [KKR18].

• isDeltaMatroid : IsDeltaMatroid R
• parity_eq ⦃x y : ι → Bool⦄ : x ∈ R → y ∈ R → parityOn Finset.univ x = parityOn Finset.univ y

@[simp]

theorem Cslib.BitString.not_isDeltaMatroid_empty {ι : Type u_1} [DecidableEq ι] : ¬IsDeltaMatroid ∅

Empty relations are not delta-matroids under the nonempty convention.

theorem Cslib.BitString.isDeltaMatroid_singleton {ι : Type u_1} [DecidableEq ι] (x : ι → Bool) : IsDeltaMatroid {x}

A singleton relation is a delta-matroid.

theorem Cslib.BitString.isDeltaMatroid_univ {ι : Type u_1} [DecidableEq ι] : IsDeltaMatroid Set.univ

The full Boolean cube is a delta-matroid, using a single-coordinate exchange.

theorem Cslib.BitString.isEvenDeltaMatroid_singleton {ι : Type u_1} [DecidableEq ι] [Fintype ι] (x : ι → Bool) : IsEvenDeltaMatroid {x}

A singleton relation is even, including a singleton of odd parity.

theorem Cslib.BitString.parityOn_univ_flipOn_singleton {ι : Type u_1} [DecidableEq ι] [Fintype ι] (x : ι → Bool) (i : ι) : parityOn Finset.univ (flipOn {i} x) = !parityOn Finset.univ x

Flipping one coordinate negates total parity.

theorem Cslib.BitString.parityOn_univ_flipOn_pair {ι : Type u_1} [DecidableEq ι] [Fintype ι] (x : ι → Bool) {i j : ι} (hij : i ≠ j) : parityOn Finset.univ (flipOn {i, j} x) = parityOn Finset.univ x

Flipping two distinct coordinates preserves total parity.

theorem Cslib.BitString.IsEvenDeltaMatroid.not_mem_flipOn_singleton {ι : Type u_1} [DecidableEq ι] {R : Set (ι → Bool)} {x : ι → Bool} [Fintype ι] (hR : IsEvenDeltaMatroid R) (hx : x ∈ R) (i : ι) : flipOn {i} x ∉ R

Evenness rules out feasible one-coordinate flips.

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

In an even delta-matroid, exchange flips two distinct coordinates on which the tuples differ.

theorem Cslib.BitString.exists_ne_disagree_of_parity_eq {ι : Type u_1} {x y : ι → Bool} [Fintype ι] (h : parityOn Finset.univ x = parityOn Finset.univ y) {i : ι} (hi : x i ≠ y i) : ∃ (j : ι), j ≠ i ∧ x j ≠ y j

Tuples of equal parity cannot disagree at just one coordinate.

theorem Cslib.BitString.isEvenDeltaMatroid_parityOn_fiber {ι : Type u_1} [DecidableEq ι] [Fintype ι] (b : Bool) (hne : ∃ (x : ι → Bool), parityOn Finset.univ x = b) : IsEvenDeltaMatroid {x : ι → Bool | parityOn Finset.univ x = b}

Every nonempty total-parity fiber is an even delta-matroid. The witness is necessary: the odd fiber on the empty coordinate type is empty.