Cyclic differences of Boolean tuples

The cyclic difference records the exclusive or of each coordinate and its successor, including the last-to-first edge. This is the tuple operation in [KKR18], Definition 14 (arXiv v6, printed p. 0:6). Coordinates remain ordered; no symmetry of a relation is assumed. The empty tuple is included, and every cyclic difference has even parity.

Main definitions

• Cslib.BitString.cyclicDifference: neighboring exclusive ors around the coordinate cycle.
• Cslib.BitString.cyclicIntegral: prefix-sum inverse on even-parity tuples.
• Cslib.BitString.IsSelfComplementary, Cslib.BitString.cyclicDifferenceRelation: relational API.

Main results

• Cslib.BitString.cyclicDifference_not: complementing a tuple preserves its differences.
• Cslib.BitString.cyclicDifference_add: cyclic differences are linear over the Boolean ring.
• Cslib.BitString.parityOn_cyclicDifference: every cyclic difference has even parity.
• Cslib.BitString.cyclicDifference_eq_iff: fibers consist of a tuple and its complement.
• Cslib.BitString.exists_cyclicDifference_eq_iff: image is exactly the even-parity tuples.
• Cslib.BitString.mem_cyclicDifferenceRelation_iff: recover a self-complementary relation.

def Cslib.BitString.cyclicDifference {n : ℕ} (x : Fin n → Bool) : Fin n → Bool

Exclusive ors of neighboring coordinates, with cyclic last-to-first adjacency.

theorem Cslib.BitString.cyclicDifference_eq_add {n : ℕ} (x : Fin n → Bool) : cyclicDifference x = x + fun (i : Fin n) => x ((finRotate n) i)

Cyclic differences are the sum of a tuple and its one-step cyclic shift.

theorem Cslib.BitString.cyclicDifference_const (n : ℕ) (b : Bool) : (cyclicDifference fun (x : Fin n) => b) = fun (x : Fin n) => false

Constant tuples have zero cyclic difference, including at arity zero.

theorem Cslib.BitString.cyclicDifference_not {n : ℕ} (x : Fin n → Bool) : (cyclicDifference fun (i : Fin n) => !x i) = cyclicDifference x

Complementary tuples have identical cyclic differences.

theorem Cslib.BitString.cyclicDifference_add {n : ℕ} (x y : Fin n → Bool) : cyclicDifference (x + y) = cyclicDifference x + cyclicDifference y

Taking cyclic differences is linear over the Boolean ring.

theorem Cslib.BitString.parityOn_cyclicDifference {n : ℕ} (x : Fin n → Bool) : parityOn Finset.univ (cyclicDifference x) = false

A cyclic difference has an even number of true coordinates.

theorem Cslib.BitString.cyclicDifference_eq_zero_iff {n : ℕ} (x : Fin n → Bool) : (cyclicDifference x = fun (x : Fin n) => false) ↔ ∃ (b : Bool), x = fun (x : Fin n) => b

Zero differences force a tuple to be constant. The empty tuple is included.

theorem Cslib.BitString.cyclicDifference_eq_iff {n : ℕ} (x y : Fin n → Bool) : cyclicDifference x = cyclicDifference y ↔ x = y ∨ x = fun (i : Fin n) => !y i

The only ambiguity in recovering a tuple from its cyclic differences is complementation.

def Cslib.BitString.cyclicIntegral {n : ℕ} (d : Fin n → Bool) : Fin n → Bool

Recover a tuple with initial value zero by summing preceding cyclic differences.

theorem Cslib.BitString.cyclicIntegral_succ {n : ℕ} (d : Fin (n + 1) → Bool) (i : Fin n) : cyclicIntegral d i.succ = (d i.castSucc ^^ cyclicIntegral d i.castSucc)

The prefix sum changes by the bit at the newly included coordinate.

@[simp]

theorem Cslib.BitString.cyclicIntegral_zero {n : ℕ} (d : Fin (n + 1) → Bool) : cyclicIntegral d 0 = false

The prefix sum starts at zero.

theorem Cslib.BitString.cyclicDifference_cyclicIntegral {n : ℕ} (d : Fin n → Bool) (hd : parityOn Finset.univ d = false) : cyclicDifference (cyclicIntegral d) = d

Every even-parity tuple is the cyclic difference of its prefix-sum tuple.

theorem Cslib.BitString.exists_cyclicDifference_eq_iff {n : ℕ} (d : Fin n → Bool) : (∃ (x : Fin n → Bool), cyclicDifference x = d) ↔ parityOn Finset.univ d = false

The image of cyclic difference is exactly the even-parity tuples, including arity zero.

def Cslib.BitString.IsSelfComplementary {ι : Type u_1} (R : Set (ι → Bool)) : Prop

Invariance of a Boolean relation under simultaneous complementation of all coordinates. This is Definition 13 of [KKR18], with empty relations allowed.

def Cslib.BitString.cyclicDifferenceRelation {n : ℕ} (R : Set (Fin n → Bool)) : Set (Fin n → Bool)

The relation of cyclic differences, retaining the original coordinate order.

theorem Cslib.BitString.cyclicDifferenceRelation_nonempty_iff {n : ℕ} (R : Set (Fin n → Bool)) : (cyclicDifferenceRelation R).Nonempty ↔ R.Nonempty

Cyclic differences preserve nonemptiness of relations.

theorem Cslib.BitString.parityOn_mem_cyclicDifferenceRelation {n : ℕ} {R : Set (Fin n → Bool)} {d : Fin n → Bool} (hd : d ∈ cyclicDifferenceRelation R) : parityOn Finset.univ d = false

Every tuple of a cyclic-difference relation has even parity.

theorem Cslib.BitString.mem_cyclicDifferenceRelation_iff {n : ℕ} {R : Set (Fin n → Bool)} (hR : IsSelfComplementary R) (x : Fin n → Bool) : cyclicDifference x ∈ cyclicDifferenceRelation R ↔ x ∈ R

A self-complementary relation is recovered exactly from its cyclic differences.

theorem Cslib.BitString.isSelfComplementary_preimage_cyclicDifference {n : ℕ} (S : Set (Fin n → Bool)) : IsSelfComplementary (cyclicDifference ⁻¹' S)

The preimage of any difference relation is self-complementary.