The polygon rotation from an ordered incidence rotation

The variable permutation is recovered from the supplied incidence rotation, rather than assumed. The polygon rotation replaces each variable occurrence by two consecutive darts. Its cycles are proved to be exactly the endpoint fibers of the actual listed polygon graph. This construction has no planarity, runtime or oracle premise.

Main definitions

• Cslib.Complexity.CSP.variablePermutation: recovered variable-side incidence rotation.
• Cslib.Complexity.CSP.polygonRotation: actual rotation of the listed polygon graph.

Main results

• Cslib.Complexity.CSP.sameCycle_variablePermutation: exact variable fibers.
• Cslib.Complexity.CSP.rotate_polygonDart_false, Cslib.Complexity.CSP.rotate_polygonDart_true: exact indexed successor formulas.
• Cslib.Complexity.CSP.faceNext_polygonDart_false, Cslib.Complexity.CSP.faceNext_polygonDart_true: exact black/white face successors.

noncomputable def Cslib.Complexity.CSP.variablePermutation {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (r : (incidenceGraph F).RotationSystem) : Equiv.Perm F.Occurrence

The variable permutation is induced by the actual incidence rotation. Its inverse recovers an occurrence after applying the inverse rotation, not an arbitrary cyclic ordering.

@[simp]

theorem Cslib.Complexity.CSP.rotate_incidenceDart_false {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (r : (incidenceGraph F).RotationSystem) (o : F.Occurrence) : r.rotate (incidenceDart o false) = incidenceDart ((variablePermutation r) o) false

The induced permutation reads exactly the supplied successor at variable ends.

theorem Cslib.Complexity.CSP.variablePermutation_var {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (r : (incidenceGraph F).RotationSystem) (o : F.Occurrence) : ((variablePermutation r) o).var = o.var

Variable rotation does not change the original variable name.

theorem Cslib.Complexity.CSP.sameCycle_variablePermutation {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (r : (incidenceGraph F).RotationSystem) (o p : F.Occurrence) : (variablePermutation r).SameCycle o p ↔ o.var = p.var

The induced cycles are precisely the original equal-variable fibers.

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

Coordinates pairing the two polygon darts at an occurrence's original variable. The second dart is the reverse side of the preceding scope edge.

@[simp]

theorem Cslib.Complexity.CSP.vertex_polygonBlockEquiv {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (o : F.Occurrence) (side : Bool) : ((polygonBlockEquiv F) (o, side)).vertex = List.idxOf o.var F.distinctVars

Both members of an occurrence block are at its original dense variable.

noncomputable def Cslib.Complexity.CSP.polygonRotation {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (r : (incidenceGraph F).RotationSystem) : (polygonGraph F).RotationSystem

The actual polygon rotation. At each variable, replace its recovered occurrence cycle by the blocks (p_o,q_(B⁻¹ o)). The endpoint-fiber law is a theorem of this permutation.

@[simp]

theorem Cslib.Complexity.CSP.polygonBlockEquiv_false {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (o : F.Occurrence) : (polygonBlockEquiv F) (o, false) = polygonDart o false

A variable block starts at the forward dart of its occurrence edge.

@[simp]

theorem Cslib.Complexity.CSP.polygonBlockEquiv_true {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (o : F.Occurrence) : (polygonBlockEquiv F) (o, true) = polygonDart ((Equiv.symm (argumentPermutation F)) o) true

The second member is the backward dart of the preceding scope edge.

theorem Cslib.Complexity.CSP.rotate_polygonBlock {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (r : (incidenceGraph F).RotationSystem) (x : F.Occurrence × Bool) : (polygonRotation r).rotate ((polygonBlockEquiv F) x) = (polygonBlockEquiv F) ((variablePermutation r).doubled x)

In block coordinates, the constructed successor doubles the recovered variable cycle.

@[simp]

theorem Cslib.Complexity.CSP.rotate_polygonDart_false {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (r : (incidenceGraph F).RotationSystem) (o : F.Occurrence) : (polygonRotation r).rotate (polygonDart o false) = polygonDart ((Equiv.symm (argumentPermutation F)) o) true

Exact successor at a forward polygon dart.

@[simp]

theorem Cslib.Complexity.CSP.rotate_polygonDart_true {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (r : (incidenceGraph F).RotationSystem) (o : F.Occurrence) : (polygonRotation r).rotate (polygonDart o true) = polygonDart ((variablePermutation r) ((argumentPermutation F) o)) false

Exact successor at a backward polygon dart.

@[simp]

theorem Cslib.Complexity.CSP.faceNext_polygonDart_false {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (r : (incidenceGraph F).RotationSystem) (o : F.Occurrence) : (polygonRotation r).faceNext (polygonDart o false) = polygonDart ((argumentPermutation F) o) false

Black faces traverse each actual scope in its original cyclic order.

@[simp]

theorem Cslib.Complexity.CSP.faceNext_polygonDart_true {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (r : (incidenceGraph F).RotationSystem) (o : F.Occurrence) : (polygonRotation r).faceNext (polygonDart o true) = polygonDart ((Equiv.symm (argumentPermutation F)) ((Equiv.symm (variablePermutation r)) o)) true

White faces use exactly the permutation B⁻¹ A⁻¹ on occurrences.