Ordered minors for nonselfdual Boolean languages

The arbitrary-arity parity and majority minor arguments are an original reconstruction of the expressibility argument omitted after Lemma 4 of [DK15], printed pp. 438–439. They are not attributed to a printed proof of that lemma. All relations use the existing CSP.booleanRelation/IsPolymorphism interface. Traces preserve survivor order. These are finite semantic constructions; geometric realization, native reduction, runtime and planar hardness are separate obligations.

Main results

• Cslib.Logic.PL.CSP.RelationMinor.exists_majority_minor: a normalized ternary majority failure.
• Cslib.Logic.PL.CSP.RelationMinor.exists_binary_parity_minor: a binary parity failure.
• Cslib.Logic.PL.CSP.RelationMinor.exists_nand_trace: an actual ordered trace to NAND.

theorem Cslib.Logic.PL.CSP.RelationMinor.parity_preserves_of_arity_le_one {n : ℕ} {R : Set (Fin n → Bool)} (hn : n ≤ 1) : IsPolymorphism (parity 3) R

Every relation of arity at most one is preserved by ternary parity, including empty and nullary relations.

theorem Cslib.Logic.PL.CSP.RelationMinor.majority_preserves_of_arity_le_two {n : ℕ} {R : Set (Fin n → Bool)} (hn : n ≤ 2) : IsPolymorphism (majority 3) R

Every relation of arity at most two is majority-preserved, including empty and nullary relations. The finite check concerns the operation's two-coordinate selector law only.

theorem Cslib.Logic.PL.CSP.RelationMinor.units_of_projection_closure {n : ℕ} {R : Set (Fin (n + 1) → Bool)} {k : ℕ} {f : (Fin k → Bool) → Bool} (hz : 0 ∉ R) (a : Fin k → Fin (n + 1) → Bool) (ha : ∀ (j : Fin k), a j ∈ R) (hout : (fun (i : Fin (n + 1)) => f fun (j : Fin k) => a j i) = 0) (hp : ∀ (j : Fin (n + 1)), IsPolymorphism f (project R j)) (j : Fin (n + 1)) : Pi.single j true ∈ R

If a projected zero output is forced by closure, its unique feasible lift is the unit at the deleted port. This works for any operation fixing the constant zero input.

theorem Cslib.Logic.PL.CSP.RelationMinor.mem_of_cofactor_closure {n : ℕ} {R : Set (Fin (n + 1) → Bool)} {k : ℕ} {f : (Fin k → Bool) → Bool} {j : Fin (n + 1)} {b : Bool} (hf : (f fun (x : Fin k) => b) = b) (h : IsPolymorphism f (cofactor R j b)) (a : Fin k → Fin (n + 1) → Bool) (ha : ∀ (i : Fin k), a i ∈ R) (hb : ∀ (i : Fin k), a i j = b) : (fun (i : Fin (n + 1)) => f fun (k : Fin k) => a k i) ∈ R

Cofactor closure applied to tuples sharing the pinned bit, lifted back to the original relation. The operation must fix that constant bit.

theorem Cslib.Logic.PL.CSP.RelationMinor.exists_majority_minor {m : ℕ} {R : Set (Fin m → Bool)} (h : ¬IsPolymorphism (majority 3) R) : ∃ (S : Set (Fin 3 → Bool)), Nonempty (Trace R S) ∧ 0 ∉ S ∧ ∀ (i : Fin 3), Pi.single i true ∈ S

A majority failure has an actual ordered ternary minor containing the three units and missing zero. This original reconstruction works at every starting arity; it assumes neither pins as language symbols nor a minor oracle. Interpreting cofactors as gadgets still needs pins.

theorem Cslib.Logic.PL.CSP.RelationMinor.exists_binary_parity_minor {m : ℕ} {R : Set (Fin m → Bool)} (h : ¬IsPolymorphism (parity 3) R) : ∃ (S : Set (Fin 2 → Bool)), Nonempty (Trace R S) ∧ ¬IsPolymorphism (parity 3) S ∧ 0 ∉ S ∧ ∀ (i : Fin 2), Pi.single i true ∈ S

Every parity-failing Boolean relation has a binary parity-failing ordered minor. This arbitrary-arity reconstruction uses actual projection/cofactor/twist traces. Affine separation is used only to prove the even-tuple cancellation step, not as a gadget or minor oracle.

theorem Cslib.Logic.PL.CSP.RelationMinor.binary_parity_failure_eq {S : Set (Fin 2 → Bool)} (h : ¬IsPolymorphism (parity 3) S) (hz : 0 ∉ S) (hu : ∀ (i : Fin 2), Pi.single i true ∈ S) : S = {x : Fin 2 → Bool | x ≠ 0}

A normalized binary parity failure has exactly the three nonzero tuples. In particular the minimum-failure argument has not produced an empty or two-tuple relation.

theorem Cslib.Logic.PL.CSP.RelationMinor.exists_nand_trace {m : ℕ} {R : Set (Fin m → Bool)} (h : ¬IsPolymorphism (parity 3) R) : Nonempty (Trace R nand)

Every relation failing ternary parity has an actual finite ordered trace to NAND. Only projections, cofactors and single-port twists occur in the returned trace.