Ordered Boolean relation minors

Relations are the sets of tuples used by CSP.booleanRelation. Deletion uses Fin.succAbove, so surviving ports retain their order. RelationMinor.Trace records each projection, cofactor, and single-coordinate twist separately. It does not assert geometric planarity: pins and disequality must be supplied when interpreting these traces as gadgets.

The adjacent operations combine a restriction of the first two ports with immediate deletion of the first port. They are the operations of [DK15], Lemma 2, printed p. 437, with this deletion made explicit. There is no arbitrary identification or all-port intersection.

Main definitions

• Cslib.Logic.PL.CSP.RelationMinor.project: ordered existential deletion.
• Cslib.Logic.PL.CSP.RelationMinor.cofactor: pinning and ordered deletion.
• Cslib.Logic.PL.CSP.RelationMinor.twist: coordinatewise translation of a relation.
• Cslib.Logic.PL.CSP.RelationMinor.adjacent: adjacent restriction and immediate deletion.
• Cslib.Logic.PL.CSP.RelationMinor.Trace: finite ordered minor traces.

def Cslib.Logic.PL.CSP.RelationMinor.project {n : ℕ} (R : Set (Fin (n + 1) → Bool)) (j : Fin (n + 1)) : Set (Fin n → Bool)

Delete one coordinate existentially, retaining the order of all other coordinates.

def Cslib.Logic.PL.CSP.RelationMinor.cofactor {n : ℕ} (R : Set (Fin (n + 1) → Bool)) (j : Fin (n + 1)) (b : Bool) : Set (Fin n → Bool)

Fix one coordinate to b and immediately delete it.

def Cslib.Logic.PL.CSP.RelationMinor.twist {n : ℕ} (R : Set (Fin n → Bool)) (t : Fin n → Bool) : Set (Fin n → Bool)

Translate by a bit string. Since every bit string is its own inverse, this is both the image and the inverse image under translation.

def Cslib.Logic.PL.CSP.RelationMinor.adjacent {n : ℕ} (R : Set (Fin (n + 2) → Bool)) (different : Bool) : Set (Fin (n + 1) → Bool)

Restrict the first two adjacent coordinates to equality (different = false) or disequality (different = true), then immediately delete the first coordinate.

def Cslib.Logic.PL.CSP.RelationMinor.rotate {n : ℕ} (R : Set (Fin (n + 1) → Bool)) : Set (Fin (n + 1) → Bool)

Cyclically rotate the ports by one position; no arbitrary permutation is allowed.

def Cslib.Logic.PL.CSP.RelationMinor.pin (b : Bool) : Set (Fin 1 → Bool)

The unary pin relation, distinct from a unary constant operation.

def Cslib.Logic.PL.CSP.RelationMinor.disequality : Set (Fin 2 → Bool)

Ordered binary disequality.

def Cslib.Logic.PL.CSP.RelationMinor.nand : Set (Fin 2 → Bool)

Ordered binary NAND: its unique missing row is 11.

@[instance_reducible]

instance Cslib.Logic.PL.CSP.RelationMinor.instDecidablePredForallFinOfNatNatBoolMemSetPin (b : Bool) : DecidablePred fun (x : Fin 1 → Bool) => x ∈ pin b

@[instance_reducible]

instance Cslib.Logic.PL.CSP.RelationMinor.instDecidablePredForallFinOfNatNatBoolMemSetDisequality : DecidablePred fun (x : Fin 2 → Bool) => x ∈ disequality

@[instance_reducible]

instance Cslib.Logic.PL.CSP.RelationMinor.instDecidablePredForallFinOfNatNatBoolMemSetNand : DecidablePred fun (x : Fin 2 → Bool) => x ∈ nand

@[instance_reducible]

instance Cslib.Logic.PL.CSP.RelationMinor.instDecidablePredForallFinBoolMemSetProjectOfForallHAddNatOfNat {n : ℕ} (R : Set (Fin (n + 1) → Bool)) [DecidablePred fun (x : Fin (n + 1) → Bool) => x ∈ R] (j : Fin (n + 1)) : DecidablePred fun (x : Fin n → Bool) => x ∈ project R j

@[instance_reducible]

instance Cslib.Logic.PL.CSP.RelationMinor.instDecidablePredForallFinBoolMemSetCofactorOfForallHAddNatOfNat {n : ℕ} (R : Set (Fin (n + 1) → Bool)) [DecidablePred fun (x : Fin (n + 1) → Bool) => x ∈ R] (j : Fin (n + 1)) (b : Bool) : DecidablePred fun (x : Fin n → Bool) => x ∈ cofactor R j b

