Initial parity tests from a Tanner code

[OpenAI2026ETH, Lemma 6.1] constructs, for a formula with m ≤ B n clauses, at most 3 n sparse parity tests on the m clause-violation bits whose common kernel contains no nonzero vector of weight less than m / P, where μ = ⌊log₂ m⌋ + 1, P = 20000 B² μ², and each test reads at most D₀ = 320000 B² μ³ bits. This file proves that such tests exist (Cslib.BitString.exists_initialTests); computing them by exhaustive search, and the cost of that search, are not treated here.

The tests are a shortened Tanner code (Cslib.BitString.Tanner.le_weight_of_shortRow). With d = min(m, D₀) and q = 2 ^ ℓ least with q d ≥ m, the graph is the double cover of a Cayley graph of the cube Fin ℓ → Bool with d generators that are ε-biased for ε = 1 / (200 B μ) (Cslib.BitString.exists_isSmallBias_map_of_exp_lt; if ℓ = 0 there is nothing to check). The local code has c = ⌈d / (8 B)⌉ checks and distance more than h = ⌈d / (100 B μ)⌉ - 1 (Cslib.BitString.exists_forall_weight_le), as at most (d + 1) ^ h < 2 ^ c nonzero strings have weight at most h (Cslib.BitString.card_filter_weight_le_le). The distance bound (h + 1)(h + 1 - ε d) q ≤ d · weight then gives weight at least q d / P ≥ m / P, and there are 2 q c ≤ 3 n rows of at most d ≤ D₀ ones.

Main results

• Cslib.BitString.card_filter_weight_le_le: at most (d + 1) ^ h strings have weight at most h.
• Cslib.BitString.exists_initialTests: the initial parity tests of [OpenAI2026ETH, Lemma 6.1].

References

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

theorem Cslib.BitString.card_filter_weight_le_le (d h : ℕ) : {w : Fin d → Bool | weight w ≤ h}.card ≤ (d + 1) ^ h

At most (d + 1) ^ h strings of length d have weight at most h.

theorem Cslib.BitString.exists_initialTests {n m B : ℕ} (hn : 1 ≤ n) (hB : 1 ≤ B) (hm : m ≤ B * n) : ∃ (rows : List (Fin m → Bool)), rows.length ≤ 3 * n ∧ (∀ r ∈ rows, weight r ≤ 320000 * B ^ 2 * (Nat.log 2 m + 1) ^ 3) ∧ ∀ (z : Fin m → Bool), z ≠ 0 → (∀ r ∈ rows, r ⬝ᵥ z = false) → m ≤ 20000 * B ^ 2 * (Nat.log 2 m + 1) ^ 2 * weight z

Initial parity tests [OpenAI2026ETH, Lemma 6.1]. Let n, B ≥ 1 and m ≤ B n, and put μ = ⌊log₂ m⌋ + 1, P = 20000 B² μ² and D₀ = 320000 B² μ³. There are at most 3 n rows over Fin m, each with at most D₀ ones, such that every nonzero bit string orthogonal to all of them has at least m / P ones.