Sequential initial-test search and shortened Tanner check matrices

Deterministic sequential search and shortened Tanner parity-check construction from OpenAI, The Exponential Time Hypothesis is False, §6.1, Lemma 6.1 (pp. 40–42), giving the executable counterpart to Cslib.BitString.exists_initialTests. Given n, B ≥ 1 and m ≤ B * n, initialTestsRows m B constructs a binary matrix A^(0) on m columns with at most 3 * n rows of weight at most initialRowWeightBound B m whose GF(2) kernel excludes every nonzero vector of weight below m / greedyRowListLength B m, in exp(poly(B, log(m + 2))) bit operations and poly(n, m, B) working space via Cslib.GenericRAM.IndexFold.run.

Main definitions

• dG, ellG, qG, cG, hDist, biasDen: Lemma 6.1 parameter schedule.
• checkSmallBiasShifts, checkLocalCodeDistance, findSmallBiasShifts, findLocalCheckMatrix: streaming IndexFold.run checkers and sequential searchers.
• buildShortenedTannerRows, initialTestsRows: shortened Tanner check-matrix assembly.

Main results

• checkSmallBiasShifts_eq_true_iff, checkLocalCodeDistance_eq_true_iff, isSmallBias_findSmallBiasShifts, weight_le_of_findLocalCheckMatrix: checker/searcher specs.
• initialTestsRows_spec, map_ofList_initialTestsRows_spec, initialTestsRows_computableInO, initialTestsRows_computableInO_nmb: unconditional Lemma 6.1 correctness and ComputableInO.

References

• OpenAI, The Exponential Time Hypothesis is False, §6.1, Lemma 6.1
• R. M. Tanner, A recursive approach to low complexity codes
• J. Naor, M. Naor, Small-bias probability spaces

Lemma 6.1 integer parameter schedule

def Cslib.Complexity.InitialTestsSearch.dG (m B : ℕ) : ℕ

Cayley degree d_G = min(m, D₀) (D₀ = initialRowWeightBound B m) of [OAI26c], Lemma 6.1.

def Cslib.Complexity.InitialTestsSearch.ellG (m B : ℕ) : ℕ

Cube dimension ℓ_G = ⌈log₂ ⌈m / d_G⌉⌉ of [OAI26c], Lemma 6.1 (0 if d_G = 0).

def Cslib.Complexity.InitialTestsSearch.qG (m B : ℕ) : ℕ

Vertex-side size q_G = 2 ^ ℓ_G of the double cover in [OAI26c], Lemma 6.1.

def Cslib.Complexity.InitialTestsSearch.cG (m B : ℕ) : ℕ

Local parity-check row count c_G = ⌈d_G / (8 B)⌉ of [OAI26c], Lemma 6.1 (0 if B = 0).

def Cslib.Complexity.InitialTestsSearch.hDist (m B : ℕ) : ℕ

Maximum rejected weight h = ⌈d_G / (100 B μ)⌉ - 1 for the local code of Lemma 6.1 (0 if d_G = 0 or B = 0).

def Cslib.Complexity.InitialTestsSearch.biasDen (m B : ℕ) : ℕ

Reciprocal bias denominator 200 B μ (ε = 1 / biasDen m B) in [OAI26c], (6.2).

theorem Cslib.Complexity.InitialTestsSearch.dG_pos {m B : ℕ} (hm : 1 ≤ m) (hB : 1 ≤ B) : 0 < dG m B

theorem Cslib.Complexity.InitialTestsSearch.le_qG_mul_dG {m B : ℕ} (hm : 1 ≤ m) (hB : 1 ≤ B) : m ≤ qG m B * dG m B

theorem Cslib.Complexity.InitialTestsSearch.qG_mul_dG_lt_two_mul {m B : ℕ} (hm : 1 ≤ m) (hB : 1 ≤ B) : qG m B * dG m B < 2 * m

theorem Cslib.Complexity.InitialTestsSearch.qG_lt_two_mul {m B : ℕ} (hm : 1 ≤ m) (hB : 1 ≤ B) : qG m B < 2 * m

