Positional deletion in the actual ordered boundary word

Cyclic probe transport moves a selected marker to the front, actual edge deletion removes it, and inverse transport restores the inherited survivor order. The body is unchanged. Boundary distinctness is explicit and preserved through these constructors. All steps construct actual checked incidence tables internally; no target-embedding provider is used. The preprocessing is finite and static, with no uniform runtime assertion.

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

Move the first distinct boundary marker to the end by a positive cyclic shift.

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

Move the final distinct boundary marker to the front by the inverse cyclic shift.

noncomputable def Cslib.Complexity.CSP.OrderedBoundary.Witness.forgetAt {Rel V : Type} [DecidableEq V] (k : ℕ) {F : Logic.PL.CSP Rel V} {ports : List V} (w : Witness F ports) (hn : ports.Nodup) (hk : k < ports.length) : Witness F (ports.eraseIdx k)

Delete any selected distinct boundary position, retaining the precise original order of every survivor. The original body, including closed/nullary components, is unchanged. The recursion is on the actual valid position; this is static template preprocessing.