2.11. Indexed CSP and Table Operations🔗

Cslib.Logic.PL.CSP.Occurrence preserves constraint and scope positions, including repeated variables and identical constraints. Given a supplied value outside : D, consistent valid local labels reconstruct precisely a global CSP model. Reconstruction uses outside at nonoccurring variables; this hypothesis matters when the domain may be empty. The native incidence graph retains one edge per argument; it never expands sparse binary names to a range.

open Cslib.Logic.PL in
example {Rel V D : Type} (sem : Rel → List D → Bool)
    (F : CSP Rel V) (outside : D) :
    F.Satisfiable sem ↔ ∃ l : F.OccurrenceLabeling D,
      CSP.ValidLabeling sem l ∧ CSP.ConsistentLabeling l :=
  CSP.satisfiable_iff_exists_labeling sem outside

Cslib.Logic.PL.CSP.Table is an explicit relation alphabet for the same CSP lists. Its semantics rejects malformed row widths. Local contraction projects outside coordinates and appends a connector bit for zero or one internal change. The local native certificate does not yet prove blossom correctness. Exactly-one generation takes a scope list whose length funds its quadratic output:

open Cslib.Logic.PL.CSP Cslib.Complexity.CSP in
example (scope : List ℕ) (hs : scope ≠ []) :
    ∃ row, (Table.exactlyOne scope).sem row = true :=
  (Table.exists_sem_exactlyOne scope).mpr
    (List.length_pos_iff.mpr hs)

open Cslib.Complexity Cslib.Logic.PL.CSP
  Cslib.Complexity.CSP Turing.MultiTapeTM in
example : ComputableInPolyTime (Table.exactlyOne (V := ℕ))
    (encList encNat) encTable :=
  computableInPolyTime_tableExactlyOne

Cslib.Complexity.Graph.RotationSystem retains indexed ends of loops and parallel edges, all face orbits including fixed points, and cyclic vertex orders. Cslib.Complexity.CSP.RespectsArgumentOrder requires the constraint-side rotation to follow the scope's cyclic order. This rotation structure imposes no genus-zero condition and supplies no planarity recognizer or solver.