theorem Cslib.Complexity.InitialTestsSearch.qG_le_two_mul_add_one (m B : ℕ) : qG m B ≤ 2 * m + 1

theorem Cslib.Complexity.InitialTestsSearch.two_mul_qG_mul_cG_le_three_mul {n m B : ℕ} (hn : 1 ≤ n) (hm : 1 ≤ m) (hB : 1 ≤ B) (hmn : m ≤ B * n) : 2 * qG m B * cG m B ≤ 3 * n

theorem Cslib.Complexity.InitialTestsSearch.dG_le_hDist_succ_mul {m B : ℕ} (hm : 1 ≤ m) (hB : 1 ≤ B) : dG m B ≤ (hDist m B + 1) * (100 * B * (Nat.log 2 m + 1))

theorem Cslib.Complexity.InitialTestsSearch.greedyRowListLength_polyTime {α : Type} {ei : α ↪ List Bool} {m B : α → ℕ} (hm : Turing.MultiTapeTM.ComputableInPolyTime m ei Turing.MultiTapeTM.encUnary) (hB : Turing.MultiTapeTM.ComputableInPolyTime B ei Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => BitString.greedyRowListLength (B a) (m a)) ei Turing.MultiTapeTM.encUnary

theorem Cslib.Complexity.InitialTestsSearch.initialRowWeightBound_polyTime {α : Type} {ei : α ↪ List Bool} {m B : α → ℕ} (hm : Turing.MultiTapeTM.ComputableInPolyTime m ei Turing.MultiTapeTM.encUnary) (hB : Turing.MultiTapeTM.ComputableInPolyTime B ei Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => BitString.initialRowWeightBound (B a) (m a)) ei Turing.MultiTapeTM.encUnary

theorem Cslib.Complexity.InitialTestsSearch.dG_polyTime {α : Type} {ei : α ↪ List Bool} {m B : α → ℕ} (hm : Turing.MultiTapeTM.ComputableInPolyTime m ei Turing.MultiTapeTM.encUnary) (hB : Turing.MultiTapeTM.ComputableInPolyTime B ei Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => dG (m a) (B a)) ei Turing.MultiTapeTM.encUnary

theorem Cslib.Complexity.InitialTestsSearch.ellG_polyTime {α : Type} {ei : α ↪ List Bool} {m B : α → ℕ} (hm : Turing.MultiTapeTM.ComputableInPolyTime m ei Turing.MultiTapeTM.encUnary) (hB : Turing.MultiTapeTM.ComputableInPolyTime B ei Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => ellG (m a) (B a)) ei Turing.MultiTapeTM.encUnary

theorem Cslib.Complexity.InitialTestsSearch.qG_polyTime {α : Type} {ei : α ↪ List Bool} {m B : α → ℕ} (hm : Turing.MultiTapeTM.ComputableInPolyTime m ei Turing.MultiTapeTM.encUnary) (hB : Turing.MultiTapeTM.ComputableInPolyTime B ei Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => qG (m a) (B a)) ei Turing.MultiTapeTM.encUnary

theorem Cslib.Complexity.InitialTestsSearch.cG_polyTime {α : Type} {ei : α ↪ List Bool} {m B : α → ℕ} (hm : Turing.MultiTapeTM.ComputableInPolyTime m ei Turing.MultiTapeTM.encUnary) (hB : Turing.MultiTapeTM.ComputableInPolyTime B ei Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => cG (m a) (B a)) ei Turing.MultiTapeTM.encUnary

theorem Cslib.Complexity.InitialTestsSearch.hDist_polyTime {α : Type} {ei : α ↪ List Bool} {m B : α → ℕ} (hm : Turing.MultiTapeTM.ComputableInPolyTime m ei Turing.MultiTapeTM.encUnary) (hB : Turing.MultiTapeTM.ComputableInPolyTime B ei Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => hDist (m a) (B a)) ei Turing.MultiTapeTM.encUnary

theorem Cslib.Complexity.InitialTestsSearch.biasDen_polyTime {α : Type} {ei : α ↪ List Bool} {m B : α → ℕ} (hm : Turing.MultiTapeTM.ComputableInPolyTime m ei Turing.MultiTapeTM.encUnary) (hB : Turing.MultiTapeTM.ComputableInPolyTime B ei Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => biasDen (m a) (B a)) ei Turing.MultiTapeTM.encUnary

