Instantiating Section 3–4 replacement designs at the concrete Lemma 4.8 parameter schedule

Section 4.7 of [OpenAI2026ETH] (Lemma 4.8, equations (4.17)–(4.18), pp. 34–35) chooses the concrete polylogarithmic parameter schedule (numGroups n, numNodes n, rowBound β n, auxDim n, tau n, intervalStart β n) so that all numerical hypotheses of Lemma 4.7 hold for sufficiently large n and the three-term counting-cost rate $$ \frac{R}{Q} \log \frac{2Q}{R} + \tau \log(2D + 1) + \frac{1}{r} $$ is bounded by $O_\beta(\nu^2 / \sqrt{\lambda}) = o(1)$.

This module connects Cslib.Complexity.SubexponentialSAT.ReplacementParams with the concrete algebraic replacement design construction Cslib.LinearAlgebra.ReplacementDesign (Lemma 4.7) and the shared-summary counting design interface Cslib.ReplacementCounting.Design (Definition 3.1 and Proposition 3.4):

1. Exact rational-to-real alignment of the schedule parameters:

   • tauRat n : ℚ := 1 / ((numGroups n : ℚ) * Nat.clog 2 n) casts to tau n : ℝ.
   • When 1 ≤ numGroups n and 1 ≤ rowBound β n, the rational binomial tail probability binomTailProb (numNodes n) (numGroups n) (intervalStart β n) (rowBound β n) casts to binomTail β n : ℝ (cast_binomTailProb_eq_binomTail).
   • Cslib.ReplacementCounting.threeTermExponent (numGroups n) (numNodes n) (rowBound β n) (auxDim n) (tau n) is definitionally equal to rowCost β n (threeTermExponent_eq_rowCost).

