The occurrence-indexed polygon graph of an ordered CSP

There is one edge per actual argument occurrence, from that variable to the next variable in the same cyclic scope. The edge list uses the existing incidence occurrence order. Unary scopes give loops; repeated names and duplicate constraints retain separate edge positions. No relation arity or bound on the variable universe is used. Nullary constraints contribute no edge.

This is an explicit finite-list construction of the primal face model of [DK15], printed p. 434. The exact occurrence maps and permutation formulas are original reconstruction. The graph alone does not establish geometric realizability or a native time bound.

Main definitions

• Cslib.Complexity.CSP.polygonGraph: explicit occurrence-ordered cyclic-scope edges.
• Cslib.Complexity.CSP.polygonEdgeEquiv: exact occurrence-to-edge-position map.
• Cslib.Complexity.CSP.polygonDart: the two indexed ends of each occurrence edge.

Main results

• Cslib.Complexity.CSP.vertex_polygonDart: exact dense endpoints.
• Cslib.Complexity.CSP.polygon_scope_word: original scope order after dense naming.
• Cslib.Complexity.CSP.length_vertices_polygonGraph_le: vertices bounded by occurrences.

def Cslib.Complexity.CSP.argumentPermutation {Rel V : Type} (F : Logic.PL.CSP Rel V) : Equiv.Perm F.Occurrence

Argument succession, with an explicit inverse at each constraint position.

def Cslib.Complexity.CSP.polygonNext {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (i j : ℕ) (v : V) : ℕ

The next dense variable, computed from an occurrence record by bounded list lookups. Invalid records return the supplied variable's dense name; actual occurrences never use it.

@[simp]

theorem Cslib.Complexity.CSP.polygonNext_occurrence {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (o : F.Occurrence) : polygonNext F (↑o.fst) (↑o.snd) o.var = List.idxOf (argumentSuccessor o).var F.distinctVars

Actual ordered occurrences read the next scope variable, with cyclic wraparound.

def Cslib.Complexity.CSP.polygonGraph {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) : Graph

Dense occurring variables and one listed cyclic-scope edge per occurrence.

@[simp]

theorem Cslib.Complexity.CSP.length_edges_polygonGraph {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) : (polygonGraph F).edges.length = (incidenceGraph F).edges.length

The polygon construction keeps exactly the incidence edge positions.

def Cslib.Complexity.CSP.polygonDart {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (o : F.Occurrence) (side : Bool) : (polygonGraph F).Dart

Every argument occurrence retains its own listed polygon edge.

theorem Cslib.Complexity.CSP.getElem_polygonEdge {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (o : F.Occurrence) : (polygonGraph F).edges[incidenceEdgeIndex o] = (List.idxOf o.var F.distinctVars, List.idxOf (argumentSuccessor o).var F.distinctVars)

The listed edge at an occurrence has its two prescribed dense endpoints.

@[simp]

theorem Cslib.Complexity.CSP.vertex_polygonDart {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (o : F.Occurrence) (side : Bool) : (polygonDart o side).vertex = if side = true then List.idxOf (argumentSuccessor o).var F.distinctVars else List.idxOf o.var F.distinctVars

Both endpoint choices retain the cyclic scope order, even when the edge is a loop.

theorem Cslib.Complexity.CSP.polygonDart_injective {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} : Function.Injective fun (x : F.Occurrence × Bool) => polygonDart x.1 x.2

No two occurrence/end pairs are collapsed by equal endpoint labels.

theorem Cslib.Complexity.CSP.exists_polygonDart {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (d : (polygonGraph F).Dart) : ∃ (o : F.Occurrence), polygonDart o d.2 = d

Every polygon dart has an occurrence and an end; no additional darts are introduced.

noncomputable def Cslib.Complexity.CSP.polygonDartEquiv {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) : F.Occurrence × Bool ≃ (polygonGraph F).Dart

Occurrence/end coordinates on the actual listed polygon graph. The inverse only recovers indices from the existing occurrence enumeration; it chooses no graph or rotation.

noncomputable def Cslib.Complexity.CSP.polygonEdgeEquiv {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) : F.Occurrence ≃ Fin (polygonGraph F).edges.length

The exact edge-position map: one edge for each actual argument occurrence.

theorem Cslib.Complexity.CSP.length_edges_polygonGraph_eq_card {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) : (polygonGraph F).edges.length = Fintype.card F.Occurrence

Edge count is exactly the number of ordered occurrences, rather than distinct pairs.

@[simp]

theorem Cslib.Complexity.CSP.polygonDartEquiv_apply {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (x : F.Occurrence × Bool) : (polygonDartEquiv F) x = polygonDart x.1 x.2

The forward polygon coordinate map is the explicit occurrence/end map.

theorem Cslib.Complexity.CSP.sameCycle_argumentPermutation {Rel V : Type} {F : Logic.PL.CSP Rel V} (o p : F.Occurrence) : (argumentPermutation F).SameCycle o p ↔ o.fst = p.fst

The scope permutation has exactly one orbit per nonempty constraint position.

theorem Cslib.Complexity.CSP.polygonGraph_endpoints {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} {edge : ℕ × ℕ} (he : edge ∈ (polygonGraph F).edges) : edge.1 ∈ (polygonGraph F).vertices ∧ edge.2 ∈ (polygonGraph F).vertices

Both ends of every polygon edge are declared dense occurring variables.

theorem Cslib.Complexity.CSP.length_vertices_polygonGraph_le {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) : (polygonGraph F).vertices.length ≤ (polygonGraph F).edges.length

Dense vertex count is bounded by actual scope occurrences, independent of label sizes.

theorem Cslib.Complexity.CSP.polygon_scope_word {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (i : Fin (List.length F)) : (List.ofFn fun (j : Fin F[↑i].2.length) => (polygonDart ⟨i, j⟩ false).vertex) = List.map (fun (x : V) => List.idxOf x F.distinctVars) F[↑i].2

The forward-dart word at a constraint is its exact original scope after dense naming.

theorem Cslib.Complexity.CSP.length_constraints_le_polygon_edges {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (hPos : ∀ (i : Fin (List.length F)), 0 < F[↑i].2.length) : List.length F ≤ (polygonGraph F).edges.length

With positive actual scopes, constraint positions are also bounded by occurrences.