Private streaming IndexFold and matrix-search combinators

Polynomial-time and streaming checkers

def Cslib.Complexity.InitialTestsSearch.checkSmallBiasShifts (ell d maxBiasNum maxBiasDen : ℕ) (shifts : List (List Bool)) : Bool

Streaming small-bias shift checker ([OAI26c], Lemma 6.1, eq. (6.2)): checks that shifts has d rows of length ell and |d - 2 * odd(b)| * maxBiasDen ≤ maxBiasNum * d on all nonzero masks b ∈ {0, 1} ^ ell \ {0}, returning false on any shape or bias violation.

theorem Cslib.Complexity.InitialTestsSearch.checkSmallBiasShifts_eq_true_iff {ell d maxBiasNum maxBiasDen : ℕ} [NeZero d] (hden : 0 < maxBiasDen) (shifts : List (List Bool)) : checkSmallBiasShifts ell d maxBiasNum maxBiasDen shifts = true ↔ shifts.length = d ∧ (∀ row ∈ shifts, row.length = ell) ∧ BitString.IsSmallBias (↑maxBiasNum / ↑maxBiasDen) (PMF.map (fun (j : Fin d) => BitString.ofList ell (shifts.getD ↑j [])) (Probability.PMF.uniformOfFintype (Fin d)))

Exact characterization of checkSmallBiasShifts for d ≥ 1 and 0 < maxBiasDen.

theorem Cslib.Complexity.InitialTestsSearch.checkSmallBiasShifts_computableInO : ∃ (pT : ℕ → ℕ) (pS : ℕ → ℕ), PolynomiallyBounded pT ∧ PolynomiallyBounded pS ∧ have encQ := Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat))) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits); Turing.MultiTapeTM.ComputableInO (fun (q : (ℕ × ℕ × ℕ × ℕ) × List (List Bool)) => checkSmallBiasShifts q.1.1 q.1.2.1 q.1.2.2.1 q.1.2.2.2 q.2) encQ Turing.MultiTapeTM.encBool (fun (q : (ℕ × ℕ × ℕ × ℕ) × List (List Bool)) => (2 ^ q.1.1 + 1) * pT (encQ q).length) fun (q : (ℕ × ℕ × ℕ × ℕ) × List (List Bool)) => pS (encQ q).length

Native ComputableInO certificate for checkSmallBiasShifts.

theorem Cslib.Complexity.InitialTestsSearch.checkSmallBiasShifts_polyTime {α : Type} {encIn : α ↪ List Bool} {ell d maxBiasNum maxBiasDen : α → ℕ} {shifts : α → List (List Bool)} (hell : Turing.MultiTapeTM.ComputableInPolyTime ell encIn Turing.MultiTapeTM.encUnary) (hd : Turing.MultiTapeTM.ComputableInPolyTime d encIn Turing.MultiTapeTM.encUnary) (hnum : Turing.MultiTapeTM.ComputableInPolyTime maxBiasNum encIn Turing.MultiTapeTM.encNat) (hden : Turing.MultiTapeTM.ComputableInPolyTime maxBiasDen encIn Turing.MultiTapeTM.encNat) (hshifts : Turing.MultiTapeTM.ComputableInPolyTime shifts encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) (hq : Turing.MultiTapeTM.PolyBounded (fun (a : α) => (encIn a).length) fun (a : α) => 2 ^ ell a) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => checkSmallBiasShifts (ell a) (d a) (maxBiasNum a) (maxBiasDen a) (shifts a)) encIn Turing.MultiTapeTM.encBool

Plain polynomial-time certificate for checkSmallBiasShifts when 2 ^ ell is poly-bounded.

