Tanner codes on small-bias Cayley graphs

A Tanner code Tanner, Section II places bits on the edges of a regular graph and requires the bits around every vertex, ordered by port, to lie in a fixed local code. Here the graph is the bipartite double cover of a Cayley graph of the cube Fin ℓ → Bool with generators s₁, …, s_d (Cslib.RotationMap.cubeCayley): left vertex u is joined by its port-j edge to right vertex u + sⱼ, and edge words are bit strings on (Fin ℓ → Bool) × Fin d. The local code is the kernel of a matrix A with c rows (Cslib.BitString.Tanner.IsWord).

• Local codes (Cslib.BitString.exists_forall_weight_le): if fewer than 2 ^ c nonzero strings of length d have weight at most h, some c × d matrix rejects all of them, so its kernel has minimum distance more than h. A union bound: a nonzero string lies in the kernel of exactly 2 ^ ((d - 1) c) of the 2 ^ (d c) matrices (Cslib.BitString.card_kernel), since its inner product with a uniform row is a balanced parity.
• Distance (Cslib.BitString.Tanner.le_weight_of_isWord): if the local code has distance more than h and the generators are ε-biased with ε ≥ 0, every nonzero Tanner word x has (h + 1) (h + 1 - ε d) 2 ^ ℓ ≤ d · weight x. The vertices U, V touched by x on the two sides each see at least h + 1 of its bits, while all its bits are edges between U and V, which the mixing estimate (Cslib.RotationMap.card_interedges_cubeCayley_le) bounds.
• Shortening (Cslib.BitString.Tanner.le_weight_of_shortRow): keeping m of the edges, by an embedding Fin m ↪ (Fin ℓ → Bool) × Fin d, gives 2 · 2 ^ ℓ · c explicit rows on Fin m (Cslib.BitString.Tanner.shortRow), each with at most d ones (Cslib.BitString.Tanner.weight_shortRow_le), whose nonzero kernel strings obey the same bound, again for ε ≥ 0.

These are the local-code, distance and shortening steps in the proof of [OpenAI2026ETH, Lemma 6.1], which builds the initial parity tests from such a code.

Main definitions

• Cslib.BitString.Tanner.IsWord: the Tanner code of a local check matrix.
• Cslib.BitString.Tanner.shortRow: the rows of the shortened code.

Main results

• Cslib.BitString.exists_forall_weight_le: local codes of given distance by the union bound.
• Cslib.BitString.Tanner.le_weight_of_isWord: the distance of the Tanner code.
• Cslib.BitString.Tanner.weight_shortRow_le: the rows of the shortened code are sparse.
• Cslib.BitString.Tanner.le_weight_of_shortRow: the distance of the shortened code.

References

• OpenAI, The Exponential Time Hypothesis is False, §6.1
• R. M. Tanner, A recursive approach to low complexity codes

theorem Cslib.BitString.card_dotProduct_eq_false {d : ℕ} {w : Fin d → Bool} (hw : w ≠ 0) : {x : Fin d → Bool | x ⬝ᵥ w = false}.card = 2 ^ (d - 1)

The rows orthogonal to a nonzero w: 2 ^ (d - 1) of the 2 ^ d.

theorem Cslib.BitString.card_kernel {c d : ℕ} {w : Fin d → Bool} (hw : w ≠ 0) : {A : Fin c → Fin d → Bool | ∀ (i : Fin c), A i ⬝ᵥ w = false}.card = (2 ^ (d - 1)) ^ c

Matrices with c rows whose kernel contains a nonzero w: 2 ^ ((d - 1) c).

theorem Cslib.BitString.exists_forall_weight_le {c d h : ℕ} (hlt : {w : Fin d → Bool | w ≠ 0 ∧ weight w ≤ h}.card < 2 ^ c) : ∃ (A : Fin c → Fin d → Bool), ∀ (w : Fin d → Bool), w ≠ 0 → weight w ≤ h → ∃ (i : Fin c), A i ⬝ᵥ w = true

Local codes by the union bound: if fewer than 2 ^ c nonzero strings have weight at most h, some matrix with c rows rejects them all.

def Cslib.BitString.Tanner.leftWord {ℓ d : ℕ} (x : (Fin ℓ → Bool) × Fin d → Bool) (u : Fin ℓ → Bool) : Fin d → Bool

The edge word at the left vertex u: the bits of its d edges, by port.

def Cslib.BitString.Tanner.rightWord {ℓ d : ℕ} (s : Fin d → Fin ℓ → Bool) (x : (Fin ℓ → Bool) × Fin d → Bool) (v : Fin ℓ → Bool) : Fin d → Bool

The edge word at the right vertex v: its port-j edge comes from v + s j.

def Cslib.BitString.Tanner.IsWord {ℓ d c : ℕ} (s : Fin d → Fin ℓ → Bool) (A : Fin c → Fin d → Bool) (x : (Fin ℓ → Bool) × Fin d → Bool) : Prop

The Tanner code: every vertex sees a local word in the kernel of A.

theorem Cslib.BitString.Tanner.weight_eq_sum_left {ℓ d : ℕ} (x : (Fin ℓ → Bool) × Fin d → Bool) : weight x = ∑ u : Fin ℓ → Bool, weight (leftWord x u)

The weight of an edge word is the sum of the weights of its left words.

theorem Cslib.BitString.Tanner.weight_eq_sum_right {ℓ d : ℕ} (s : Fin d → Fin ℓ → Bool) (x : (Fin ℓ → Bool) × Fin d → Bool) : weight x = ∑ v : Fin ℓ → Bool, weight (rightWord s x v)

The weight of an edge word is the sum of the weights of its right words.

