Sparsity and list-length parameters for initial and greedy parity tests

Shared CNF-free parameter definitions for the initial parity-check matrix construction and greedy row-augmentation procedure of OpenAI, The Exponential Time Hypothesis is False, §§6.1–6.2, Lemmas 6.1–6.2 (pp. 40–42), with μ = ⌊log₂ m⌋ + 1.

Main definitions

• Cslib.BitString.initialRowWeightBound: D₀(B, m) = 320000 * B ^ 2 * (Nat.log 2 m + 1) ^ 3.
• Cslib.BitString.greedyRowListLength: P(B, m) = 20000 * B ^ 2 * (Nat.log 2 m + 1) ^ 2.

References

• OpenAI, The Exponential Time Hypothesis is False, §§6.1–6.2, Lemmas 6.1–6.2

def Cslib.BitString.initialRowWeightBound (B m : ℕ) : ℕ

The Lemma 6.1 initial row weight bound D₀(B, m) = 320000 * B ^ 2 * (Nat.log 2 m + 1) ^ 3 ([OAI26c], §6.1, Lemma 6.1).

def Cslib.BitString.greedyRowListLength (B m : ℕ) : ℕ

The Lemma 6.1–6.2 support denominator and greedy candidate list length P(B, m) = 20000 * B ^ 2 * (Nat.log 2 m + 1) ^ 2 ([OAI26c], §§6.1–6.2, Lemmas 6.1–6.2).