@[instance_reducible]

instance Cslib.Logic.PL.CSP.RelationMinor.instDecidablePredForallFinBoolMemSetTwist {n : ℕ} (R : Set (Fin n → Bool)) [DecidablePred fun (x : Fin n → Bool) => x ∈ R] (t : Fin n → Bool) : DecidablePred fun (x : Fin n → Bool) => x ∈ twist R t

@[instance_reducible]

instance Cslib.Logic.PL.CSP.RelationMinor.instDecidablePredForallFinHAddNatOfNatBoolMemSetAdjacent {n : ℕ} (R : Set (Fin (n + 2) → Bool)) [DecidablePred fun (x : Fin (n + 2) → Bool) => x ∈ R] (d : Bool) : DecidablePred fun (x : Fin (n + 1) → Bool) => x ∈ adjacent R d

@[instance_reducible]

instance Cslib.Logic.PL.CSP.RelationMinor.instDecidablePredForallFinHAddNatOfNatBoolMemSetRotate {n : ℕ} (R : Set (Fin (n + 1) → Bool)) [DecidablePred fun (x : Fin (n + 1) → Bool) => x ∈ R] : DecidablePred fun (x : Fin (n + 1) → Bool) => x ∈ rotate R

inductive Cslib.Logic.PL.CSP.RelationMinor.Trace {m : ℕ} (R : Set (Fin m → Bool)) {n : ℕ} : Set (Fin n → Bool) → Type

A finite sequence of projections, cofactors and one-coordinate twists, with the intermediate relation and its arity recorded at each step. Cofactors require pins and flips require disequality when a trace is interpreted geometrically.

• refl {m : ℕ} {R : Set (Fin m → Bool)} : Trace R R

  The empty trace.

• project {m : ℕ} {R : Set (Fin m → Bool)} {n : ℕ} {S : Set (Fin (n + 1) → Bool)} (trace : Trace R S) (j : Fin (n + 1)) : Trace R (RelationMinor.project S j)

  Append an existential deletion.

• cofactor {m : ℕ} {R : Set (Fin m → Bool)} {n : ℕ} {S : Set (Fin (n + 1) → Bool)} (trace : Trace R S) (j : Fin (n + 1)) (b : Bool) : Trace R (RelationMinor.cofactor S j b)

  Append a pin and deletion.

• flip {m : ℕ} {R : Set (Fin m → Bool)} {n : ℕ} {S : Set (Fin n → Bool)} (trace : Trace R S) (j : Fin n) : Trace R (twist S (Pi.single j true))

  Append a twist of just one port.

def Cslib.Logic.PL.CSP.RelationMinor.Trace.trans {m n : ℕ} {R : Set (Fin m → Bool)} {S : Set (Fin n → Bool)} (a : Trace R S) {k : ℕ} {T : Set (Fin k → Bool)} (b : Trace S T) : Trace R T

Concatenate two finite ordered traces.

theorem Cslib.Logic.PL.CSP.RelationMinor.twist_twist {n : ℕ} (R : Set (Fin n → Bool)) (s t : Fin n → Bool) : twist (twist R s) t = twist R (s + t)

Consecutive translations combine by addition in the Boolean cube.

noncomputable def Cslib.Logic.PL.CSP.RelationMinor.Trace.translate {m n : ℕ} {R : Set (Fin m → Bool)} {S : Set (Fin n → Bool)} (trace : Trace R S) (t : Fin n → Bool) : Trace R (twist S t)

A mask twist expands to finitely many single-port twists.

theorem Cslib.Logic.PL.CSP.RelationMinor.remove_mem_project {n : ℕ} {R : Set (Fin (n + 1) → Bool)} {a : Fin (n + 1) → Bool} (ha : a ∈ R) (j : Fin (n + 1)) : j.removeNth a ∈ project R j

Deleting a feasible tuple gives a feasible projected tuple.

theorem Cslib.Logic.PL.CSP.RelationMinor.remove_mem_cofactor {n : ℕ} {R : Set (Fin (n + 1) → Bool)} {a : Fin (n + 1) → Bool} (ha : a ∈ R) (j : Fin (n + 1)) : j.removeNth a ∈ cofactor R j (a j)

A tuple satisfying the pin survives in its cofactor.

theorem Cslib.Logic.PL.CSP.RelationMinor.single_mem_of_zero_mem_project {n : ℕ} {R : Set (Fin (n + 1) → Bool)} (hzero : 0 ∉ R) (j : Fin (n + 1)) (h : 0 ∈ project R j) : Pi.single j true ∈ R

A zero projection of a relation missing zero has only its unit-vector lift.