Attaching an ordered two-port body at any old coordinate

The remaining external port is a fresh last free name. Its boundary marker is inserted immediately before the selected old marker. This explicit boundary word need not be the canonical enlarged free order. Later hiding and identification use this actual word.

def Cslib.Complexity.CSP.OrderedBoundary.binaryAttachmentPorts (k a : ℕ) (j : Fin k) : List (Fin (k + 1) ⊕ Fin a)

The fresh last name is inserted just before old coordinate j; all old coordinates retain their order and are cast into the enlarged free block.

theorem Cslib.Complexity.CSP.OrderedBoundary.nodup_binaryAttachmentPorts (k a : ℕ) (j : Fin k) : (binaryAttachmentPorts k a j).Nodup

The explicit noncanonical enlarged boundary contains distinct actual free labels.

theorem Cslib.Complexity.CSP.OrderedBoundary.length_binaryAttachmentPorts (k a : ℕ) (j : Fin k) : (binaryAttachmentPorts k a j).length = k + 1

Exactly one fresh free marker is added to the existing k markers.

theorem Cslib.Complexity.CSP.OrderedBoundary.eraseIdx_binaryAttachmentPorts_swap (k a : ℕ) (j : Fin k) : List.map (Sum.map (⇑(Equiv.swap j.castSucc (Fin.last k))) id) ((binaryAttachmentPorts k a j).eraseIdx (↑j + 1)) = List.ofFn fun (i : Fin k) => Sum.inl i.castSucc

Remove the selected old marker after the insertion, then swap its name with the fresh last name. The remaining word is exactly the old canonical free order.

noncomputable def Cslib.Complexity.CSP.OrderedBoundary.GadgetWitness.binaryBoundary {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {S : Set (Fin 2 → Bool)} {d : Logic.PL.CSP.PPGadget arity sem S} (v : GadgetWitness d) (t : Fin 2) : Witness d.body [Sum.inl t.rev, Sum.inl t]

Source binary argument order starting with the other port and ending at the attachment. At two ports both cases are positive cyclic shifts, never a higher-arity reflection.

noncomputable def Cslib.Complexity.CSP.OrderedBoundary.GadgetWitness.attachBinary {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {k : ℕ} {R : Set (Fin k → Bool)} {S : Set (Fin 2 → Bool)} {g : Logic.PL.CSP.PPGadget arity sem R} {d : Logic.PL.CSP.PPGadget arity sem S} (w : GadgetWitness g) (v : GadgetWitness d) (j : Fin k) (t : Fin 2) : Witness (Logic.PL.CSP.relabel (attachPortLabel k g.numAux d.numAux j t) (Logic.PL.CSP.relabel Sum.inl g.body ++ Logic.PL.CSP.relabel Sum.inr d.body)) (List.take (↑j) (List.ofFn fun (i : Fin k) => Sum.inl i.castSucc) ++ Sum.inl (Fin.last k) :: List.drop (↑j) (List.ofFn fun (i : Fin k) => Sum.inl i.castSucc))

The actual boundary after attachment uses the new last name immediately before j. The body rows are exact disjoint copies followed by the proved one-pair label map.