Cofacial variable corners from consecutive directed arguments

Two consecutive constraint arguments determine cofacial variable-side corners, one at the later argument and one immediately before the earlier argument in its variable rotation. The two literal face steps derive cofaciality from the original clockwise argument order. Repeated variables and other boundary visits are permitted; distinctness is a separate condition when a later operation merges the selected vertices. These identities are original.

theorem Cslib.Complexity.CSP.side_rotate_symm_variable {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (rho : (incidenceGraph F).RotationSystem) (o : F.Occurrence) : ((Equiv.symm rho.rotate) (incidenceDart o false)).2 = false

A predecessor in a variable's actual cyclic rotation is still on the variable side. No injectivity of variable labels or bound on the degree is required.

theorem Cslib.Complexity.CSP.faceNext_variable_of_argumentSuccessor {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (rho : (incidenceGraph F).RotationSystem) (ho : RespectsArgumentOrder rho) (o p : F.Occurrence) (hp : argumentSuccessor p = o) : rho.faceNext (incidenceDart o false) = incidenceDart p true

With the existing face convention, the later argument's variable corner reaches the earlier argument's constraint end in one face step. This uses the directed argument cycle.

theorem Cslib.Complexity.CSP.sameCycle_variable_corners_of_argumentSuccessor {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (rho : (incidenceGraph F).RotationSystem) (ho : RespectsArgumentOrder rho) (o p : F.Occurrence) (hp : argumentSuccessor p = o) : rho.faceNext.SameCycle (incidenceDart o false) ((Equiv.symm rho.rotate) (incidenceDart p false))

Consecutive ordered arguments supply cofacial variable corners internally: the later argument end and the predecessor of the earlier variable end are two face steps apart. The theorem also covers repeated labels and coincident corners without inventing a dart.