Native ordered CSP incidence multigraphs

Variables receive dense names in first-occurrence order; constraint-position vertices follow. There is one listed edge per ordered argument occurrence, including repeated variables and identical constraints. The existing positive-CNF adapter has exactly these scopes, so both the construction and its native polynomial-time certificate reuse SAT.incidenceGraph.

The incidence model is the bipartite multigraph of Fulla–Živný, On Planar Valued CSPs, arXiv:1602.06323v3, Section 2.1, p. 4 (the paragraph preceding Definition 1). Constraint positions replace their indexed valued constraints; ordered scopes give their argument incidences. This module treats arbitrary-domain decision CSPs, retaining nullary constraints and using only occurring variables. It supplies neither a drawing nor the order-preserving plane representation of Definition 1. That extra structure is needed for a planar-CSP claim.

The finite-list naming and encoding proofs are original. Binary source labels are never expanded into a range up to their maximum; generated vertex names are bounded by the input's list sizes.

Main results

• Cslib.Complexity.CSP.incidenceGraph_edges: exact ordered edge list.
• Cslib.Complexity.CSP.incidenceEdgeIndex: identifies each occurrence's distinct edge record.
• Cslib.Complexity.CSP.computableInPolyTime_incidenceGraph: native binary graph construction.

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

The existing listed multigraph, with dense variable and constraint-position vertices.

theorem Cslib.Complexity.CSP.incidenceGraph_vertices {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) : (incidenceGraph F).vertices = List.range (F.numVars + List.length F)

The graph declares precisely the variable interval followed by the constraint interval.

theorem Cslib.Complexity.CSP.incidenceGraph_edges {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) : (incidenceGraph F).edges = List.map (fun (o : ℕ × ℕ × V) => (List.idxOf o.2.2 F.distinctVars, F.numVars + o.1)) F.occurrences

Each occurrence contributes one edge in constraint-then-scope order. Parallel edges remain separate list entries; the original scope position is recoverable from the occurrence table.

theorem Cslib.Complexity.CSP.length_vertices_incidenceGraph {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) : (incidenceGraph F).vertices.length = F.numVars + List.length F

Vertex count includes every constraint position, even identical and nullary constraints.

theorem Cslib.Complexity.CSP.length_edges_incidenceGraph {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) : (incidenceGraph F).edges.length = (List.map (fun (c : Logic.PL.Constraint Rel V) => c.2.length) F).sum

Edge count includes each argument occurrence, even repeated variables.

theorem Cslib.Complexity.CSP.incidenceGraph_bipartite {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} {e : ℕ × ℕ} (he : e ∈ (incidenceGraph F).edges) : e.1 < F.numVars ∧ F.numVars ≤ e.2 ∧ e.2 < F.numVars + List.length F

Every listed edge joins the variable part to the constraint-position part.

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

Both endpoints of every listed edge are declared vertices.

theorem Cslib.Complexity.CSP.incidenceVertices_declared {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (v : ℕ) : v ∈ (incidenceGraph F).incidenceVertices → v ∈ (incidenceGraph F).vertices

Every entry of the flattened incidence-endpoint list is a declared graph vertex.

theorem Cslib.Complexity.CSP.incidenceGraph_loopless {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} {e : ℕ × ℕ} (he : e ∈ (incidenceGraph F).edges) : e.1 ≠ e.2

The two vertex intervals are disjoint, so incidence edges are never loops.

def Cslib.Complexity.CSP.incidenceEdgeIndex {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (o : F.Occurrence) : ℕ

Edge-list position of an argument occurrence, retaining parallel edge identity.

theorem Cslib.Complexity.CSP.incidenceEdgeIndex_lt {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (o : F.Occurrence) : incidenceEdgeIndex o < (incidenceGraph F).edges.length

Every argument occurrence indexes a declared edge record.

theorem Cslib.Complexity.CSP.incidenceEdgeIndex_injective {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} : Function.Injective incidenceEdgeIndex

Different scope or constraint positions give different edge-list positions.

theorem Cslib.Complexity.CSP.exists_incidenceEdgeIndex {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (i : ℕ) (hi : i < (incidenceGraph F).edges.length) : ∃ (o : F.Occurrence), incidenceEdgeIndex o = i

Every edge-list position comes from an argument occurrence.

theorem Cslib.Complexity.CSP.getElem_incidenceEdgeIndex {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (o : F.Occurrence) : (incidenceGraph F).edges[incidenceEdgeIndex o] = (List.idxOf o.var F.distinctVars, F.numVars + ↑o.fst)

The occurrence's listed edge connects its dense variable name to its constraint position.

theorem Cslib.Complexity.CSP.edgeEndpoint_incidenceEdgeIndex {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (o : F.Occurrence) (side : Bool) : (incidenceGraph F).edgeEndpoint (incidenceEdgeIndex o) side = if side = true then F.numVars + ↑o.fst else List.idxOf o.var F.distinctVars

Reuse the general graph endpoint reader: false is the variable, true the constraint.

theorem Cslib.Complexity.CSP.computableInPolyTime_incidenceGraph {Rel V : Type} [DecidableEq V] (encRel : Rel ↪ List Bool) (encV : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime incidenceGraph (encCSP encRel encV) encGraph

Construct the native graph under framed CSP encoding and binary graph labels. Source variables are compared as encoded strings; there is no iteration to their largest name.