2. From Feasible to concrete and counting replacement designs:

   • Feasible.exists_replacementDesign: any Feasible β n b w (∑ f, #(scope f)) instance on a factor scope family scope : F → Finset (Fin n) with 1 ≤ b, w, per-variable degree ≤ b, per-factor width ≤ w, and total incidence ∑ f, #(scope f) ≤ b * n yields a concrete Cslib.LinearAlgebra.ReplacementDesign at the Lemma 4.8 schedule.
   • Feasible.toCountingDesign and Feasible.domainExaminationBound_le_mul_exp_rowCost: converts any concrete schedule design into a Cslib.ReplacementCounting.Design whose Proposition 3.4 domain-examination count is bounded by 2 * numNodes n * numGroups n * exp ((c + 4) * n * rowCost β n) and hence by the explicit O_β(n * ν² / √λ) subexponential bound of Lemma 4.8.
   • exists_schedule_replacementDesign: combines exists_feasible (Lemma 4.8) with Feasible.exists_replacementDesign (Lemma 4.7) to give the uniform n₀ ≥ 20 threshold for the polylogarithmic regime 1 ≤ b, w ≤ (Nat.clog 2 n) ^ β and n ≤ M ≤ b * n.

Main definitions

• Cslib.Complexity.SubexponentialSAT.ReplacementParams.tauRat: rational step scale 1 / (numGroups n * Nat.clog 2 n) : ℚ.
• Cslib.Complexity.SubexponentialSAT.ReplacementParams.Feasible.toCountingDesign: canonical Cslib.ReplacementCounting.Design attached to a concrete schedule ReplacementDesign.

Main results

• Cslib.Complexity.SubexponentialSAT.ReplacementParams.cast_binomTailProb_eq_binomTail: ((binomTailProb (numNodes n) (numGroups n) (intervalStart β n) (rowBound β n) : ℚ) : ℝ) = binomTail β n.
• Cslib.Complexity.SubexponentialSAT.ReplacementParams.threeTermExponent_eq_rowCost: threeTermExponent at the Lemma 4.8 schedule equals rowCost β n.
• Cslib.Complexity.SubexponentialSAT.ReplacementParams.Feasible.exists_replacementDesign, Cslib.Complexity.SubexponentialSAT.ReplacementParams. exists_schedule_replacementDesign: end-to-end Lemma 4.7 + Lemma 4.8 + Proposition 3.4 mathematical assembly.

References

• OpenAI, The Exponential Time Hypothesis is False, Section 3.5, Proposition 3.4, pp. 25–26; Section 4.6, Lemma 4.7, pp. 33–34; Section 4.7, Lemma 4.8, pp. 34–35.

1. Rational parameter alignment with Lemma 4.7

def Cslib.Complexity.SubexponentialSAT.ReplacementParams.tauRat (n : ℕ) : ℚ

Rational measurement step scale τ = 1 / (r λ) ∈ ℚ of equation (4.17) ([OAI26c], p. 34).

@[simp]

theorem Cslib.Complexity.SubexponentialSAT.ReplacementParams.cast_tauRat (n : ℕ) : ↑(tauRat n) = tau n

Casting tauRat n to ℝ recovers tau n.

theorem Cslib.Complexity.SubexponentialSAT.ReplacementParams.notMem_interval_iff {β n k : ℕ} (hR : 1 ≤ rowBound β n) : k ∉ interval β n ↔ k < intervalStart β n ∨ intervalStart β n + rowBound β n ≤ k

When 1 ≤ rowBound β n, membership in interval β n is equivalent to lying in [intervalStart β n, intervalStart β n + rowBound β n).

theorem Cslib.Complexity.SubexponentialSAT.ReplacementParams.cast_binomTailProb_eq_binomTail {β n : ℕ} (hr : 1 ≤ numGroups n) (hR : 1 ≤ rowBound β n) : ↑(LinearAlgebra.binomTailProb (numNodes n) (numGroups n) (intervalStart β n) (rowBound β n)) = binomTail β n

When 1 ≤ numGroups n and 1 ≤ rowBound β n, casting the rational binomial tail probability binomTailProb (numNodes n) (numGroups n) (intervalStart β n) (rowBound β n) to ℝ gives binomTail β n.

@[simp]

theorem Cslib.Complexity.SubexponentialSAT.ReplacementParams.threeTermExponent_eq_rowCost (β n : ℕ) : ReplacementCounting.threeTermExponent (numGroups n) (numNodes n) (rowBound β n) (auxDim n) (tau n) = rowCost β n

The three-term counting-cost rate threeTermExponent instantiated at the Lemma 4.8 schedule is definitionally equal to rowCost β n.

2. Extracting Lemma 4.7 hypotheses and designs from Feasible

theorem Cslib.Complexity.SubexponentialSAT.ReplacementParams.Feasible.one_le_n {β n b w M : ℕ} (hF : Feasible β n b w M) : 1 ≤ n

1 ≤ n holds under Feasible β n b w M.

theorem Cslib.Complexity.SubexponentialSAT.ReplacementParams.Feasible.one_le_rowBound {β n b w M : ℕ} (hF : Feasible β n b w M) : 1 ≤ rowBound β n

1 ≤ rowBound β n holds under Feasible β n b w M.

theorem Cslib.Complexity.SubexponentialSAT.ReplacementParams.Feasible.rowBound_lt_numNodes {β n b w M : ℕ} (hF : Feasible β n b w M) : rowBound β n < numNodes n

rowBound β n < numNodes n holds under Feasible β n b w M.

theorem Cslib.Complexity.SubexponentialSAT.ReplacementParams.Feasible.tauRat_pos {β n b w M : ℕ} (hF : Feasible β n b w M) : 0 < tauRat n

0 < tauRat n holds under Feasible β n b w M.

theorem Cslib.Complexity.SubexponentialSAT.ReplacementParams.Feasible.tauRat_le_half {β n b w M : ℕ} (hF : Feasible β n b w M) : tauRat n ≤ 1 / 2

tauRat n ≤ 1 / 2 holds under Feasible β n b w M.

theorem Cslib.Complexity.SubexponentialSAT.ReplacementParams.Feasible.intervalStart_add_le_numNodes {β n b w M : ℕ} (hF : Feasible β n b w M) {a : ℕ} (ha : a < rowBound β n) : intervalStart β n + a ≤ numNodes n

Every shift intervalStart β n + a for a < rowBound β n lies in [0, numNodes n].

theorem Cslib.Complexity.SubexponentialSAT.ReplacementParams.Feasible.binomTailProb_lt {β n b w M : ℕ} (hF : Feasible β n b w M) : LinearAlgebra.binomTailProb (numNodes n) (numGroups n) (intervalStart β n) (rowBound β n) < tauRat n / (↑(numGroups n) * ↑b)

Under Feasible β n b w M, the rational binomial tail probability satisfies Lemma 4.7's strict threshold binomTailProb < tauRat n / (numGroups n * b).

theorem Cslib.Complexity.SubexponentialSAT.ReplacementParams.Feasible.exists_replacementDesign {β n b w : ℕ} {F : Type u_1} [Fintype F] (scope : F → Finset (Fin n)) (hF : Feasible β n b w (∑ f : F, (scope f).card)) (hb_pos : 1 ≤ b) (hw_pos : 1 ≤ w) (hb : ∀ (v : Fin n), {f : F | v ∈ scope f}.card ≤ b) (hw : ∀ (f : F), (scope f).card ≤ w) (hM_le : ∑ f : F, (scope f).card ≤ b * n) : Nonempty (LinearAlgebra.ReplacementDesign scope (numNodes n) (numGroups n) (intervalStart β n) (rowBound β n) (tauRat n))

Lemma 4.7 + Lemma 4.8 concrete replacement design existence: Given hF : Feasible β n b w (∑ f, #(scope f)) on a factor scope family scope : F → Finset (Fin n) with 1 ≤ b, 1 ≤ w, per-variable occurrence ≤ b, per-factor scope size ≤ w, and total incidence ∑ f, #(scope f) ≤ b * n, there exists a concrete Section 4 ReplacementDesign scope (numNodes n) (numGroups n) (intervalStart β n) (rowBound β n) (tauRat n).

noncomputable def Cslib.Complexity.SubexponentialSAT.ReplacementParams.Feasible.toCountingDesign {β n b w M : ℕ} {F : Type u_1} [Fintype F] {scope : F → Finset (Fin n)} (hF : Feasible β n b w M) (D : LinearAlgebra.ReplacementDesign scope (numNodes n) (numGroups n) (intervalStart β n) (rowBound β n) (tauRat n)) (s : Finset F) : ReplacementCounting.Design (Fin n) s (fun (f : F) => ↥(scope f)) (fun (x : F) (v : ↥(scope x)) => ↑v) (numGroups n) (numNodes n) (rowBound β n) (auxDim n) (tau n)

Converts any concrete ReplacementDesign at the Lemma 4.8 schedule into a Section 3 Cslib.ReplacementCounting.Design for an active factor subset s : Finset F.

theorem Cslib.Complexity.SubexponentialSAT.ReplacementParams.Feasible.domainExaminationBound_le_mul_exp_rowCost {β n b w M : ℕ} {F : Type u_1} [Fintype F] {scope : F → Finset (Fin n)} (hF : Feasible β n b w M) (D : LinearAlgebra.ReplacementDesign scope (numNodes n) (numGroups n) (intervalStart β n) (rowBound β n) (tauRat n)) (s : Finset F) {q : ℕ} {c : ℝ} (hc : 0 ≤ c) (hq : ↑q ≤ c * ↑n * (↑(rowBound β n) / ↑(numNodes n))) : have C := hF.toCountingDesign D s; ∑ t : Fin (numNodes n), ↑{p : Finset (Fin n) × Finset (Fin n) | p.1.card ≤ q ∧ p.2 ⊆ p.1}.card * (2 * ↑(C.measurementBox t).card * ∑ g : Fin (numGroups n), ↑(Fintype.card (C.LocalCube t g))) ≤ 2 * ↑(numNodes n) * ↑(numGroups n) * Real.exp ((c + 4) * ↑n * rowCost β n) ∧ 2 * ↑(numNodes n) * ↑(numGroups n) * Real.exp ((c + 4) * ↑n * rowCost β n) ≤ 2 * ↑(numNodes n) * ↑(numGroups n) * Real.exp ((c + 4) * ↑n * (1028 * (↑β + 3) * ↑(Nat.clog 2 (Nat.clog 2 n)) ^ 2 / √↑(Nat.clog 2 n)))

Proposition 3.4 + Lemma 4.8 domain-examination bound in terms of rowCost β n: For any Feasible β n b w M and concrete schedule design D, the induced counting design hF.toCountingDesign D s examines at most 2 * numNodes n * numGroups n * exp ((c + 4) * n * rowCost β n) local Boolean assignments across all numNodes n nodes and all subset pairs (E, U) with #E ≤ q ((q : ℝ) ≤ c * n * (R / Q)), which in turn is bounded by 2 * numNodes n * numGroups n * exp ((c + 4) * n * (1028 * (β + 3) * ν² / √λ)).

theorem Cslib.Complexity.SubexponentialSAT.ReplacementParams.exists_schedule_replacementDesign {β : ℕ} (hβ : 1 ≤ β) : ∃ (n₀ : ℕ), 20 ≤ n₀ ∧ ∀ ⦃n b w : ℕ⦄ {F : Type u_1} [inst : Fintype F] (scope : F → Finset (Fin n)), n₀ ≤ n → 1 ≤ b → b ≤ Nat.clog 2 n ^ β → 1 ≤ w → w ≤ Nat.clog 2 n ^ β → n ≤ ∑ f : F, (scope f).card → ∑ f : F, (scope f).card ≤ b * n → (∀ (v : Fin n), {f : F | v ∈ scope f}.card ≤ b) → (∀ (f : F), (scope f).card ≤ w) → Feasible β n b w (∑ f : F, (scope f).card) ∧ Nonempty (LinearAlgebra.ReplacementDesign scope (numNodes n) (numGroups n) (intervalStart β n) (rowBound β n) (tauRat n))

Uniform Lemma 4.7 + Lemma 4.8 schedule design existence: For every integer 1 ≤ β, there exists n₀ ≥ 20 such that for all n ≥ n₀, 1 ≤ b, w ≤ (Nat.clog 2 n) ^ β, and any factor scope family scope : F → Finset (Fin n) with n ≤ ∑ f, #(scope f) ≤ b * n, per-variable occurrence ≤ b, and per-factor width ≤ w, the schedule (4.17) is Feasible and admits both a concrete ReplacementDesign and an induced Cslib.ReplacementCounting.Design.