Ordered boundary operations on cyclic differences

Explicit coordinate maps for adjacent identification and the two-difference cap. These are operations on Boolean tuples, with the cyclic order retained. In particular the last edge of an adjacent identification is the last-to-first edge, rather than an implicit permutation.

Main definitions

• Cslib.BitString.zeroPort: identifies the endpoints of one cyclic edge.
• Cslib.BitString.differencePort: lists the remaining difference coordinates in order.
• Cslib.BitString.capPort: identifies old ports 1 and 3 and hides old port 2.

Main results

• Cslib.BitString.mem_cyclicDifferenceRelation_zeroRestriction: exact conditioned deletion.
• Cslib.BitString.mem_cyclicDifferenceRelation_capRelation: exact cap semantics.
• Cslib.BitString.capDifferencePort_eq_zero_iff: only the first retained difference maps to zero.
• Cslib.BitString.three_le_val_capDifferencePort: every other retained difference follows the two hidden coordinates.

def Cslib.BitString.zeroPort {n : ℕ} (i j : Fin (n + 2)) : Fin (n + 1)

Identify old ports i and i+1, keeping i; at the last edge identify the last port with port 0 and keep port 0. All other free ports keep their order.

def Cslib.BitString.differencePort {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) : Fin (n + 2)

The retained difference coordinates after deleting difference i, in increasing order.

def Cslib.BitString.retainPort {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) : Fin (n + 2)

The retained original ports; this is a right inverse of zeroPort.

@[simp]

theorem Cslib.BitString.zeroPort_retainPort {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) : zeroPort i (retainPort i j) = j

Retaining ports after adjacent identification recovers the new free-port labels.

theorem Cslib.BitString.zeroPort_next {n : ℕ} (i : Fin (n + 2)) : zeroPort i ((finRotate (n + 2)) i) = zeroPort i i

The deleted edge has equal endpoint labels, including the wraparound case.

theorem Cslib.BitString.zeroPort_differencePort {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) : zeroPort i (differencePort i j) = j

Each retained edge starts at its corresponding new port.

theorem Cslib.BitString.zeroPort_next_differencePort {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) : zeroPort i ((finRotate (n + 2)) (differencePort i j)) = (finRotate (n + 1)) j

Each retained edge ends at the cyclic successor of its corresponding new port.

theorem Cslib.BitString.cyclicDifference_zeroPort {n : ℕ} (i : Fin (n + 2)) (y : Fin (n + 1) → Bool) : cyclicDifference (y ∘ zeroPort i) i = false

Adjacent identification forces exactly the deleted difference to zero.

theorem Cslib.BitString.cyclicDifference_zeroPort_differencePort {n : ℕ} (i : Fin (n + 2)) (y : Fin (n + 1) → Bool) : cyclicDifference (y ∘ zeroPort i) ∘ differencePort i = cyclicDifference y

All remaining differences are retained in their original cyclic order.

def Cslib.BitString.capPort {n : ℕ} (j : Fin (n + 4)) : Fin (n + 2) ⊕ Fin 1

Old ports 1 and 3 share new free port 1; old port 2 becomes the fresh auxiliary. The free order is old ports 0,1,4,5,…, with no permutation of the surviving ports.

def Cslib.BitString.capDifferencePort {n : ℕ} (j : Fin (n + 2)) : Fin (n + 4)

Difference coordinates surviving the cap, in the order 0,3,4,….

def Cslib.BitString.capRetainPort {n : ℕ} (j : Fin (n + 2)) : Fin (n + 4)

Original ports retained by the cap, in the order 0,1,4,5,….

theorem Cslib.BitString.capPort_not {n : ℕ} (y : Fin (n + 2) → Bool) (z : Fin 1 → Bool) : (Sum.elim (fun (i : Fin (n + 2)) => !y i) fun (i : Fin 1) => !z i) ∘ capPort = fun (i : Fin (n + 4)) => !Sum.elim y z (capPort i)

Complementing a cap assignment complements all old ports, including the hidden one.

theorem Cslib.BitString.retainPort_zeroPort {n : ℕ} (i j : Fin (n + 2)) : retainPort i (zeroPort i j) = j ∨ j = (finRotate (n + 2)) i ∧ retainPort i (zeroPort i j) = i ∨ j = i ∧ retainPort i (zeroPort i j) = (finRotate (n + 2)) i

Re-expanding a retained port returns the original port except for the merged endpoint.

