Composition of Boolean delta-matroids

Composition identifies shared coordinates and existentially removes them. This formalizes Proposition 6 and its evenness corollary of [KKR18], arXiv v6, printed pp. 4–5. In addition to the source's exchange hypotheses we require a nonempty output: nonempty inputs alone need not have compatible shared coordinates. Empty external coordinate types are allowed. The proof uses one-sided exchange twice to eliminate one equal pair, then eliminates finitely many pairs; it assumes no simultaneous exchange principle.

Main definitions

• comp: relational composition along finitely many shared Boolean coordinates.
• tracePair, trace: eliminate one equal pair, or a finite family of equal pairs.
• oneHotRelation: exactly-one on an arbitrary coordinate type.
• star, starAt: the all-zero or single-internal/connector-pair gadget and its twists.

Main results

• IsDeltaMatroid.comp, IsEvenDeltaMatroid.comp: closure with compatible output.
• isEvenDeltaMatroid_oneHotRelation: exactly-one has odd common parity.
• isEvenDeltaMatroid_starAt: the reference-based contraction gadget is even.

def Cslib.BitString.sumProd {ι κ : Type u} (R : Set (ι → Bool)) (S : Set (κ → Bool)) : Set (ι ⊕ κ → Bool)

The direct product of Boolean relations on disjoint coordinate types.

theorem Cslib.BitString.IsDeltaMatroid.sumProd {ι κ : Type u} [DecidableEq ι] [DecidableEq κ] {R : Set (ι → Bool)} {S : Set (κ → Bool)} (hR : IsDeltaMatroid R) (hS : IsDeltaMatroid S) : IsDeltaMatroid (BitString.sumProd R S)

Direct products preserve one-sided exchange.

