Components of the occurrence-indexed polygon graph

Replacing a positive constraint star by its indexed cyclic scope preserves connected components. All component statements use the existing graph reachability relation on declared vertices.

Main results

• Cslib.Complexity.CSP.sameComponent_polygon_iff: exact reachability correspondence.
• Cslib.Complexity.CSP.polygonComponentEquiv: bijection of actual graph components.

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

All endpoints in the flattened polygon list are declared dense vertices.

theorem Cslib.Complexity.CSP.polygon_sameComponent_successor {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (o : F.Occurrence) : Graph.RotationCertificate.SameComponent (polygonGraph F) (List.idxOf o.var F.distinctVars) (List.idxOf (argumentSuccessor o).var F.distinctVars)

Consecutive scope positions are connected by their actual listed polygon edge, including when its endpoints coincide.

theorem Cslib.Complexity.CSP.polygon_sameComponent_constraint {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (o p : F.Occurrence) (h : o.fst = p.fst) : Graph.RotationCertificate.SameComponent (polygonGraph F) (List.idxOf o.var F.distinctVars) (List.idxOf p.var F.distinctVars)

All arguments of one constraint lie in the same polygon component. This includes unary and repeated-variable scopes and does not identify different constraint positions.

theorem Cslib.Complexity.CSP.polygon_sameComponent_of_incidence {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (o p : F.Occurrence) (h : Graph.RotationCertificate.SameComponent (incidenceGraph F) (List.idxOf o.var F.distinctVars) (List.idxOf p.var F.distinctVars)) : Graph.RotationCertificate.SameComponent (polygonGraph F) (List.idxOf o.var F.distinctVars) (List.idxOf p.var F.distinctVars)

Every incidence path between occurring variables becomes a polygon path.

theorem Cslib.Complexity.CSP.incidence_sameComponent_polygonEdge {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (o : F.Occurrence) : Graph.RotationCertificate.SameComponent (incidenceGraph F) (List.idxOf o.var F.distinctVars) (List.idxOf (argumentSuccessor o).var F.distinctVars)

The two variables of a polygon edge are connected through its original constraint star.

theorem Cslib.Complexity.CSP.incidence_sameComponent_of_polygon {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} {u v : ℕ} (h : Graph.RotationCertificate.SameComponent (polygonGraph F) u v) : Graph.RotationCertificate.SameComponent (incidenceGraph F) u v

Every polygon path lifts to an incidence path, using the two original star edges for each listed polygon edge.

theorem Cslib.Complexity.CSP.exists_occurrence_dense {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (v : ℕ) (hv : v < F.numVars) : ∃ (o : F.Occurrence), List.idxOf o.var F.distinctVars = v

Every dense variable vertex has an actual occurrence, even with enormous sparse source names. No finite universe of source variables is required.

theorem Cslib.Complexity.CSP.sameComponent_polygon_iff {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} {u v : ℕ} (hu : u < F.numVars) (hv : v < F.numVars) : Graph.RotationCertificate.SameComponent (polygonGraph F) u v ↔ Graph.RotationCertificate.SameComponent (incidenceGraph F) u v

Exact component correspondence on all dense variable vertices.

noncomputable def Cslib.Complexity.CSP.polygonComponentMap {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) : (polygonGraph F).induced.ConnectedComponent → (incidenceGraph F).induced.ConnectedComponent

The inclusion of dense variable vertices induces the actual map of graph components.

theorem Cslib.Complexity.CSP.polygonComponentMap_injective {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) : Function.Injective (polygonComponentMap F)

Distinct polygon components remain distinct incidence components.

theorem Cslib.Complexity.CSP.polygonComponentMap_surjective {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (hPos : ∀ (i : Fin (List.length F)), 0 < F[↑i].2.length) : Function.Surjective (polygonComponentMap F)

Positive scopes ensure that no incidence component consists of a deleted nullary constraint vertex. Thus every incidence component contains a polygon vertex.

noncomputable def Cslib.Complexity.CSP.polygonComponentEquiv {Rel V : Type} [DecidableEq V] (F : Logic.PL.CSP Rel V) (hPos : ∀ (i : Fin (List.length F)), 0 < F[↑i].2.length) : (polygonGraph F).induced.ConnectedComponent ≃ (incidenceGraph F).induced.ConnectedComponent

Exact component bijection for positive scopes, including disconnected and empty bodies.