Cyclic rotation of the existing original-language gadget constructor

The boundary moves backwards before the actual free labels move forwards. The resulting canonical free-port word is distinct and in its inherited positive order. The body is exactly PPGadget.relabelFree (fun i => i + 1), as used by Construction.gadget; no reflection or new relation symbol is used. These are static finite realization constructions, with no uniform preprocessing-time assertion.

noncomputable def Cslib.Complexity.CSP.OrderedBoundary.GadgetWitness.rotate {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {n : ℕ} {R : Set (Fin (n + 1) → Bool)} {g : Logic.PL.CSP.PPGadget arity sem R} (w : GadgetWitness g) : GadgetWitness (g.relabelFree fun (i : Fin (n + 1)) => i + 1)

Cyclically rotate the exact existing semantic gadget body and canonical free ports. Both the inherited boundary order and its distinctness are discharged internally.