One-in-three gadgets over the original Boolean language

Interpret the construction trees from NonSelfDual.witnesses, then append the actual ternary body and three copies of the actual NAND body on (0,1), (1,2), (2,0). Each occurrence has fresh auxiliaries. No macro symbols, pins or disequality symbols are added to the language.

The minor mathematics and triangle semantics are reused from the original reconstruction of [DK15], Lemma 4, printed pp. 438–439. This endpoint establishes equality-free primitive-positive definability only. Geometric realization, native reduction and the full planar dichotomy remain separate obligations.

def Cslib.Logic.PL.CSP.NonSelfDual.triangleGadget {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {R : Set (Fin 3 → Bool)} [DecidablePred fun (x : Fin 3 → Bool) => x ∈ R] (r : PPGadget arity sem R) (d : PPGadget arity sem RelationMinor.nand) (hz : 0 ∉ R) (hu : ∀ (i : Fin 3), Pi.single i true ∈ R) : PPGadget arity sem (BitString.oneHotRelation (Fin 3))

Expand the ordered triangle into original-language bodies. The ternary body comes first, followed by the NAND bodies on (0,1), (1,2), (2,0), with separate auxiliary blocks.

theorem Cslib.Logic.PL.CSP.NonSelfDual.exists_oneHotGadget {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} (h : ¬HasSchaeferPolymorphism arity sem) (hn : ¬HasPolymorphism arity sem fun (a : Fin 1 → Bool) => !a 0) : Nonempty (PPGadget arity sem (BitString.oneHotRelation (Fin 3)))

If the six Schaefer operations and unary complement all fail, one-in-three has an actual equality-free gadget over the original language. No constants or minor oracle are assumed.

theorem Cslib.Logic.PL.CSP.RelationMinor.exists_disequalityGadget {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} (h : ¬HasSchaeferPolymorphism arity sem) : Nonempty (PPGadget arity sem disequality)

Absence of the six Schaefer operations alone gives an original-language disequality gadget. Unary complement need not fail, so this also serves the selfcomplementary branch.