Executing ordered relation constructions as original-language gadgets

RelationMinor.Construction.gadget recursively executes the recorded recipe on actual primitive-positive bodies. Pins and disequality are interpreted from their enabling trees, so every constraint uses an original language symbol. Conjunction has disjoint auxiliary blocks, and projection hides exactly the selected port, preserving survivor order.

This is finite semantic interpretation. The intermediate conjunctions and free-port maps make no planarity assertion; geometric realization and native reductions are separate.

def Cslib.Logic.PL.CSP.PPGadget.hidePort {n : ℕ} (j : Fin (n + 1)) : Fin (n + 1) → Fin n ⊕ Fin 1

Hide one old free port as the first fresh auxiliary; survivors keep their order.

def Cslib.Logic.PL.CSP.PPGadget.project {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {n : ℕ} {R : Set (Fin (n + 1) → Bool)} (g : PPGadget arity sem R) (j : Fin (n + 1)) : PPGadget arity sem (RelationMinor.project R j)

Existential deletion uses Fin.insertNth, with one fresh auxiliary before the old block.

def Cslib.Logic.PL.CSP.PPGadget.equalDrop {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {n : ℕ} {R : Set (Fin (n + 2) → Bool)} (g : PPGadget arity sem R) : PPGadget arity sem (RelationMinor.adjacent R false)

Identify the first two ports and drop the first, without an equality symbol.

def Cslib.Logic.PL.CSP.PPGadget.differentDrop {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {n : ℕ} {R : Set (Fin (n + 2) → Bool)} (g : PPGadget arity sem R) (d : PPGadget arity sem RelationMinor.disequality) : PPGadget arity sem (RelationMinor.adjacent R true)

Attach an interpreted disequality constraint to the first pair, then hide its first port.

def Cslib.Logic.PL.CSP.PPGadget.cofactor {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {n : ℕ} {R : Set (Fin (n + 1) → Bool)} (g : PPGadget arity sem R) (j : Fin (n + 1)) (b : Bool) (p : PPGadget arity sem (RelationMinor.pin b)) : PPGadget arity sem (RelationMinor.cofactor R j b)

Attach the constructed pin at the selected coordinate, then hide that coordinate.

def Cslib.Logic.PL.CSP.PPGadget.flipPort {n : ℕ} (j i : Fin n) : Fin (n + 1)

Move the selected old coordinate to a temporary last free port; all other old ports keep their indices, cast into the enlarged free block.

def Cslib.Logic.PL.CSP.PPGadget.flip {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {n : ℕ} {R : Set (Fin n → Bool)} (g : PPGadget arity sem R) (j : Fin n) (d : PPGadget arity sem RelationMinor.disequality) : PPGadget arity sem (RelationMinor.twist R (Pi.single j true))

Attach constructed disequality between the newly exposed coordinate and the old hidden coordinate. The temporary last port is then hidden before all existing auxiliaries.

def Cslib.Logic.PL.CSP.RelationMinor.Construction.gadget {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {n : ℕ} {R : Set (Fin n → Bool)} (c : Construction arity sem R) : PPGadget arity sem R

Execute every node of an ordered construction on actual original-language gadget bodies. The defining equations retain the operation recipe, including all enabling trees.

theorem Cslib.Logic.PL.CSP.RelationMinor.Available.nonempty_ppGadget {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {n : ℕ} {R : Set (Fin n → Bool)} (h : Available arity sem R) : Nonempty (PPGadget arity sem R)

A finite construction gives an actual gadget over the original language.