theorem Cslib.BitString.parityOn_univ_sum {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (x : α ⊕ β → Bool) : parityOn Finset.univ x = ((parityOn Finset.univ fun (i : α) => x (Sum.inl i)) ^^ parityOn Finset.univ fun (k : β) => x (Sum.inr k))

Parity splits over disjoint coordinate types.

theorem Cslib.BitString.IsEvenDeltaMatroid.sumProd {ι κ : Type u} [DecidableEq ι] [DecidableEq κ] [Fintype ι] [Fintype κ] {R : Set (ι → Bool)} {S : Set (κ → Bool)} (hR : IsEvenDeltaMatroid R) (hS : IsEvenDeltaMatroid S) : IsEvenDeltaMatroid (BitString.sumProd R S)

Direct products preserve common parity, including odd parity inputs.

def Cslib.BitString.tracePair {ι : Type u} (R : Set (ι ⊕ Bool → Bool)) : Set (ι → Bool)

Identify two coordinates, indexed by Bool, and remove both.

theorem Cslib.BitString.IsDeltaMatroid.tracePair {ι : Type u} [DecidableEq ι] {R : Set (ι ⊕ Bool → Bool)} (hR : IsDeltaMatroid R) (hne : (BitString.tracePair R).Nonempty) : IsDeltaMatroid (BitString.tracePair R)

Eliminating one equal pair preserves exchange, provided the result is nonempty. When exchange enters the hidden pair, a second exchange exits it. Both steps move toward the same feasible target, so the second cannot undo the first external coordinate.

theorem Cslib.BitString.IsEvenDeltaMatroid.tracePair {ι : Type u} [DecidableEq ι] [Fintype ι] {R : Set (ι ⊕ Bool → Bool)} (hR : IsEvenDeltaMatroid R) (hne : (BitString.tracePair R).Nonempty) : IsEvenDeltaMatroid (BitString.tracePair R)

An eliminated equal pair contributes zero parity.

def Cslib.BitString.trace {ι κ : Type u} (R : Set (ι ⊕ κ × Bool → Bool)) : Set (ι → Bool)

Identify and eliminate a finite family of disjoint equal pairs.

theorem Cslib.BitString.IsDeltaMatroid.trace {ι κ : Type u} [DecidableEq ι] [DecidableEq κ] [Finite κ] {R : Set (ι ⊕ κ × Bool → Bool)} (hR : IsDeltaMatroid R) (hne : (BitString.trace R).Nonempty) : IsDeltaMatroid (BitString.trace R)

Finite equal-pair elimination preserves exchange. The output must have a witness.

theorem Cslib.BitString.IsEvenDeltaMatroid.trace {ι κ : Type u} [DecidableEq ι] [DecidableEq κ] [Fintype ι] [Fintype κ] {R : Set (ι ⊕ κ × Bool → Bool)} (hR : IsEvenDeltaMatroid R) (hne : (BitString.trace R).Nonempty) : IsEvenDeltaMatroid (BitString.trace R)

Eliminating equal pairs preserves common parity.

def Cslib.BitString.comp {ι κ τ : Type u} (R : Set (ι ⊕ κ → Bool)) (S : Set (κ ⊕ τ → Bool)) : Set (ι ⊕ τ → Bool)

Composition by existential equality of the shared coordinates κ. The external coordinates retain the ι, then τ, order.

theorem Cslib.BitString.IsDeltaMatroid.comp {ι κ τ : Type u} [DecidableEq ι] [DecidableEq κ] [DecidableEq τ] [Finite κ] {R : Set (ι ⊕ κ → Bool)} {S : Set (κ ⊕ τ → Bool)} (hR : IsDeltaMatroid R) (hS : IsDeltaMatroid S) (hne : (BitString.comp R S).Nonempty) : IsDeltaMatroid (BitString.comp R S)

Proposition 6 of [KKR18], with compatibility explicit. Neither input nonemptiness nor nonempty external coordinates imply compatibility.

theorem Cslib.BitString.IsEvenDeltaMatroid.comp {ι κ τ : Type u} [DecidableEq ι] [DecidableEq κ] [DecidableEq τ] [Fintype ι] [Fintype κ] [Fintype τ] {R : Set (ι ⊕ κ → Bool)} {S : Set (κ ⊕ τ → Bool)} (hR : IsEvenDeltaMatroid R) (hS : IsEvenDeltaMatroid S) (hne : (BitString.comp R S).Nonempty) : IsEvenDeltaMatroid (BitString.comp R S)

The parity corollary after Proposition 6, with nonempty output explicit.

def Cslib.BitString.oneHotRelation (ι : Type u_1) [DecidableEq ι] : Set (ι → Bool)

The relation with exactly one true coordinate. The coordinate type must be inhabited for this relation to be a delta-matroid.

theorem Cslib.BitString.isEvenDeltaMatroid_oneHotRelation {ι : Type u} [DecidableEq ι] [Fintype ι] [Nonempty ι] : IsEvenDeltaMatroid (oneHotRelation ι)

Exactly-one is an even delta-matroid of odd common parity. This is Example 17 of [KKR18], printed p. 7, with a nonempty coordinate type explicit: the arity-zero relation has no tuples and is excluded by Definition 5.

def Cslib.BitString.star (κ : Type u_1) [DecidableEq κ] : Set (κ ⊕ Unit → Bool)

The even star gadget in Section 5.3 of [KKR18], printed p. 12. It accepts all-zero, and each tuple with one internal bit and the final connector true. It is exactly-one twisted at the connector, rather than exactly-one on all ports.

theorem Cslib.BitString.isEvenDeltaMatroid_star {κ : Type u} [DecidableEq κ] [Fintype κ] : IsEvenDeltaMatroid (star κ)

The star relation is an even delta-matroid, including with no internal coordinates.

theorem Cslib.BitString.mem_star_iff {κ : Type u} [DecidableEq κ] {x : κ ⊕ Unit → Bool} : x ∈ star κ ↔ (∀ (k : κ), x (Sum.inl k) = false) ∧ x (Sum.inr ()) = false ∨ ∃ (k : κ), (∀ (j : κ), x (Sum.inl j) = decide (j = k)) ∧ x (Sum.inr ()) = true

The star's two cases: all internal bits zero, or exactly one true internal bit. The connector is false in the first case and true in the second.

def Cslib.BitString.starAt {κ : Type u} [DecidableEq κ] [Fintype κ] (reference : κ → Bool) : Set (κ ⊕ Unit → Bool)

The star gadget based at an arbitrary internal reference tuple; its connector reference is false. Only the internal coordinates are twisted.

theorem Cslib.BitString.isEvenDeltaMatroid_starAt {κ : Type u} [DecidableEq κ] [Fintype κ] (reference : κ → Bool) : IsEvenDeltaMatroid (starAt reference)

The reference-based star remains even.

theorem Cslib.BitString.mem_starAt_iff {κ : Type u} [DecidableEq κ] [Fintype κ] (reference : κ → Bool) {x : κ ⊕ Unit → Bool} : x ∈ starAt reference ↔ (∀ (k : κ), (x (Sum.inl k) != reference k) = false) ∧ x (Sum.inr ()) = false ∨ ∃ (k : κ), (∀ (j : κ), (x (Sum.inl j) != reference j) = decide (j = k)) ∧ x (Sum.inr ()) = true

Membership in the reference-based star records zero or one internal deviations.