theorem Cslib.Complexity.InitialTestsSearch.checkSmallBiasShifts_polyTime_of_two_pow_le {α : Type} {encIn : α ↪ List Bool} {m ell d maxBiasNum maxBiasDen : α → ℕ} {shifts : α → List (List Bool)} (hm : Turing.MultiTapeTM.ComputableInPolyTime m encIn Turing.MultiTapeTM.encUnary) (hell : Turing.MultiTapeTM.ComputableInPolyTime ell encIn Turing.MultiTapeTM.encUnary) (hd : Turing.MultiTapeTM.ComputableInPolyTime d encIn Turing.MultiTapeTM.encUnary) (hnum : Turing.MultiTapeTM.ComputableInPolyTime maxBiasNum encIn Turing.MultiTapeTM.encNat) (hden : Turing.MultiTapeTM.ComputableInPolyTime maxBiasDen encIn Turing.MultiTapeTM.encNat) (hshifts : Turing.MultiTapeTM.ComputableInPolyTime shifts encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) (hle : ∀ (a : α), 2 ^ ell a ≤ 2 * m a + 1) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => checkSmallBiasShifts (ell a) (d a) (maxBiasNum a) (maxBiasDen a) (shifts a)) encIn Turing.MultiTapeTM.encBool

Specialization of checkSmallBiasShifts_polyTime when 2 ^ ell ≤ 2 * m + 1.

def Cslib.Complexity.InitialTestsSearch.checkLocalCodeDistance (c d minDist : ℕ) (H0 : List (List Bool)) : Bool

Streaming local-code distance checker ([OAI26c], Lemma 6.1) via IndexFold.run: checks that H0 has c rows of length d and every nonzero w ∈ {0, 1} ^ d \ {0} in its GF(2) kernel has Hamming weight at least minDist, returning false on any violation.

theorem Cslib.Complexity.InitialTestsSearch.checkLocalCodeDistance_eq_true_iff (c d minDist : ℕ) (H0 : List (List Bool)) : checkLocalCodeDistance c d minDist H0 = true ↔ H0.length = c ∧ (∀ row ∈ H0, row.length = d) ∧ ∀ (w : Fin d → Bool), w ≠ 0 → (∀ (i : Fin c), BitString.ofList d (H0.getD ↑i []) ⬝ᵥ w = false) → minDist ≤ BitString.weight w

Exact characterization of checkLocalCodeDistance.

theorem Cslib.Complexity.InitialTestsSearch.checkLocalCodeDistance_computableInO : ∃ (pT : ℕ → ℕ) (pS : ℕ → ℕ), PolynomiallyBounded pT ∧ PolynomiallyBounded pS ∧ have encQ := Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary)) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits); Turing.MultiTapeTM.ComputableInO (fun (q : (ℕ × ℕ × ℕ) × List (List Bool)) => checkLocalCodeDistance q.1.1 q.1.2.1 q.1.2.2 q.2) encQ Turing.MultiTapeTM.encBool (fun (q : (ℕ × ℕ × ℕ) × List (List Bool)) => (2 ^ q.1.2.1 + 1) * pT (encQ q).length) fun (q : (ℕ × ℕ × ℕ) × List (List Bool)) => pS (encQ q).length

Native ComputableInO certificate for checkLocalCodeDistance.

Sequential IndexFold searchers

def Cslib.Complexity.InitialTestsSearch.findSmallBiasShifts (ell d maxBiasNum maxBiasDen : ℕ) : List (List Bool)

Sequential IndexFold search ([OAI26c], Lemma 6.1) over 0 .. 2 ^ (d * ell) - 1, returning the first d × ell shift table passing checkSmallBiasShifts, or the total all-false fallback listRows d ell [] when no candidate passes.

theorem Cslib.Complexity.InitialTestsSearch.isSmallBias_findSmallBiasShifts {ell d maxBiasNum maxBiasDen : ℕ} [NeZero d] (hden : 0 < maxBiasDen) (hex : ∃ (s : Fin d → Fin ell → Bool), BitString.IsSmallBias (↑maxBiasNum / ↑maxBiasDen) (PMF.map s (Probability.PMF.uniformOfFintype (Fin d)))) : have shifts := findSmallBiasShifts ell d maxBiasNum maxBiasDen; checkSmallBiasShifts ell d maxBiasNum maxBiasDen shifts = true ∧ shifts.length = d ∧ (∀ row ∈ shifts, row.length = ell) ∧ BitString.IsSmallBias (↑maxBiasNum / ↑maxBiasDen) (PMF.map (fun (j : Fin d) => BitString.ofList ell (shifts.getD ↑j [])) (Probability.PMF.uniformOfFintype (Fin d)))

