Cyclic transport of actual ordered boundaries

The structural probe is reindexed by the opposite cyclic shift, preserving the original clockwise argument rotations. The source and target actual bodies are identical. Numerical genus and complete target certificate acceptance follow internally from occurrence transport and probe removal. The distinct-boundary guard is explicit; closed components and nullaries remain present, including at arity zero. These are original finite structural constructions.

noncomputable def Cslib.Complexity.CSP.OrderedBoundary.Witness.rotateOfFn {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} {n : ℕ} {v : Fin n → V} (w : Witness F (List.ofFn v)) (hn : (List.ofFn v).Nodup) : Witness F (List.ofFn (v ∘ ⇑(finRotate n)))

Cyclically shift a distinct named boundary one step forwards, retaining the literal body. The probe uses the opposite directed shift, not a reflected argument rotation.

noncomputable def Cslib.Complexity.CSP.OrderedBoundary.Witness.unrotateOfFn {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} {n : ℕ} {v : Fin n → V} (w : Witness F (List.ofFn v)) (hn : (List.ofFn v).Nodup) : Witness F (List.ofFn (v ∘ ⇑(Equiv.symm (finRotate n))))

Cyclically shift a distinct named boundary one step backwards. Arity zero and one, unused ports, arbitrary body degree and closed components need no separate provider.