Finite composition of primitive-positive gadgets

Atomic gadgets preserve the original constraint's port order. Conjunction appends bodies, sharing only free ports: the left auxiliaries precede a disjoint block of right auxiliaries. These operations give finite semantics, with no geometric or computability claim.

def Cslib.Logic.PL.CSP.PPGadget.retarget {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {n : ℕ} {R S : Set (Fin n → Bool)} (g : PPGadget arity sem R) (h : ∀ (a : Fin n → Bool), a ∈ S ↔ a ∈ R) : PPGadget arity sem S

Change the target by a pointwise equivalence, retaining the exact body and auxiliaries.

def Cslib.Logic.PL.CSP.PPGadget.atom {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} (r : Rel) : PPGadget arity sem (booleanRelation arity sem r)

A single original-language constraint, with its declared free-port order and no auxiliaries. This also covers nullary constraints.

def Cslib.Logic.PL.CSP.PPGadget.conj {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {n : ℕ} {R S : Set (Fin n → Bool)} (g : PPGadget arity sem R) (h : PPGadget arity sem S) : PPGadget arity sem (R ∩ S)

Conjoin two gadgets on the same free ports. Each occurrence gets its own auxiliary block, even when the two operands are the same gadget. Body order is left then right.

@[simp]

theorem Cslib.Logic.PL.CSP.PPGadget.length_conj_body {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {n : ℕ} {R S : Set (Fin n → Bool)} (g : PPGadget arity sem R) (h : PPGadget arity sem S) : List.length (g.conj h).body = List.length g.body + List.length h.body

Conjunction keeps every constraint of both operands, in their original order.