Soundness of findSmallBiasShifts for d ≥ 1 and 0 < maxBiasDen when a witness exists.

theorem Cslib.Complexity.InitialTestsSearch.findSmallBiasShifts_computableInO : ∃ (pT : ℕ → ℕ) (pS : ℕ → ℕ), PolynomiallyBounded pT ∧ PolynomiallyBounded pS ∧ have encH := Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat)); Turing.MultiTapeTM.ComputableInO (fun (p : ℕ × ℕ × ℕ × ℕ) => findSmallBiasShifts p.1 p.2.1 p.2.2.1 p.2.2.2) encH (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) (fun (p : ℕ × ℕ × ℕ × ℕ) => (2 ^ (p.2.1 * p.1) + 1) * (2 ^ p.1 + 1) * pT (encH p).length) fun (p : ℕ × ℕ × ℕ × ℕ) => pS (encH p).length

Native ComputableInO certificate for findSmallBiasShifts.

def Cslib.Complexity.InitialTestsSearch.findLocalCheckMatrix (c d minDist : ℕ) : List (List Bool)

Sequential IndexFold search ([OAI26c], Lemma 6.1) over 0 .. 2 ^ (c * d) - 1, returning the first c × d check matrix passing checkLocalCodeDistance, or the total all-false fallback listRows c d [] when no candidate passes.

theorem Cslib.Complexity.InitialTestsSearch.weight_le_of_findLocalCheckMatrix {c d minDist : ℕ} (hex : ∃ (A : Fin c → Fin d → Bool), ∀ (w : Fin d → Bool), w ≠ 0 → (∀ (i : Fin c), A i ⬝ᵥ w = false) → minDist ≤ BitString.weight w) : have H0 := findLocalCheckMatrix c d minDist; checkLocalCodeDistance c d minDist H0 = true ∧ H0.length = c ∧ (∀ row ∈ H0, row.length = d) ∧ ∀ (w : Fin d → Bool), w ≠ 0 → (∀ (i : Fin c), BitString.ofList d (H0.getD ↑i []) ⬝ᵥ w = false) → minDist ≤ BitString.weight w

Soundness of findLocalCheckMatrix when a check matrix of distance minDist exists.

theorem Cslib.Complexity.InitialTestsSearch.findLocalCheckMatrix_computableInO : ∃ (pT : ℕ → ℕ) (pS : ℕ → ℕ), PolynomiallyBounded pT ∧ PolynomiallyBounded pS ∧ have encH := Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary); Turing.MultiTapeTM.ComputableInO (fun (p : ℕ × ℕ × ℕ) => findLocalCheckMatrix p.1 p.2.1 p.2.2) encH (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) (fun (p : ℕ × ℕ × ℕ) => (2 ^ (p.1 * p.2.1) + 1) * (2 ^ p.2.1 + 1) * pT (encH p).length) fun (p : ℕ × ℕ × ℕ) => pS (encH p).length

Native ComputableInO certificate for findLocalCheckMatrix.

Shortened Tanner parity-check matrix builder

def Cslib.Complexity.InitialTestsSearch.buildShortenedTannerRows (m ell d c : ℕ) (shifts H0 : List (List Bool)) : List (List Bool)

Construct the 2 * 2 ^ ell * c parity-check rows of length m for the shortened Tanner code ([OAI26c], Lemma 6.1, p. 42), matching Cslib.BitString.Tanner.shortRow. Fills entries with false when d = 0 and pads/truncates missing shifts or H0 entries with false.

@[simp]

theorem Cslib.Complexity.InitialTestsSearch.length_buildShortenedTannerRows (m ell d c : ℕ) (shifts H0 : List (List Bool)) : (buildShortenedTannerRows m ell d c shifts H0).length = 2 * 2 ^ ell * c

theorem Cslib.Complexity.InitialTestsSearch.length_mem_buildShortenedTannerRows {m ell d c : ℕ} {shifts H0 : List (List Bool)} {row : List Bool} (hrow : row ∈ buildShortenedTannerRows m ell d c shifts H0) : row.length = m

