Fixed-language cyclic-difference tables

Tables enumerate the accepted tuples at the declared arity and take ordered neighboring exclusive ors, including last-to-first. This is the dR operation of [DK15], Section 3, printed p. 439, and [KKR18], Definition 14 (v6, printed p. 0:6). Empty and nullary relations retain their exact meaning. Enumeration costs may be exponential in the arity; native compilation uses this only as a fixed finite language lookup. No uniform language-preprocessing claim is made.

The fixed rejection instance has two singleton unary tables on one variable. Each relation is a nonempty even delta-matroid, although their conjunction is unsatisfiable.

Main definitions

• Cslib.Logic.PL.CSP.Table.differenceTable: explicit ordered difference table.
• Cslib.Logic.PL.CSP.Table.rejectEdge: fixed unsatisfiable edge instance.

def Cslib.Logic.PL.CSP.Table.differenceTable {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (r : Rel) : Table

Explicit accepted cyclic differences in the original scope order. Enumeration is static for each symbol of a fixed finite language, independently of raw instance scope lengths.

@[simp]

theorem Cslib.Logic.PL.CSP.Table.arity_differenceTable {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (r : Rel) : (differenceTable arity sem r).arity = arity r

theorem Cslib.Logic.PL.CSP.Table.wellFormed_differenceTable {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (r : Rel) : (differenceTable arity sem r).wellFormed = true

Stored rows have the exact original declared width.

theorem Cslib.Logic.PL.CSP.Table.booleanRelation_differenceTable {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (r : Rel) : booleanRelation Table.arity Table.sem (differenceTable arity sem r) = BitString.cyclicDifferenceRelation (booleanRelation arity sem r)

The actual guarded table denotes precisely the existing ordered difference relation.

theorem Cslib.Logic.PL.CSP.Table.sem_differenceTable {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (r : Rel) (row : List Bool) : (differenceTable arity sem r).sem row = true ↔ ∃ (x : Fin (arity r) → Bool), sem r (List.ofFn x) = true ∧ List.ofFn (BitString.cyclicDifference x) = row

Accepted rows are exactly the ordered differences of accepted source tuples.

theorem Cslib.Logic.PL.CSP.Table.parity_differenceTable {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (r : Rel) (row : List Bool) (hrow : (differenceTable arity sem r).sem row = true) : BitString.wordParity row = false

Every accepted difference row has even parity, including the nullary row.

theorem Cslib.Logic.PL.CSP.Table.sem_differenceTable_cyclicDifference {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (r : Rel) (hself : BitString.IsSelfComplementary (booleanRelation arity sem r)) {n : ℕ} (hwidth : n = arity r) (x : Fin n → Bool) : (differenceTable arity sem r).sem (List.ofFn (BitString.cyclicDifference x)) = true ↔ sem r (List.ofFn x) = true

Self-complementary recovery through the actual explicit table, at any matching arity.

theorem Cslib.Logic.PL.CSP.Table.isEvenDeltaMatroid_differenceTable {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (r : Rel) (h : BitString.IsEvenDeltaMatroid (BitString.cyclicDifferenceRelation (booleanRelation arity sem r))) : BitString.IsEvenDeltaMatroid (booleanRelation Table.arity Table.sem (differenceTable arity sem r))

Static language evenness transfers to the actual explicit table. Empty relations are excluded by this hypothesis, rather than silently treated as nonempty delta-matroids.

theorem Cslib.Logic.PL.CSP.Table.length_rows_differenceTable_le {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (r : Rel) : (differenceTable arity sem r).rows.length ≤ 2 ^ arity r

At most one row per Boolean source tuple; duplicates need not be removed.

def Cslib.Logic.PL.CSP.Table.pinTable (b : Bool) : Table

Unary singleton table, allowing either common parity.

theorem Cslib.Logic.PL.CSP.Table.booleanRelation_pinTable (b : Bool) : booleanRelation arity sem (pinTable b) = {fun (x : Fin 1) => b}

The unary singleton table pins its sole coordinate.

theorem Cslib.Logic.PL.CSP.Table.isEvenDeltaMatroid_pinTable (b : Bool) : BitString.IsEvenDeltaMatroid (booleanRelation arity sem (pinTable b))

Singleton unary relations are even delta-matroids, including the odd pin.

def Cslib.Logic.PL.CSP.Table.rejectEdge : CSP Table ℕ

Fixed unsatisfiable edge instance with two nonempty singleton unary relations.

theorem Cslib.Logic.PL.CSP.Table.edgeInstance_rejectEdge : rejectEdge.EdgeInstance

Rejection remains an edge instance: one variable in two distinct unary constraints.

theorem Cslib.Logic.PL.CSP.Table.wellFormed_rejectEdge : WellFormed arity rejectEdge

Both rejecting tables have the exact declared width.

theorem Cslib.Logic.PL.CSP.Table.not_satisfiable_rejectEdge : ¬Satisfiable sem rejectEdge

Rejection is semantic, not a malformed or empty-relation shortcut.

theorem Cslib.Logic.PL.CSP.Table.rejectEdge_tables (c : Constraint Table ℕ) (hc : c ∈ rejectEdge) : BitString.IsEvenDeltaMatroid (booleanRelation arity sem c.1)

Every rejecting constraint uses a nonempty even delta-matroid.