2.20. Delta-Matroid Closure for Local Contraction🔗

Cslib.BitString.IsDeltaMatroid.comp and Cslib.BitString.IsEvenDeltaMatroid.comp prove relational composition along finite shared coordinates. They require a nonempty output: nonempty input relations can disagree on the shared values. The proofs use the one-sided exchange axiom and permit empty external coordinate types.

For the actual guarded table operation, Cslib.Logic.PL.CSP.Table.isEvenDeltaMatroid_contract supplies the mathematical invariant used by blossom contraction. A feasible reference and distinct in-range internal positions are enough; the reference witnesses output nonemptiness internally:

open Cslib.BitString Cslib.Logic.PL.CSP in
example {table : Table} {reference : List Bool} {positions : List ℕ}
    (hR : IsEvenDeltaMatroid (booleanRelation Table.arity Table.sem table))
    (hc : Table.canContract table reference positions = true) :
    IsEvenDeltaMatroid (booleanRelation Table.arity Table.sem
      (Table.contract table reference positions)) :=
  Table.isEvenDeltaMatroid_contract hR hc

The new connector's exactly-one relation is even for every nonempty scope, with odd common parity. Empty scopes are excluded. These local mathematical closures feed the whole-instance layer and complete native edge solver below.