The ordered NAND triangle for one-in-three

The original reconstruction here combines a ternary relation containing all units and missing zero with NAND on its three cyclic adjacent pairs. The target is the existing BitString.oneHotRelation (Fin 3). It gives an actual four-constraint CSP.PPGadget, in exposed order 0,1,2. NonSelfDual.witnesses derives the required relations from independently selected language symbols, without assuming constants in the language.

[DK15], Lemma 4, printed pp. 438–439, states the planar expressibility conclusion without its proof. The arbitrary-arity minor arguments and this triangle are original reconstructions, not the omitted printed proof. Geometric interpretation of the finite construction trees, substitution into a plane instance, hardness and runtime remain separate.

Main definitions

• Cslib.Logic.PL.CSP.NonSelfDual.triangle: the actual four-constraint macro gadget.

Main results

• Cslib.Logic.PL.CSP.NonSelfDual.witnesses: derive its macros without a constants premise.

inductive Cslib.Logic.PL.CSP.NonSelfDual.TriangleSymbol : Type

The two macros in the triangle: its ordered ternary relation and binary NAND.

• relation : TriangleSymbol

  The given ternary relation.

• nand : TriangleSymbol

  Binary NAND.

@[instance_reducible]

instance Cslib.Logic.PL.CSP.NonSelfDual.instDecidableEqTriangleSymbol : DecidableEq TriangleSymbol

def Cslib.Logic.PL.CSP.NonSelfDual.triangleArity : TriangleSymbol → ℕ

The widths of the triangle macros.

def Cslib.Logic.PL.CSP.NonSelfDual.triangleSem (R : Set (Fin 3 → Bool)) [DecidablePred fun (x : Fin 3 → Bool) => x ∈ R] : TriangleSymbol → List Bool → Bool

Exact-width interpretation of the triangle macros.

def Cslib.Logic.PL.CSP.NonSelfDual.triangleBody : CSP TriangleSymbol (Fin 3 ⊕ Fin 0)

The ordered inner ternary face and three cyclic binary digons. All three variables are free; there are no macro auxiliary variables. The last binary scope is (2,0).

theorem Cslib.Logic.PL.CSP.NonSelfDual.triangleBody_wellFormed : WellFormed triangleArity triangleBody

The four macro constraints have exactly their declared widths.

theorem Cslib.Logic.PL.CSP.NonSelfDual.triangleBody_eval_iff (R : Set (Fin 3 → Bool)) [DecidablePred fun (x : Fin 3 → Bool) => x ∈ R] (x : Fin 3 → Bool) (b : Fin 0 → Bool) : eval (triangleSem R) (Sum.elim x b) triangleBody = true ↔ x ∈ R ∧ (x = 0 ∨ x ∈ BitString.oneHotRelation (Fin 3))

NAND on all three adjacent pairs leaves precisely the three units or zero.

def Cslib.Logic.PL.CSP.NonSelfDual.triangle (R : Set (Fin 3 → Bool)) [DecidablePred fun (x : Fin 3 → Bool) => x ∈ R] (hz : 0 ∉ R) (hu : ∀ (i : Fin 3), Pi.single i true ∈ R) : PPGadget triangleArity (triangleSem R) (BitString.oneHotRelation (Fin 3))

The actual four-constraint triangle defines one-in-three for every ternary relation containing the units and missing zero. No symmetry of that relation is assumed.

theorem Cslib.Logic.PL.CSP.NonSelfDual.witnesses {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} (h : ¬HasSchaeferPolymorphism arity sem) (hn : ¬HasPolymorphism arity sem fun (a : Fin 1 → Bool) => !a 0) : RelationMinor.Available arity sem RelationMinor.disequality ∧ (∀ (b : Bool), RelationMinor.Available arity sem (RelationMinor.pin b)) ∧ RelationMinor.Available arity sem RelationMinor.nand ∧ ∃ (R : Set (Fin 3 → Bool)), RelationMinor.Available arity sem R ∧ 0 ∉ R ∧ ∀ (i : Fin 3), Pi.single i true ∈ R

The complete semantic witnesses for the nonselfdual construction. Disequality and both pins are derived, and the parity and majority failure witnesses may be different symbols. There is no constants premise or conditional minor oracle.