theorem Cslib.Complexity.InitialTestsSearch.count_true_mem_buildShortenedTannerRows_le {m ell d c : ℕ} (hd : 0 < d) (hm : m ≤ 2 ^ ell * d) {shifts H0 : List (List Bool)} {row : List Bool} (hrow : row ∈ buildShortenedTannerRows m ell d c shifts H0) : List.count true row ≤ d

theorem Cslib.Complexity.InitialTestsSearch.le_weight_of_buildShortenedTannerRows {m ell d c maxBiasNum maxBiasDen h : ℕ} [NeZero d] (hden : 0 < maxBiasDen) (hm : m ≤ 2 ^ ell * d) {shifts H0 : List (List Bool)} (hshifts : checkSmallBiasShifts ell d maxBiasNum maxBiasDen shifts = true) (hH0 : checkLocalCodeDistance c d (h + 1) H0 = true) {z : Fin m → Bool} (hz0 : z ≠ 0) (hz : ∀ row ∈ buildShortenedTannerRows m ell d c shifts H0, BitString.ofList m row ⬝ᵥ z = false) : ↑(h + 1) * (↑(h + 1) - ↑maxBiasNum / ↑maxBiasDen * ↑d) * 2 ^ ell ≤ ↑d * ↑(BitString.weight z)

Distance transfer from Tanner.le_weight_of_shortRow for d ≥ 1, 0 < maxBiasDen.

theorem Cslib.Complexity.InitialTestsSearch.le_mul_weight_of_buildShortenedTannerRows_params {n m B : ℕ} (hn : 1 ≤ n) (hm : 1 ≤ m) (hB : 1 ≤ B) (hmn : m ≤ B * n) {shifts H0 : List (List Bool)} (hshifts : checkSmallBiasShifts (ellG m B) (dG m B) 1 (biasDen m B) shifts = true) (hH0 : checkLocalCodeDistance (cG m B) (dG m B) (hDist m B + 1) H0 = true) : have rows := buildShortenedTannerRows m (ellG m B) (dG m B) (cG m B) shifts H0; rows.length ≤ 3 * n ∧ (∀ row ∈ rows, row.length = m ∧ List.count true row ≤ BitString.initialRowWeightBound B m) ∧ ∀ (z : Fin m → Bool), z ≠ 0 → (∀ row ∈ rows, BitString.ofList m row ⬝ᵥ z = false) → m ≤ BitString.greedyRowListLength B m * BitString.weight z

Specialization of buildShortenedTannerRows to Lemma 6.1 (1 ≤ n, m, B, m ≤ B * n).

theorem Cslib.Complexity.InitialTestsSearch.buildShortenedTannerRows_polyTime {α : Type} {encIn : α ↪ List Bool} {m ell d c bound : α → ℕ} {shifts H0 : α → List (List Bool)} (hm : Turing.MultiTapeTM.ComputableInPolyTime m encIn Turing.MultiTapeTM.encUnary) (hell : Turing.MultiTapeTM.ComputableInPolyTime ell encIn Turing.MultiTapeTM.encUnary) (hd : Turing.MultiTapeTM.ComputableInPolyTime d encIn Turing.MultiTapeTM.encUnary) (hc : Turing.MultiTapeTM.ComputableInPolyTime c encIn Turing.MultiTapeTM.encUnary) (hbound : Turing.MultiTapeTM.ComputableInPolyTime bound encIn Turing.MultiTapeTM.encUnary) (hshifts : Turing.MultiTapeTM.ComputableInPolyTime shifts encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) (hH0 : Turing.MultiTapeTM.ComputableInPolyTime H0 encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) (hle : ∀ (a : α), 2 ^ ell a ≤ bound a) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => buildShortenedTannerRows (m a) (ell a) (d a) (c a) (shifts a) (H0 a)) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)

Plain polynomial-time certificate for buildShortenedTannerRows when 2 ^ ell ≤ bound.

Unconditional Lemma 6.1 initial-tests assembly and native resource bounds

