Polymorphism preservation by actual primitive-positive bodies

The existing common-polymorphism interface acts on satisfying assignments of each literal wellformed CSP body, then on its existential auxiliary assignments. This original adapter includes repeated variable positions, empty conjunctions, nullary constraints and nullary operations. It is solely semantic: arbitrary primitive-positive definability supplies no ordered boundary or planarity conclusion.

theorem Cslib.Logic.PL.CSP.HasPolymorphism.eval {Rel : Type u_1} {V : Type u_2} {J : Type u_3} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {f : (J → Bool) → Bool} (h : HasPolymorphism arity sem f) (F : CSP Rel V) (hw : WellFormed arity F) (a : J → V → Bool) (ha : ∀ (j : J), CSP.eval sem (a j) F = true) : CSP.eval sem (fun (v : V) => f fun (j : J) => a j v) F = true

A common polymorphism preserves satisfying assignments of an actual wellformed body. Every scope is read at its declared arity; duplicate occurrences and nullaries remain literal.

theorem Cslib.Logic.PL.CSP.PPGadget.isPolymorphism {J : Type u_3} {f : (J → Bool) → Bool} {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {n : ℕ} {R : Set (Fin n → Bool)} (g : PPGadget arity sem R) (h : HasPolymorphism arity sem f) : IsPolymorphism f R

Every actual primitive-positive gadget preserves the language's common polymorphisms. This forward semantic fact includes nullary operations and makes no boundary assertion.