theorem Cslib.BitString.comp_retainPort_zeroPort {n : ℕ} (i : Fin (n + 2)) (x : Fin (n + 2) → Bool) (h : cyclicDifference x i = false) : (x ∘ retainPort i) ∘ zeroPort i = x

An assignment with zero difference at i is exactly the expansion of its retained ports.

def Cslib.BitString.zeroRestriction {n : ℕ} (i : Fin (n + 2)) (P : Set (Fin (n + 2) → Bool)) : Set (Fin (n + 1) → Bool)

Adjacent equality restriction followed by deletion of the redundant port.

@[instance_reducible]

instance Cslib.BitString.instDecidablePredForallFinHAddNatOfNatBoolMemSetZeroRestriction {n : ℕ} (i : Fin (n + 2)) (P : Set (Fin (n + 2) → Bool)) [DecidablePred fun (x : Fin (n + 2) → Bool) => x ∈ P] : DecidablePred fun (x : Fin (n + 1) → Bool) => x ∈ zeroRestriction i P

theorem Cslib.BitString.mem_cyclicDifferenceRelation_zeroRestriction {n : ℕ} (i : Fin (n + 2)) (P : Set (Fin (n + 2) → Bool)) (d : Fin (n + 1) → Bool) : d ∈ cyclicDifferenceRelation (zeroRestriction i P) ↔ ∃ s ∈ cyclicDifferenceRelation P, s i = false ∧ s ∘ differencePort i = d

Exact difference semantics of adjacent identification, including deletion of the last edge. The deleted coordinate must be zero; this is conditioned restriction, not plain projection.

@[simp]

theorem Cslib.BitString.capPort_zero (n : ℕ) : capPort 0 = Sum.inl 0

Old port 0 is retained as free port 0.

@[simp]

theorem Cslib.BitString.capPort_one (n : ℕ) : capPort 1 = Sum.inl 1

Old port 1 is retained as free port 1.

@[simp]

theorem Cslib.BitString.capPort_two (n : ℕ) : capPort 2 = Sum.inr 0

Old port 2 becomes the fresh hidden port.

@[simp]

theorem Cslib.BitString.capPort_three (n : ℕ) : capPort 3 = Sum.inl 1

Old port 3 is identified with free port 1.

theorem Cslib.BitString.capPort_of_four_le {n : ℕ} (j : Fin (n + 4)) (h : 4 ≤ ↑j) : capPort j = Sum.inl ⟨↑j - 2, ⋯⟩

Old ports from 4 onward retain their order, shifted down by two.

theorem Cslib.BitString.capPort_capDifferencePort {n : ℕ} (j : Fin (n + 2)) : capPort (capDifferencePort j) = Sum.inl j

Retained difference edges start at the corresponding new free ports of a cap.

theorem Cslib.BitString.capPort_next_capDifferencePort {n : ℕ} (j : Fin (n + 2)) : capPort ((finRotate (n + 4)) (capDifferencePort j)) = Sum.inl ((finRotate (n + 2)) j)

Retained difference edges end at the corresponding cyclic successors after a cap.

theorem Cslib.BitString.cyclicDifference_capPort {n : ℕ} (y : Fin (n + 2) → Bool) (z : Fin 1 → Bool) : cyclicDifference (Sum.elim y z ∘ capPort) ∘ capDifferencePort = cyclicDifference y

The cap retains precisely the differences in order 0,3,4,….

theorem Cslib.BitString.cyclicDifference_capPort_pair {n : ℕ} (y : Fin (n + 2) → Bool) (z : Fin 1 → Bool) : cyclicDifference (Sum.elim y z ∘ capPort) 1 = cyclicDifference (Sum.elim y z ∘ capPort) 2

A cap imposes equality of old differences 1 and 2.

theorem Cslib.BitString.cyclicDifference_pair_eq_iff {n : ℕ} (x : Fin (n + 4) → Bool) : cyclicDifference x 1 = cyclicDifference x 2 ↔ x 1 = x 3

Equality of adjacent differences is equality of the two outside ports.

theorem Cslib.BitString.comp_capRetainPort_capPort {n : ℕ} (x : Fin (n + 4) → Bool) (h : x 1 = x 3) : (Sum.elim (x ∘ capRetainPort) fun (x_1 : Fin 1) => x 2) ∘ capPort = x

Reconstruct an old assignment from its retained and hidden cap ports.

def Cslib.BitString.capRelation {n : ℕ} (P : Set (Fin (n + 4) → Bool)) : Set (Fin (n + 2) → Bool)

Identify old ports 1 and 3, hide old port 2, and retain the other free ports in order.

@[instance_reducible]

