Even delta-matroid table relations

The relations here are exactly CSP.booleanRelation Table.arity Table.sem, including the existing declared-width and well-formedness guards. Exactly-one has odd common parity and requires a nonempty scope. Local contraction follows Section 5.3, printed pp. 12–13 of [KKR18], arXiv v6: a feasible reference and distinct in-range internal positions suffice for the local closure. The star composition is transported back to the actual outside-coordinate order with the connector last, using Table.sem_contract_cases rather than reproving the operation semantics. No blossom invariant or solver is assumed. The generic exactly-one result corresponds to Example 17, printed p. 7; the empty scope is excluded as required by the nonempty convention in Definition 5.

Main results

• booleanRelation_exactlyOne: identifies the actual table relation with exactly-one.
• isEvenDeltaMatroid_exactlyOne: arbitrary nonempty connector scope.
• not_isDeltaMatroid_exactlyOne_nil: zero connectors are rejected.
• isEvenDeltaMatroid_contract: closure of the actual guarded local contraction.

theorem Cslib.Logic.PL.CSP.Table.booleanRelation_exactlyOne {V : Type u_1} (scope : List V) : booleanRelation arity sem (exactlyOne scope) = BitString.oneHotRelation (Fin scope.length)

The guarded table relation is precisely the usual exactly-one relation.

theorem Cslib.Logic.PL.CSP.Table.isEvenDeltaMatroid_exactlyOne {V : Type u_1} (scope : List V) (hne : scope ≠ []) : BitString.IsEvenDeltaMatroid (booleanRelation arity sem (exactlyOne scope))

The new connector table is an even delta-matroid for every nonempty scope. Repeated names in the supplied scope do not change this local relation claim.

theorem Cslib.Logic.PL.CSP.Table.not_isDeltaMatroid_exactlyOne_nil {V : Type u_1} : ¬BitString.IsDeltaMatroid (booleanRelation arity sem (exactlyOne []))

Zero connectors give the empty relation, excluded by the nonempty delta-matroid convention.

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

Local contraction preserves the actual guarded declared-arity even delta-matroid relation. A feasible reference supplies compatibility with the star gadget. The selected positions must be distinct and in range, exactly as required by canContract; no blossom condition is used.