Constants and disequality from ordered constructions

This is the semantic descent of [DK15], Lemma 3, printed pp. 437–438. Equality restriction is always followed immediately by deletion of the first of the adjacent ports, so minimum arity suffices. Unary constant operations are kept distinct from unary pin relations. Different language symbols may witness the failures of the different polymorphisms.

The conclusions give finite RelationMinor.Construction trees, with all enabling relations constructed from original symbols. Geometric interpretation and complexity are not claimed.

Main results

• Cslib.Logic.PL.CSP.RelationMinor.disequality_of_not_hasSchaeferPolymorphism: disequality.
• Cslib.Logic.PL.CSP.RelationMinor.constants_of_not_hasSchaeferPolymorphism: both pins as well.

theorem Cslib.Logic.PL.CSP.RelationMinor.disequality_or_pin_of_missing_constant {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {m : ℕ} {R : Set (Fin m → Bool)} (hR : Available arity sem R) (b : Bool) (hne : R.Nonempty) (hz : (fun (x : Fin m) => b) ∉ R) : Available arity sem disequality ∨ Available arity sem (pin !b)

Failure of a unary constant yields disequality or the opposite unary pin, by projections and immediate adjacent equality-deletions alone. This includes arbitrary and nullary arities.

theorem Cslib.Logic.PL.CSP.RelationMinor.disequality_of_pins {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {m n : ℕ} {R : Set (Fin m → Bool)} {S : Set (Fin n → Bool)} (hR : Available arity sem R) (hS : Available arity sem S) (pins : ∀ (b : Bool), Available arity sem (pin b)) (ha : ¬IsPolymorphism (fun (a : Fin 2 → Bool) => a 0 && a 1) R) (ho : ¬IsPolymorphism (fun (a : Fin 2 → Bool) => a 0 || a 1) S) : Available arity sem disequality

With actual unary pins, separate AND and OR failures construct disequality by the specific binary intersection of Lemma 3. No ternary or unrestricted intersection is used.

theorem Cslib.Logic.PL.CSP.RelationMinor.pins_of_disequality {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} {m : ℕ} {R : Set (Fin m → Bool)} (hR : Available arity sem R) (hd : Available arity sem disequality) (h : ¬IsPolymorphism (fun (a : Fin 1 → Bool) => !a 0) R) (b : Bool) : Available arity sem (pin b)

Disequality and failure of complement construct both unary pins. Each descent uses only the first adjacent pair, with its first coordinate immediately deleted.

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

The non-Schaefer hypothesis constructs disequality from original language symbols. The ZERO/ONE witnesses and the AND/OR witnesses are selected independently.

theorem Cslib.Logic.PL.CSP.RelationMinor.constants_of_not_hasSchaeferPolymorphism {Rel : Type} {arity : Rel → ℕ} {sem : Rel → List Bool → Bool} (h : ¬HasSchaeferPolymorphism arity sem) (hn : ¬HasPolymorphism arity sem fun (a : Fin 1 → Bool) => !a 0) : Available arity sem disequality ∧ ∀ (b : Bool), Available arity sem (pin b)

Lemma 3's nonselfdual endpoint, with no adjoined-constant premise: disequality and both unary pins have finite ordered constructions from the original language. Complement, constant, AND and OR failures may belong to different symbols.