Exact boundary-word and quotient-label transport

Positive cyclic movement swaps consecutive boundary blocks. Adjacent identification can then be used on ordinary lists with the exact selected-pair kernel on actual labels.

noncomputable def Cslib.Complexity.CSP.OrderedBoundary.Witness.rotateAppend {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} {left right : List V} (w : Witness F (left ++ right)) (hn : (left ++ right).Nodup) : Witness F (right ++ left)

Move a whole initial block to the end by positive cyclic shifts of the same body.

noncomputable def Cslib.Complexity.CSP.OrderedBoundary.Witness.identifyHead {Rel V W : Type} [DecidableEq V] [DecidableEq W] {F : Logic.PL.CSP Rel V} {x y : V} {ports : List V} (w : Witness F (x :: y :: ports)) (f : V → W) (hxy : x ≠ y) (hk : ∀ a ∈ F.vars ++ x :: y :: ports, ∀ b ∈ F.vars ++ x :: y :: ports, f a = f b ↔ Function.update id y x a = Function.update id y x b) (hn : (List.map f (y :: ports)).Nodup) : Witness (Logic.PL.CSP.relabel f F) (List.map f (y :: ports))

Adjacent identification on a literal list boundary, retaining its mapped tail order.