Greedy selection of random parity tests

A test list γ = ((e₁, c₁), …, (e_P, c_P)) of P pairs of an index eⱼ < m and a bit cⱼ represents the test row testRow γ over 𝔽₂, whose coordinate e is the sum of the bits cⱼ with eⱼ = e (Cslib.BitString.testRow). The row rejects a bit string z when its parity testRow γ ⬝ᵥ z = Σⱼ cⱼ z_{eⱼ} (Cslib.BitString.testParity) is true.

If z is nonzero with at least m / P ones, then at least a quarter of the (2m) ^ P lists reject z (Cslib.BitString.pow_le_four_mul_card_testParity_eq_true). Exactly 2 ^ (P - 1) (m ^ P - (m - weight z) ^ P) lists do: for indices that hit a one of z, the parity is the parity of the coefficients on a nonempty set, which is balanced (Cslib.card_filter_parityOn_eq); and (1 - 1/P) ^ P ≤ e⁻¹ < 1/2.

Averaging then gives a deterministic procedure [OpenAI2026ETH, Lemma 6.2]. Given points x with violation vectors v x, a list of rows accepts x when every row has parity zero on v x. Starting from rows after which every accepted point with a nonzero violation vector has at least m / P violations, append 3 n rows testRow γ, each minimizing the number of accepted points. Each step keeps at most three quarters of the accepted points with nonzero violation vectors, so with at most 2 ^ n points the final rows accept exactly the points whose violation vector is zero (Cslib.BitString.numPassing_greedy). The procedure only compares counts of accepted points, which exceed the unknown number of zero-violation points by the number of accepted bad points (Cslib.BitString.numPassing_eq).

Main definitions

• Cslib.BitString.testRow, Cslib.BitString.testParity: the row of a test list and its parity.
• Cslib.BitString.PassesTests, Cslib.BitString.numPassing: acceptance by a list of rows, and the number of accepted points.

Main results

• Cslib.BitString.weight_testRow_le: a test row of list length P has Hamming weight at most P.
• Cslib.BitString.two_mul_card_testParity_eq_true: the exact number of rejecting lists.
• Cslib.BitString.pow_le_four_mul_card_testParity_eq_true: a quarter of the lists reject.
• Cslib.BitString.four_mul_card_accept_le_of_forall_le: a minimizing list accepts at most three quarters of a set of such vectors.
• Cslib.BitString.numPassing_greedy: the greedy procedure after 3 n rounds.

References

• OpenAI, The Exponential Time Hypothesis is False, §6.2

Test lists

def Cslib.BitString.testParity {m P : ℕ} (γ : Fin P → Fin m × Bool) (z : Fin m → Bool) : Bool

The parity of the test list γ = ((eⱼ, cⱼ))ⱼ on the bit string z: Σⱼ cⱼ z_{eⱼ}.

def Cslib.BitString.testRow {m P : ℕ} (γ : Fin P → Fin m × Bool) : Fin m → Bool

The test row of a list: coordinate e is the sum of the bits cⱼ with eⱼ = e.

theorem Cslib.BitString.testRow_dotProduct {m P : ℕ} (γ : Fin P → Fin m × Bool) (z : Fin m → Bool) : testRow γ ⬝ᵥ z = testParity γ z

The parity of a list is the inner product of its row with the bit string.

theorem Cslib.BitString.weight_testRow_le {m P : ℕ} (γ : Fin P → Fin m × Bool) : weight (testRow γ) ≤ P

A test row built from a list γ of P index-bit pairs has Hamming weight at most P.

theorem Cslib.BitString.two_mul_card_dotProduct_eq_true {P : ℕ} {w : Fin P → Bool} {j : Fin P} (hj : w j = true) : 2 * {c : Fin P → Bool | c ⬝ᵥ w = true}.card = 2 ^ P

Exactly half of the coefficient strings have inner product true with a nonzero string: the inner product with w is the parity on the support of w (dotProduct_eq_parityOn), which is balanced (Cslib.card_filter_parityOn_eq).

theorem Cslib.BitString.two_mul_card_testParity_eq_true {m P : ℕ} (z : Fin m → Bool) : 2 * {γ : Fin P → Fin m × Bool | testParity γ z = true}.card = 2 ^ P * (m ^ P - {i : Fin m | z i = false}.card ^ P)

The exact number of rejecting lists: 2 ^ (P - 1) (m ^ P - (m - weight z) ^ P), written without division.

