Uhlig's recovery code

Uhlig's two-copy construction stores bits x 0, …, x (M - 1) as the M + 1 adjacent sums x 0, x 0 ^^ x 1, …, x (M - 2) ^^ x (M - 1), x (M - 1). Sums of code positions are taken in the Boolean ring, where addition is exclusive or. Each bit is the sum of an initial segment of the code and also the sum of the complementary final segment. For two requests a and b, the smaller request uses the initial segment ending at its index and the larger request uses the final segment after its index. These recovery sets are disjoint even when a = b, so every code position serves at most one request.

The code is stated for sequences indexed by ℕ; only the value at M must vanish.

Main definitions

• Cslib.BitString.Uhlig.code: the adjacent sums of a sequence.
• Cslib.BitString.Uhlig.first, Cslib.BitString.Uhlig.second: the code positions used by the first and second of two requests.

Main results

• Cslib.BitString.Uhlig.sum_range_code: recovery from an initial segment.
• Cslib.BitString.Uhlig.sum_Ico_code: recovery from a final segment.
• Cslib.BitString.Uhlig.second_eq_false_of_first: the two recovery sets are disjoint.
• Cslib.BitString.Uhlig.sum_first_code_route, Cslib.BitString.Uhlig.sum_second_code_route: each request recovers its bit when every code position reads the input of the request that uses it.

References

• D. Uhlig, Networks computing Boolean functions for multiple input values.
• I. Wegener, The Complexity of Boolean Functions, proof of Theorem 10.2.3.
• Adapted from MassProduction/Uhlig.lean in S. Schlesinger, Boolean circuit mass production formalization.

def Cslib.BitString.Uhlig.code (x : ℕ → Bool) : ℕ → Bool

Uhlig's code of a bit sequence: position 0 holds x 0 and position j + 1 holds x j ^^ x (j + 1).

theorem Cslib.BitString.Uhlig.sum_range_code (x : ℕ → Bool) (a : ℕ) : ∑ j ∈ Finset.range (a + 1), code x j = x a

The code positions up to a sum to x a.

theorem Cslib.BitString.Uhlig.sum_Ico_code {x : ℕ → Bool} {M a : ℕ} (hx : x M = false) (ha : a ≤ M) : ∑ j ∈ Finset.Ico (a + 1) (M + 1), code x j = x a

If x M vanishes, the code positions after a, up to M, also sum to x a.

def Cslib.BitString.Uhlig.first (a b j : ℕ) : Bool

With requests a and b, the first request uses position j when the requests are in order and j ≤ a, or out of order and a < j.

def Cslib.BitString.Uhlig.second (a b j : ℕ) : Bool

With requests a and b, the second request uses position j when the requests are in order and b < j, or out of order and j ≤ b.

theorem Cslib.BitString.Uhlig.second_eq_false_of_first {a b j : ℕ} (h : first a b j = true) : second a b j = false

No code position serves both requests, including when a = b.

theorem Cslib.BitString.Uhlig.sum_first_code {x : ℕ → Bool} {M a : ℕ} (hx : x M = false) (ha : a < M) (b : ℕ) : ∑ j ∈ Finset.range (M + 1), (first a b j && code x j) = x a

The first request recovers x a from its positions. The other index is arbitrary.

theorem Cslib.BitString.Uhlig.sum_second_code {x : ℕ → Bool} {M b : ℕ} (hx : x M = false) (hb : b < M) (a : ℕ) : ∑ j ∈ Finset.range (M + 1), (second a b j && code x j) = x b

The second request recovers x b from its positions. The other index is arbitrary.

theorem Cslib.BitString.Uhlig.sum_first_code_route {Z : Type u_1} {h : Z → ℕ → Bool} {M a : ℕ} (hM : ∀ (z : Z), h z M = false) (ha : a < M) (b : ℕ) (z z' : Z) : ∑ j ∈ Finset.range (M + 1), (first a b j && code (h (if first a b j = true then z else z')) j) = h z a

Route the first input z to the first request's positions and z' to all others. Then the first request recovers its bit of z.

theorem Cslib.BitString.Uhlig.sum_second_code_route {Z : Type u_1} {h : Z → ℕ → Bool} {M b : ℕ} (hM : ∀ (z : Z), h z M = false) (hb : b < M) (a : ℕ) (z z' : Z) : ∑ j ∈ Finset.range (M + 1), (second a b j && code (h (if first a b j = true then z else z')) j) = h z' b

With the same routing, the second request recovers its bit of z'.