theorem Cslib.BitString.Tanner.le_weight_of_isWord {ℓ d c : ℕ} [NeZero d] (s : Fin d → Fin ℓ → Bool) {ε : ℝ} (hε : 0 ≤ ε) (hs : IsSmallBias ε (PMF.map s (Probability.PMF.uniformOfFintype (Fin d)))) (A : Fin c → Fin d → Bool) {h : ℕ} (hA : ∀ (w : Fin d → Bool), w ≠ 0 → (∀ (i : Fin c), A i ⬝ᵥ w = false) → h < weight w) {x : (Fin ℓ → Bool) × Fin d → Bool} (hx : IsWord s A x) (hx0 : x ≠ 0) : ↑(h + 1) * (↑(h + 1) - ε * ↑d) * 2 ^ ℓ ≤ ↑d * ↑(weight x)

The distance of the Tanner code. If every nonzero local word accepted by A has weight more than h, and the generators are ε-biased with ε ≥ 0, then every nonzero Tanner word x has (h + 1) (h + 1 - ε d) 2 ^ ℓ ≤ d · weight x.

Shortening

def Cslib.BitString.Tanner.shortRow {ℓ d c m : ℕ} (s : Fin d → Fin ℓ → Bool) (A : Fin c → Fin d → Bool) (emb : Fin m ↪ (Fin ℓ → Bool) × Fin d) (r : Bool × (Fin ℓ → Bool) × Fin c) : Fin m → Bool

The row of the shortened Tanner code for the check i at a vertex: on the left vertex u (side = false) or the right vertex u (side = true), coordinate e reads the port of the retained edge emb e if that edge is incident to the vertex.

def Cslib.BitString.Tanner.extend {ℓ d m : ℕ} (emb : Fin m ↪ (Fin ℓ → Bool) × Fin d) (z : Fin m → Bool) : (Fin ℓ → Bool) × Fin d → Bool

The edge word extending z by zero outside the retained edges.

theorem Cslib.BitString.Tanner.extend_emb {ℓ d m : ℕ} (emb : Fin m ↪ (Fin ℓ → Bool) × Fin d) (z : Fin m → Bool) (e : Fin m) : extend emb z (emb e) = z e

The extension agrees with z on the retained edges.

theorem Cslib.BitString.Tanner.extend_of_notMem {ℓ d m : ℕ} (emb : Fin m ↪ (Fin ℓ → Bool) × Fin d) (z : Fin m → Bool) {p : (Fin ℓ → Bool) × Fin d} (hp : ∀ (e : Fin m), emb e ≠ p) : extend emb z p = 0

The extension vanishes off the retained edges.

theorem Cslib.BitString.Tanner.weight_extend {ℓ d m : ℕ} (emb : Fin m ↪ (Fin ℓ → Bool) × Fin d) (z : Fin m → Bool) : weight (extend emb z) = weight z

Extending by zero preserves the weight.

theorem Cslib.BitString.Tanner.shortRow_dotProduct_left {ℓ d c m : ℕ} (s : Fin d → Fin ℓ → Bool) (A : Fin c → Fin d → Bool) (emb : Fin m ↪ (Fin ℓ → Bool) × Fin d) (z : Fin m → Bool) (u : Fin ℓ → Bool) (i : Fin c) : shortRow s A emb (false, u, i) ⬝ᵥ z = A i ⬝ᵥ leftWord (extend emb z) u

A left row of the shortened code checks the left word of the extension.

theorem Cslib.BitString.Tanner.shortRow_dotProduct_right {ℓ d c m : ℕ} (s : Fin d → Fin ℓ → Bool) (A : Fin c → Fin d → Bool) (emb : Fin m ↪ (Fin ℓ → Bool) × Fin d) (z : Fin m → Bool) (v : Fin ℓ → Bool) (i : Fin c) : shortRow s A emb (true, v, i) ⬝ᵥ z = A i ⬝ᵥ rightWord s (extend emb z) v

A right row of the shortened code checks the right word of the extension.

theorem Cslib.BitString.Tanner.weight_shortRow_le {ℓ d c m : ℕ} (s : Fin d → Fin ℓ → Bool) (A : Fin c → Fin d → Bool) (emb : Fin m ↪ (Fin ℓ → Bool) × Fin d) (r : Bool × (Fin ℓ → Bool) × Fin c) : weight (shortRow s A emb r) ≤ d

Each row of the shortened code has at most d ones: the retained edges at a vertex have distinct ports.

theorem Cslib.BitString.Tanner.le_weight_of_shortRow {ℓ d c m : ℕ} [NeZero d] (s : Fin d → Fin ℓ → Bool) {ε : ℝ} (hε : 0 ≤ ε) (hs : IsSmallBias ε (PMF.map s (Probability.PMF.uniformOfFintype (Fin d)))) (A : Fin c → Fin d → Bool) {h : ℕ} (hA : ∀ (w : Fin d → Bool), w ≠ 0 → (∀ (i : Fin c), A i ⬝ᵥ w = false) → h < weight w) (emb : Fin m ↪ (Fin ℓ → Bool) × Fin d) {z : Fin m → Bool} (hz : ∀ (r : Bool × (Fin ℓ → Bool) × Fin c), shortRow s A emb r ⬝ᵥ z = false) (hz0 : z ≠ 0) : ↑(h + 1) * (↑(h + 1) - ε * ↑d) * 2 ^ ℓ ≤ ↑d * ↑(weight z)

The shortened Tanner code. Under the hypotheses of le_weight_of_isWord, including ε ≥ 0, every nonzero z orthogonal to all the rows shortRow has (h + 1) (h + 1 - ε d) 2 ^ ℓ ≤ d · weight z.