Substitution of free ports in primitive-positive gadgets

The conjunction is changed only by relabeling its scopes. Free labels can be identified, and selected old free ports can become fresh existential auxiliaries. Repeated scope variables are permitted. These operations assert finite semantics only, with no planarity conclusion.

theorem Cslib.Logic.PL.CSP.WellFormed.relabel {Rel : Type} {arity : Rel → ℕ} {V W : Type} {F : CSP Rel V} (h : WellFormed arity F) (f : V → W) : WellFormed arity (CSP.relabel f F)

Relabeling variables preserves each constraint's declared scope width.

def Cslib.Logic.PL.CSP.PPGadget.relabelFree {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {n m : ℕ} {R : Set (Fin n → Bool)} (g : PPGadget arity sem R) (f : Fin n → Fin m) : PPGadget arity sem {a : Fin m → Bool | a ∘ f ∈ R}

Relabel the free ports, keeping the same auxiliary labels and the same constraints. Noninjective maps perform variable identification, rather than adding an equality symbol.

def Cslib.Logic.PL.CSP.PPGadget.substitutePort {n m k : ℕ} (a : ℕ) (f : Fin n → Fin m ⊕ Fin k) : Fin n ⊕ Fin a → Fin m ⊕ Fin (k + a)

The exact variable map for substitution. The k fresh hidden labels precede the old auxiliaries; free labels are mapped by f, and every old auxiliary remains distinct.

def Cslib.Logic.PL.CSP.PPGadget.substitute {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {n m k : ℕ} {R : Set (Fin n → Bool)} (g : PPGadget arity sem R) (f : Fin n → Fin m ⊕ Fin k) : PPGadget arity sem {a : Fin m → Bool | ∃ (z : Fin k → Bool), Sum.elim a z ∘ f ∈ R}

Identify and hide free ports by the specified label map. No constraints are added or removed. The first k auxiliaries are exactly the newly hidden ports.

@[simp]

theorem Cslib.Logic.PL.CSP.PPGadget.length_relabelFree_body {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {n m : ℕ} {R : Set (Fin n → Bool)} (g : PPGadget arity sem R) (f : Fin n → Fin m) : List.length (g.relabelFree f).body = List.length g.body

Free-port relabeling retains the exact number of constraints.

@[simp]

theorem Cslib.Logic.PL.CSP.PPGadget.length_substitute_body {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {n m k : ℕ} {R : Set (Fin n → Bool)} (g : PPGadget arity sem R) (f : Fin n → Fin m ⊕ Fin k) : List.length (g.substitute f).body = List.length g.body

Hiding free ports retains the exact number of constraints.