Explicit-table edge-model checks

Check scope widths, nonempty well-formed stored relations, edge incidences, common parity and the one-sided symmetric exchange axiom by scanning actual stored rows and coordinates. No Boolean cube or interval below a binary arity or variable name is enumerated. Duplicate rows and constraints are permitted; repeated names within a scope are rejected.

The checked model is EdgeInstance.EvenConstraints with the actual Table.sem, including its global well-formedness guard. The even delta-matroid convention requires nonempty local relations, including the unique true nullary relation. This checker is original bookkeeping for Definition 5 of [KKR18], arXiv:1602.03124v6, printed pp. 4–5.

def Cslib.Complexity.CSP.EdgeSolver.checkPair (table : Logic.PL.CSP.Table) (x y : List Bool) : Bool

Check parity and all one-sided exchanges between two explicit stored rows. The coordinates are paid for by the first row's actual list.

def Cslib.Complexity.CSP.EdgeSolver.checkConstraint (c : Logic.PL.Constraint Logic.PL.CSP.Table ℕ) : Bool

Check a constraint's full finite model, including declared arity and scope width.

def Cslib.Complexity.CSP.EdgeSolver.checkEdge (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) : Bool

Check the actual edge model without scanning a finite universe of names.

def Cslib.Complexity.CSP.EdgeSolver.checkModel (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) : Bool

Complete model guard. False and malformed relations reject before optimization.

theorem Cslib.Complexity.CSP.EdgeSolver.checkEdge_eq_true (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) : checkEdge F = true ↔ F.EdgeInstance

The incidence guard checks precisely the original positional edge model.

theorem Cslib.Complexity.CSP.EdgeSolver.checkConstraint_sound (c : Logic.PL.Constraint Logic.PL.CSP.Table ℕ) (h : checkConstraint c = true) : BitString.IsEvenDeltaMatroid {x : Fin c.2.length → Bool | c.1.sem (List.ofFn x) = true}

The stored-row tests establish the actual nonempty even delta-matroid relation on the scope's ordered positions. There is no assumed exchange or parity certificate.

theorem Cslib.Complexity.CSP.EdgeSolver.checkConstraint_complete (c : Logic.PL.Constraint Logic.PL.CSP.Table ℕ) (hR : BitString.IsEvenDeltaMatroid {x : Fin c.2.length → Bool | c.1.sem (List.ofFn x) = true}) : checkConstraint c = true

Every actual nonempty even delta-matroid table on the scope passes the stored-row test. In particular, the checker does not impose even local parity or distinct stored rows.

theorem Cslib.Complexity.CSP.EdgeSolver.checkModel_sound (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (h : checkModel F = true) : F.EdgeInstance ∧ Logic.PL.CSP.EdgeInstance.EvenConstraints Logic.PL.CSP.Table.sem F

Every semantic solver precondition follows from the guard on the raw framed input.

theorem Cslib.Complexity.CSP.EdgeSolver.checkModel_eq_true (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) : checkModel F = true ↔ F.EdgeInstance ∧ Logic.PL.CSP.EdgeInstance.EvenConstraints Logic.PL.CSP.Table.sem F

The full guard recognizes exactly the original edge/even-delta-matroid model.