Complete black and white face correspondence

For positive actual scopes, every constraint position is one black face. Every remaining face is white and corresponds to exactly one incidence face. Singleton orbits are retained. These are combinatorial orbit correspondences; no geometric or algorithmic premise is used.

Main definitions

• Cslib.Complexity.CSP.polygonFaceEquiv: full black/white face decomposition.
• Cslib.Complexity.CSP.blackFace, Cslib.Complexity.CSP.whiteFace: its indexed inclusions.

Main results

• Cslib.Complexity.CSP.polygonFaceEquiv_black: exact constraint-position map.
• Cslib.Complexity.CSP.polygonFaceEquiv_white: exact incidence-face conjugation.
• Cslib.Complexity.CSP.polygon_edge_faces_distinct: two different faces at each edge.

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

The square of the incidence face successor, expressed on variable occurrences: A⁻¹ B⁻¹.

@[simp]

theorem Cslib.Complexity.CSP.faceNext_incidenceDart_false {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (r : (incidenceGraph F).RotationSystem) (hOrder : RespectsArgumentOrder r) (o : F.Occurrence) : r.faceNext (incidenceDart o false) = incidenceDart ((Equiv.symm (argumentPermutation F)) o) true

The incidence face successor leaves a variable end through the previous argument end.

@[simp]

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

From a constraint end, the face successor uses the inverse recovered variable cycle.

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

Coordinates pairing each variable dart with its following incidence-face dart.

@[simp]

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

The first member is the original variable dart.

@[simp]

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

The second member is the preceding argument's constraint dart.

theorem Cslib.Complexity.CSP.faceNext_incidenceBlock {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (r : (incidenceGraph F).RotationSystem) (hOrder : RespectsArgumentOrder r) (x : F.Occurrence × Bool) : r.faceNext ((incidenceBlockEquiv F) x) = (incidenceBlockEquiv F) ((incidenceSquarePermutation r).doubled x)

Every incidence face alternates the two endpoint sides. Its full permutation is the explicit doubled square permutation, after changing to these coordinates.

noncomputable def Cslib.Complexity.CSP.incidenceFaceOrbitEquiv {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (r : (incidenceGraph F).RotationSystem) (hOrder : RespectsArgumentOrder r) : r.Face ≃ Quotient (Equiv.Perm.SameCycle.setoid (incidenceSquarePermutation r))

Complete incidence-face correspondence with the square permutation, including fixed points of the square. There is no selection of favorable face cycles.

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

Sum coordinates distinguish every forward black dart from every backward white dart.

@[simp]

theorem Cslib.Complexity.CSP.polygonSumEquiv_inl {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (o : F.Occurrence) : (polygonSumEquiv F) (Sum.inl o) = polygonDart o false

Black coordinates are forward edge ends.

@[simp]

theorem Cslib.Complexity.CSP.polygonSumEquiv_inr {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (o : F.Occurrence) : (polygonSumEquiv F) (Sum.inr o) = polygonDart ((Equiv.symm (argumentPermutation F)) o) true

White coordinates use the preceding scope edge.

theorem Cslib.Complexity.CSP.faceNext_polygonSum {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (r : (incidenceGraph F).RotationSystem) (x : F.Occurrence ⊕ F.Occurrence) : (polygonRotation r).faceNext ((polygonSumEquiv F) x) = (polygonSumEquiv F) ((Equiv.sumCongr (argumentPermutation F) (incidenceSquarePermutation r)) x)

The polygon face permutation splits completely into black scope cycles and white incidence-square cycles.

noncomputable def Cslib.Complexity.CSP.polygonFaceOrbitEquiv {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (r : (incidenceGraph F).RotationSystem) : (polygonRotation r).Face ≃ Quotient (Equiv.Perm.SameCycle.setoid (argumentPermutation F)) ⊕ Quotient (Equiv.Perm.SameCycle.setoid (incidenceSquarePermutation r))

The full polygon face quotient is the disjoint sum of its black and white orbit quotients. In particular, no singleton or white face is omitted.

noncomputable def Cslib.Complexity.CSP.argumentOrbitEquiv {Rel V : Type} (F : Logic.PL.CSP Rel V) (hPos : ∀ (i : Fin (List.length F)), 0 < F[↑i].2.length) : Quotient (Equiv.Perm.SameCycle.setoid (argumentPermutation F)) ≃ Fin (List.length F)

Every positive constraint position, including duplicate constraint records, has exactly one scope orbit. Nullary constraints are explicitly excluded by the hypothesis.

noncomputable def Cslib.Complexity.CSP.polygonFaceEquiv {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (r : (incidenceGraph F).RotationSystem) (hOrder : RespectsArgumentOrder r) (hPos : ∀ (i : Fin (List.length F)), 0 < F[↑i].2.length) : (polygonRotation r).Face ≃ Fin (List.length F) ⊕ r.Face

Full face decomposition of the actual constructed rotation: one black face per indexed positive scope, and one white face per incidence face.

theorem Cslib.Complexity.CSP.polygonFaceEquiv_black {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (r : (incidenceGraph F).RotationSystem) (hOrder : RespectsArgumentOrder r) (hPos : ∀ (i : Fin (List.length F)), 0 < F[↑i].2.length) (o : F.Occurrence) : (polygonFaceEquiv r hOrder hPos) ⟦polygonDart o false⟧ = Sum.inl o.fst

The black face of an occurrence is indexed by its actual constraint position.

theorem Cslib.Complexity.CSP.incidenceFaceOrbitEquiv_mk_false {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (r : (incidenceGraph F).RotationSystem) (hOrder : RespectsArgumentOrder r) (o : F.Occurrence) : (incidenceFaceOrbitEquiv r hOrder) ⟦incidenceDart o false⟧ = ⟦o⟧

The variable dart represents its own square orbit in the incidence-face correspondence.

theorem Cslib.Complexity.CSP.polygonFaceEquiv_white {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (r : (incidenceGraph F).RotationSystem) (hOrder : RespectsArgumentOrder r) (hPos : ∀ (i : Fin (List.length F)), 0 < F[↑i].2.length) (o : F.Occurrence) : (polygonFaceEquiv r hOrder hPos) ⟦polygonDart ((Equiv.symm (argumentPermutation F)) o) true⟧ = Sum.inr ⟦incidenceDart o false⟧

The exact white correspondence sends q_(B⁻¹ o) to the face of the original variable dart o. This states the conjugation, not merely an equality of face counts.

theorem Cslib.Complexity.CSP.polygon_edge_faces_distinct {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (r : (incidenceGraph F).RotationSystem) (hOrder : RespectsArgumentOrder r) (hPos : ∀ (i : Fin (List.length F)), 0 < F[↑i].2.length) (o : F.Occurrence) : ⟦polygonDart o false⟧ ≠ ⟦polygonDart o true⟧

Each edge has distinct black and white incident faces, even for a listed loop.

noncomputable def Cslib.Complexity.CSP.blackFace {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (r : (incidenceGraph F).RotationSystem) (hOrder : RespectsArgumentOrder r) (hPos : ∀ (i : Fin (List.length F)), 0 < F[↑i].2.length) (i : Fin (List.length F)) : (polygonRotation r).Face

The black face at an actual constraint position. Positive scopes provide its darts.

noncomputable def Cslib.Complexity.CSP.whiteFace {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (r : (incidenceGraph F).RotationSystem) (hOrder : RespectsArgumentOrder r) (hPos : ∀ (i : Fin (List.length F)), 0 < F[↑i].2.length) (f : r.Face) : (polygonRotation r).Face

The white face corresponding to an original incidence face.

theorem Cslib.Complexity.CSP.blackFace_eq_mk {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (r : (incidenceGraph F).RotationSystem) (hOrder : RespectsArgumentOrder r) (hPos : ∀ (i : Fin (List.length F)), 0 < F[↑i].2.length) (o : F.Occurrence) : blackFace r hOrder hPos o.fst = ⟦polygonDart o false⟧

Every argument dart of a constraint represents its indexed black face.

theorem Cslib.Complexity.CSP.whiteFace_eq_mk {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (r : (incidenceGraph F).RotationSystem) (hOrder : RespectsArgumentOrder r) (hPos : ∀ (i : Fin (List.length F)), 0 < F[↑i].2.length) (o : F.Occurrence) : whiteFace r hOrder hPos ⟦incidenceDart o false⟧ = ⟦polygonDart ((Equiv.symm (argumentPermutation F)) o) true⟧

A variable dart's incidence face gives the white face on the preceding polygon edge.

theorem Cslib.Complexity.CSP.exists_blackFace_or_whiteFace {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (r : (incidenceGraph F).RotationSystem) (hOrder : RespectsArgumentOrder r) (hPos : ∀ (i : Fin (List.length F)), 0 < F[↑i].2.length) (f : (polygonRotation r).Face) : (∃ (i : Fin (List.length F)), blackFace r hOrder hPos i = f) ∨ ∃ (w : r.Face), whiteFace r hOrder hPos w = f

Every face is covered by the indexed black or white map.