Disequality deletion on the exact original-language body

Attach the first disequality port at old coordinate zero using different components, hide that boundary marker, and identify the remaining consecutive pair. The two joins derive their own component/cofacial guards. The auxiliary blocks are precisely those of the existing differentDrop interpreter, with the hidden old coordinate first.

noncomputable def Cslib.Complexity.CSP.OrderedBoundary.GadgetWitness.differentDrop {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {n : ℕ} {R : Set (Fin (n + 2) → Bool)} {g : Logic.PL.CSP.PPGadget arity sem R} {d : Logic.PL.CSP.PPGadget arity sem Logic.PL.CSP.RelationMinor.disequality} (w : GadgetWitness g) (v : GadgetWitness d) : GadgetWitness (g.differentDrop d)

The existing first-pair disequality deletion has an actual ordered numerical witness on exactly its original body. No pin, disequality or target-genus provider remains beyond the supplied actual source gadget witnesses.