Unary pins on the exact cofactor body

The pin's actual ordered source witness is attached at the selected free coordinate. The exact existing cofactor label map puts the hidden coordinate first, followed by the left and right old auxiliary blocks. Deleting its boundary marker gives the inherited free order, including a nullary result and completely unused original free labels.

noncomputable def Cslib.Complexity.CSP.OrderedBoundary.GadgetWitness.cofactor {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) (j : Fin (n + 1)) (b : Bool) {p : Logic.PL.CSP.PPGadget arity sem (Logic.PL.CSP.RelationMinor.pin b)} (v : GadgetWitness p) : GadgetWitness (g.cofactor j b p)

Attach an actual unary pin and hide the selected coordinate on exactly PPGadget.cofactor. The pin is an original-language gadget with its own witness, with no new relation symbol.