def Cslib.Complexity.InitialTestsSearch.initialTestsRows (m B : ℕ) : List (List Bool)

Deterministic Lemma 6.1 construction of the initial parity-check matrix A^(0) via findSmallBiasShifts, findLocalCheckMatrix, and buildShortenedTannerRows. Returns [] in the degenerate cases m = 0 or B = 0.

theorem Cslib.Complexity.InitialTestsSearch.initialTestsRows_spec {n m B : ℕ} (hn : 1 ≤ n) (hB : 1 ≤ B) (hmn : m ≤ B * n) : have rows := initialTestsRows m B; rows.length ≤ 3 * n ∧ (∀ row ∈ rows, row.length = m ∧ List.count true row ≤ BitString.initialRowWeightBound B m) ∧ ∀ (z : Fin m → Bool), z ≠ 0 → (∀ row ∈ rows, BitString.ofList m row ⬝ᵥ z = false) → m ≤ BitString.greedyRowListLength B m * BitString.weight z

Unconditional correctness of initialTestsRows ([OAI26c], 6.1) for 1 ≤ n, B and m ≤ B * n.

theorem Cslib.Complexity.InitialTestsSearch.map_ofList_initialTestsRows_spec {n m B : ℕ} (hn : 1 ≤ n) (hB : 1 ≤ B) (hmn : m ≤ B * n) : have rows := List.map (BitString.ofList m) (initialTestsRows m B); rows.length ≤ 3 * n ∧ (∀ r ∈ rows, BitString.weight r ≤ BitString.initialRowWeightBound B m) ∧ ∀ (z : Fin m → Bool), z ≠ 0 → (∀ r ∈ rows, r ⬝ᵥ z = false) → m ≤ BitString.greedyRowListLength B m * BitString.weight z

Executable witness matching Cslib.BitString.exists_initialTests for 1 ≤ n, B and m ≤ B * n.

theorem Cslib.Complexity.InitialTestsSearch.div_greedyRowListLength_le_weight_of_initialTestsRows {n m B : ℕ} (hn : 1 ≤ n) (hB : 1 ≤ B) (hmn : m ≤ B * n) {z : Fin m → Bool} (hz0 : z ≠ 0) (hz : ∀ row ∈ initialTestsRows m B, BitString.ofList m row ⬝ᵥ z = false) : ↑m / ↑(BitString.greedyRowListLength B m) ≤ ↑(BitString.weight z)

Real division corollary (m : ℝ) / greedyRowListLength B m ≤ weight z for 1 ≤ n, B and m ≤ B * n.

theorem Cslib.Complexity.InitialTestsSearch.initialTestsRows_computableInO : ∃ (q : ℕ → ℕ) (S : ℕ → ℕ), PolynomiallyBounded q ∧ PolynomiallyBounded S ∧ Turing.MultiTapeTM.ComputableInO (fun (p : ℕ × ℕ) => initialTestsRows p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) (fun (p : ℕ × ℕ) => 2 ^ q (p.2 + Nat.log 2 (p.1 + 2))) fun (p : ℕ × ℕ) => S (p.1 + p.2)

Native ComputableInO certificate for initialTestsRows on unary (m, B), proving pure 2 ^ q (B + Nat.log 2 (m + 2)) time and S (m + B) space.

theorem Cslib.Complexity.InitialTestsSearch.initialTestsRows_computableInO_nmb : ∃ (q : ℕ → ℕ) (S : ℕ → ℕ), PolynomiallyBounded q ∧ PolynomiallyBounded S ∧ Turing.MultiTapeTM.ComputableInO (fun (p : ℕ × ℕ × ℕ) => initialTestsRows p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary)) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) (fun (p : ℕ × ℕ × ℕ) => p.1 + 2 ^ q (p.2.2 + Nat.log 2 (p.2.1 + 2))) fun (p : ℕ × ℕ × ℕ) => S (p.1 + p.2.1 + p.2.2)

Triple-input (n, m, B) form of initialTestsRows_computableInO on unary (n, m, B), proving n + 2 ^ q (B + Nat.log 2 (m + 2)) time (where + n scans past the unary n prefix on the input tape) and S (n + m + B) space.