Binary intersection on the exact appended gadget body

Two ordered binary boundaries share their ports in the two-digon arrangement. The first join uses disjoint components, and the remaining adjacent markers supply the cofacial second join. The body is precisely PPGadget.conj, with left then right auxiliary blocks. The result is restricted to arity two; no general all-port conjunction is asserted.

noncomputable def Cslib.Complexity.CSP.OrderedBoundary.GadgetWitness.binaryMeet {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {R S : Set (Fin 2 → Bool)} {g : Logic.PL.CSP.PPGadget arity sem R} {h : Logic.PL.CSP.PPGadget arity sem S} (w : GadgetWitness g) (v : GadgetWitness h) : GadgetWitness (g.conj h)

Actual arity-two conjunction has its own checked ordered numerical witness, with exact original body rows and disjoint auxiliary blocks. Every join guard is derived internally.