theorem Cslib.BitString.pow_le_four_mul_card_testParity_eq_true {m P : ℕ} (z : Fin m → Bool) (hP : 1 ≤ P) (hz : m ≤ P * weight z) : (2 * m) ^ P ≤ 4 * {γ : Fin P → Fin m × Bool | testParity γ z = true}.card

A quarter of the lists reject a bit string with at least m / P ones.

Averaging and iteration

theorem Cslib.BitString.four_mul_card_accept_le_of_forall_le {m P : ℕ} {ι : Type u_1} (S : Finset ι) (z : ι → Fin m → Bool) (hP : 1 ≤ P) (hz₀ : ∀ x ∈ S, z x ≠ 0) (hz : ∀ x ∈ S, m ≤ P * weight (z x)) (γ : Fin P → Fin m × Bool) (hγ : ∀ (γ' : Fin P → Fin m × Bool), {x ∈ S | testParity γ (z x) = false}.card ≤ {x ∈ S | testParity γ' (z x) = false}.card) : 4 * {x ∈ S | testParity γ (z x) = false}.card ≤ 3 * S.card

Averaging. A list minimizing the number of accepted strings accepts at most three quarters of a set of nonzero bit strings, each with at least m / P ones.

theorem Cslib.BitString.eq_zero_of_four_mul_le_three_mul (D : ℕ → ℕ) {n : ℕ} (hn : 1 ≤ n) (h₀ : D 0 ≤ 2 ^ n) (hstep : ∀ (i : ℕ), 4 * D (i + 1) ≤ 3 * D i) : D (3 * n) = 0

Iteration. A sequence of naturals that starts at most 2 ^ n, with n ≥ 1, and shrinks by a factor of at least 3/4 at each step vanishes after 3 n steps, since (3/4) ^ (3n) 2 ^ n = (27/32) ^ n < 1.

The greedy procedure

def Cslib.BitString.PassesTests {m : ℕ} {X : Type u_1} (v : X → Fin m → Bool) (A : List (Fin m → Bool)) (x : X) : Prop

The rows A accept the point x: every row has parity zero on its violation vector.

@[instance_reducible]

instance Cslib.BitString.instDecidablePredPassesTests {m : ℕ} {X : Type u_1} (v : X → Fin m → Bool) (A : List (Fin m → Bool)) : DecidablePred (PassesTests v A)

theorem Cslib.BitString.passesTests_append_singleton {m : ℕ} {X : Type u_1} (v : X → Fin m → Bool) (A : List (Fin m → Bool)) (h : Fin m → Bool) (x : X) : PassesTests v (A ++ [h]) x ↔ PassesTests v A x ∧ h ⬝ᵥ v x = false

def Cslib.BitString.numPassing {m : ℕ} {X : Type u_1} [Fintype X] (v : X → Fin m → Bool) (A : List (Fin m → Bool)) : ℕ

N(A): the number of points accepted by the rows A.

theorem Cslib.BitString.numPassing_eq {m : ℕ} {X : Type u_1} [Fintype X] (v : X → Fin m → Bool) (A : List (Fin m → Bool)) : numPassing v A = {x : X | v x = 0}.card + {x : X | PassesTests v A x ∧ v x ≠ 0}.card

N(A) = #F + D(A): every point with zero violation vector is accepted, so the number of accepted points is the number of such points plus the number of accepted points with a nonzero violation vector.

theorem Cslib.BitString.numPassing_greedy {m P : ℕ} {X : Type u_1} [Fintype X] (v : X → Fin m → Bool) {n : ℕ} (hn : 1 ≤ n) (hX : Fintype.card X ≤ 2 ^ n) (hP : 1 ≤ P) (A : ℕ → List (Fin m → Bool)) (hinit : ∀ (x : X), PassesTests v (A 0) x → v x ≠ 0 → m ≤ P * weight (v x)) (γ : ℕ → Fin P → Fin m × Bool) (hA : ∀ (i : ℕ), A (i + 1) = A i ++ [testRow (γ i)]) (hγ : ∀ (i : ℕ) (γ' : Fin P → Fin m × Bool), numPassing v (A i ++ [testRow (γ i)]) ≤ numPassing v (A i ++ [testRow γ'])) : numPassing v (A (3 * n)) = {x : X | v x = 0}.card

Greedy selection of parity tests [OpenAI2026ETH, Lemma 6.2]. Suppose that after the initial rows A 0, every accepted point with a nonzero violation vector has at least m / P violations, and that there are at most 2 ^ n points, with n ≥ 1. Append rows A (i + 1) = A i ++ [testRow (γ i)], where each list γ i minimizes the number of accepted points among all lists. Then after 3 n rounds the rows accept exactly the points with zero violation vector.