instance Cslib.BitString.instDecidablePredForallFinHAddNatOfNatBoolMemSetCapRelation {n : ℕ} (P : Set (Fin (n + 4) → Bool)) [DecidablePred fun (x : Fin (n + 4) → Bool) => x ∈ P] : DecidablePred fun (x : Fin (n + 2) → Bool) => x ∈ capRelation P

theorem Cslib.BitString.mem_cyclicDifferenceRelation_capRelation {n : ℕ} (P : Set (Fin (n + 4) → Bool)) (d : Fin (n + 2) → Bool) : d ∈ cyclicDifferenceRelation (capRelation P) ↔ ∃ s ∈ cyclicDifferenceRelation P, s 1 = s 2 ∧ s ∘ capDifferencePort = d

Exact two-difference cap semantics. Both inclusions account for the hidden witness.

theorem Cslib.BitString.differencePort_eq_succAbove {n : ℕ} (i : Fin (n + 2)) : differencePort i = i.succAbove

The retained difference map is the standard increasing embedding omitting i.

@[simp]

theorem Cslib.BitString.differencePort_zero {n : ℕ} (i : Fin (n + 2)) (hi : i ≠ 0) : differencePort i 0 = 0

Deleting an edge other than 0 leaves the distinguished difference at 0.

theorem Cslib.BitString.eq_pair_of_zero_restriction {n : ℕ} (i : Fin (n + 2)) (hi : i ≠ 0) (j : Fin (n + 1)) (s : Fin (n + 2) → Bool) (hs : s i = false) (hd : s ∘ differencePort i = flipOn {0, j} fun (x : Fin (n + 1)) => false) : s = flipOn {0, differencePort i j} fun (x : Fin (n + 2)) => false

A pair containing difference 0 has exactly the same pair as its zero-conditioned lift.

theorem Cslib.BitString.capDifferencePort_injective {n : ℕ} : Function.Injective capDifferencePort

The cap's retained differences are distinct.

@[simp]

theorem Cslib.BitString.capDifferencePort_eq_zero_iff {n : ℕ} (j : Fin (n + 2)) : capDifferencePort j = 0 ↔ j = 0

The cap preserves the distinguished zero coordinate and sends no other coordinate to it.

theorem Cslib.BitString.three_le_val_capDifferencePort {n : ℕ} {j : Fin (n + 2)} (hj : j ≠ 0) : 3 ≤ ↑(capDifferencePort j)

Every nonzero retained difference lies after the two differences hidden by the cap.

@[simp]

theorem Cslib.BitString.capDifferencePort_ne_one {n : ℕ} (j : Fin (n + 2)) : capDifferencePort j ≠ 1

The first hidden difference is not in the cap's retained coordinates.

@[simp]

theorem Cslib.BitString.capDifferencePort_ne_two {n : ℕ} (j : Fin (n + 2)) : capDifferencePort j ≠ 2

The second hidden difference is not in the cap's retained coordinates.

theorem Cslib.BitString.exists_capDifferencePort {n : ℕ} (k : Fin (n + 4)) (h1 : k ≠ 1) (h2 : k ≠ 2) : ∃ (j : Fin (n + 2)), capDifferencePort j = k

Exactly differences 1 and 2 are hidden by the cap.

theorem Cslib.BitString.eq_pair_or_quartet_of_cap {n : ℕ} (j : Fin (n + 2)) (hj : j ≠ 0) (s : Fin (n + 4) → Bool) (hs : s 1 = s 2) (hd : s ∘ capDifferencePort = flipOn {0, j} fun (x : Fin (n + 2)) => false) : (s = flipOn {0, capDifferencePort j} fun (x : Fin (n + 4)) => false) ∨ s = flipOn {0, 1, 2, capDifferencePort j} fun (x : Fin (n + 4)) => false

A pair after the cap lifts to exactly the old pair or the old quartet.

theorem Cslib.BitString.cyclicDifference_comp_finCycle {n : ℕ} (e : Fin n) (x : Fin n → Bool) : cyclicDifference (x ∘ ⇑(finCycle e)) = cyclicDifference x ∘ ⇑(finCycle e)

Cyclic translation commutes with cyclic differences; orientation is preserved.

theorem Cslib.BitString.cyclicDifference_comp_finCycle_symm {n : ℕ} (e : Fin n) (x : Fin n → Bool) : cyclicDifference (x ∘ ⇑(Equiv.symm (finCycle e))) = cyclicDifference x ∘ ⇑(Equiv.symm (finCycle e))

Cyclic translation by the inverse shift also commutes with cyclic differences.