Polynomial-time parameter schedule and exact feasibility checks for subexponential #k-SAT #
In Section 4.7 (Lemma 4.8, pp. 34–35), Section 5.5 (pp. 38–39), and Section 6.4 (Proposition 6.4,
pp. 43–44) of OpenAI, The Exponential Time Hypothesis is False, a uniform
algorithm computes the discrete replacement and sparsification parameters from input sizes and
verifies the numerical hypotheses of Lemma 4.7 and Lemma 4.8 in exact integer arithmetic, falling
back to direct evaluation on the finitely many small inputs where those checks fail rather than
referencing any noncomputable threshold constant N₀.
This module certifies the schedule parameters of ReplacementParams (numGroups, numNodes,
rowBound, auxDim, intervalStart) directly under plain ComputableInPolyTime (including
Proposition 6.4's integer-comparison characterization of numGroups via s ^ 2 * ν_n ^ 4 ≤ λ_n),
adds the Section 5.5 parameter selectors (heavyDegreeCutoff, heavyIncidenceCutoff,
chooseBeta), and proves exact cleared-denominator natural-number decision procedures
(checkBinomTail, checkReplacementFeasible, checkScheduleFeasible) with bidirectional
soundness/completeness and eventual-feasibility bridges to ReplacementParams.
Main definitions #
Cslib.Complexity.SubexponentialSAT.ParameterCheck.heavyDegreeCutoff,Cslib.Complexity.SubexponentialSAT.ParameterCheck.heavyIncidenceCutoff,Cslib.Complexity.SubexponentialSAT.ParameterCheck.chooseBeta,Cslib.Complexity.SubexponentialSAT.ParameterCheck.computeScheduleParams: Section 5.5 and full Section 4.7 parameter selectors.Cslib.Complexity.SubexponentialSAT.ParameterCheck.binomTailTerm,Cslib.Complexity.SubexponentialSAT.ParameterCheck.binomTailNumerator,Cslib.Complexity.SubexponentialSAT.ParameterCheck.checkBinomTail,Cslib.Complexity.SubexponentialSAT.ParameterCheck.checkReplacementFeasible,Cslib.Complexity.SubexponentialSAT.ParameterCheck.checkScheduleFeasible: cleared-denominator natural-number Binomial-tail and Lemma 4.7 / Lemma 4.8 feasibility decision procedures.
Main results #
Cslib.Complexity.SubexponentialSAT.ParameterCheck.numGroups_eq_findGreatest: Proposition 6.4Nat.findGreatestcharacterization ofCslib.Complexity.SubexponentialSAT.ReplacementParams.numGroups(fromReplacementParams.sq_mul_pow_four_le_clogandReplacementParams.clog_lt_succ_sq_mul_pow_four).Cslib.Complexity.SubexponentialSAT.ParameterCheck.checkBinomTail_eq_true_iff,checkBinomTail_schedule_eq_true_iff,checkScheduleFeasible_eq_true_iff: exact equivalences with real Binomial tail probabilities and schedule balance bounds.Cslib.Complexity.SubexponentialSAT.ParameterCheck.checkScheduleFeasible_eq_true_of_feasible,exists_checkScheduleFeasible_eq_true,feasible_of_checkScheduleFeasible_eq_true,feasible_of_checkScheduleFeasible_chooseBeta_eq_true: completeness, eventual feasibility, and soundness againstCslib.Complexity.SubexponentialSAT.ReplacementParams.Feasible.Cslib.Complexity.SubexponentialSAT.ParameterCheck.computableInPolyTime_numGroups,computableInPolyTime_numNodes,computableInPolyTime_rowBound,computableInPolyTime_auxDim,computableInPolyTime_intervalStart,computableInPolyTime_scheduleAndCheck_binary,computableInPolyTime_scheduleAndCheck_unary: plainTuring.MultiTapeTM.ComputableInPolyTimecertificates for the schedule and checkers.
References #
- OpenAI, The Exponential Time Hypothesis is False, Section 4.6 (Lemma 4.7, pp. 33–34), Section 4.7 (Lemma 4.8, pp. 34–35), Section 5.5 (pp. 38–39), and Section 6.4 (Proposition 6.4, pp. 43–44).
1. Section 5.5 / Section 6.4 Parameter Selectors and Full Schedule Tuple #
Auxiliary fifth-power polylogarithmic cutoff λ_n ^ 5 on n variables, where
λ_n = Nat.clog 2 n.
Instances For
Heavy-incidence threshold b₀ = ⌈M / n⌉ ⌈√λ_n⌉ of Section 5.5 ([OpenAI2026ETH], p. 38) for a
system of total scope size M on n variables.
Instances For
Selector for the smallest integer β ≥ 1 satisfying b ≤ lam ^ β and w ≤ lam ^ β in
Section 5.5 ([OpenAI2026ETH], pp. 38–39), defaulting to 1 when lam ≤ 1 and max b w > 1.
Instances For
For 1 ≤ n, heavyIncidenceCutoff M n agrees with ⌈(M : ℝ) / n⌉₊ * ⌈√λ_n⌉₊ (§5.5, p. 38).
Whenever 2 ≤ lam, chooseBeta lam b w returns the smallest integer β ≥ 1 satisfying
b ≤ lam ^ β and w ≤ lam ^ β (§5.5, pp. 38–39).
Proposition 6.4 integer-comparison characterization ([OpenAI2026ETH], pp. 43–44):
ReplacementParams.numGroups n equals the Nat.findGreatest search for the largest s ≤ λ_n
satisfying s ^ 2 * ν_n ^ 4 ≤ λ_n (and 0 when ν_n = 0).
2. Cleared-Denominator ℕ Binomial-Tail and Feasibility Checkers #
Cleared-denominator integer summand Q.choose w * (r - 1) ^ w * (r + 1) ^ (Q - w) of
(2 r) ^ Q * Pr[W = w] for W ~ Bin(Q, (r - 1) / (2 r)).
Instances For
Exact cleared-denominator integer numerator (2 r) ^ Q * Pr[W ∉ [A₀, A₀ + R)) for
W ~ Bin(Q, (r - 1) / (2 r)), summing binomTailTerm Q r w over w ∈ {0, …, Q} outside
[A₀, A₀ + R).
Instances For
Exact integer decision procedure for the biased Binomial tail bound
Pr[W ∉ [A₀, A₀ + R)) ≤ 1 / (b * r ^ 2 * lam) under W ~ Bin(Q, (r - 1) / (2 r)), including
positivity guards 1 ≤ r, 1 ≤ b, and 1 ≤ lam.
Instances For
Exact integer decision procedure for the numerical hypotheses of Lemma 4.7
([OpenAI2026ETH], pp. 33–34): checks 2 ≤ r, 1 ≤ R, R < Q, A₀ + R ≤ Q + 1,
2 * (b + wmax) * (r ^ (2 * Q)) ^ 2 ≤ M, 2 * Q * r ^ 2 ≤ n, and checkBinomTail.
Instances For
Compute the full Section 4.7 schedule (λ, ν, r, Q, R, A₀) and verify in exact integer
arithmetic both the Lemma 4.8 regime conditions (20 ≤ n, 32 ≤ R, 6 * R ≤ Q) and
checkReplacementFeasible, deciding whether to run the subexponential replacement branch or the
small-n direct-evaluation fallback of Theorem 2.2 / §5.5 ([OpenAI2026ETH], p. 39).
Instances For
binomTailNumerator as a Finset sum over {0, …, Q} outside [A₀, A₀ + R).
Exact bridge from checkBinomTail to real Bin(Q, (r - 1) / (2 r)) tail probabilities:
for 1 ≤ r, 1 ≤ b, and 1 ≤ lam, checkBinomTail Q r A₀ R b lam = true holds if and only if
the real Binomial tail outside [A₀, A₀ + R) is at most 1 / (b * r ^ 2 * lam).
Closed-interval (Finset.Icc A₀ (A₀ + R - 1)) form of checkBinomTail_eq_true_iff whenever
1 ≤ R, matching the interval I = {A₀, …, A₀ + R - 1} of Lemma 4.8.
Schedule specialization of checkBinomTail_eq_true_iff_notMem_Icc: on equation (4.17)'s
schedule, checkBinomTail decides
ReplacementParams.binomTail β n ≤ ReplacementParams.tailBudget b n exactly.
Soundness and completeness characterization of checkReplacementFeasible, unpacking all
numerical balance bounds and the exact real Binomial tail inequality.
Exact characterization of checkScheduleFeasible in terms of ReplacementParams.
Completeness of checkScheduleFeasible against ReplacementParams.Feasible: every feasible
instance passes the exact integer-arithmetic feasibility checker.
Eventual passage of checkScheduleFeasible (Lemma 4.8, [OpenAI2026ETH], p. 34:
"For fixed β, only finitely many n fail these checks"): for every 1 ≤ β, there exists
n₀ ≥ 20 above which checkScheduleFeasible n M b w β = true holds for all valid (b, w, M).
Soundness of checkScheduleFeasible against ReplacementParams.Feasible: when 1 ≤ β and
b ≤ λ_n ^ β, passing checkScheduleFeasible n M b w β implies the full
ReplacementParams.Feasible bundle, including the strict Binomial tail bound and equation (4.18)'s
rowCost bound.
Automatic soundness of checkScheduleFeasible when β = chooseBeta (Nat.clog 2 n) b w
(§5.5, pp. 38–39), needing no external 1 ≤ β or b ≤ λ_n ^ β hypotheses.
3. Plain Polynomial-Time Certificates (ComputableInPolyTime) #
Internal plain building blocks #
ReplacementParams.numGroups (r) is polynomial-time over binary naturals.
ReplacementParams.numGroups (r) is polynomial-time from binary naturals to unary.
ReplacementParams.numNodes (Q) is polynomial-time over binary naturals.
ReplacementParams.numNodes (Q) is polynomial-time from binary naturals to unary.
ReplacementParams.rowBound (R) is polynomial-time over binary pairs (β, n).
ReplacementParams.auxDim (D = r ^ (2 Q) ≤ 2 ^ (λ / 128)) is polynomial-time over binary
naturals (encNat to encNat).
ReplacementParams.intervalStart (A₀) is polynomial-time over binary pairs (β, n).
heavyDegreeCutoff (λ_n ^ 5) is polynomial-time over binary naturals.
heavyIncidenceCutoff (b₀ = ⌈M / n⌉ ⌈√λ_n⌉) is polynomial-time over binary pairs (M, n).
chooseBeta is polynomial-time over binary triples (lam, b, w).
binomTailNumerator is polynomial-time with Q in encUnary and (r, A₀, R) in encNat.
binomTailNumerator is also polynomial-time when both (Q, r) are given in encUnary.
checkBinomTail is polynomial-time with Q in encUnary and (r, A₀, R, b, lam) in
encNat.
checkBinomTail is also polynomial-time when both (Q, r) are given in encUnary.
checkReplacementFeasible is polynomial-time with Q in encUnary and
(n, M, b, wmax, lam, r, A₀, R) in encNat.
checkReplacementFeasible is also polynomial-time when both (Q, r) are given in
encUnary.
Computing the full Section 4.7 schedule (λ, ν, r, Q, R, A₀) is polynomial-time over binary
pairs (β, n).
Binary-n full-schedule and feasibility certificate (Lemma 4.8, p. 34): given
(n, M, b, wmax, β) all in binary (encNat), computing (λ, ν, r, Q, R, A₀) and deciding
checkScheduleFeasible runs in polynomial time in
|encNat n| + |encNat M| + |encNat b| + |encNat wmax| + |encNat β|.
Composed unary-n full-schedule and feasibility certificate (§5.5 / Theorem 2.2): given
(n_unary, M, b, wmax, β) with n_unary in encUnary and (M, b, wmax, β) in encNat,
computing (λ, ν, r, Q, R, A₀) and running both checkReplacementFeasible and
checkScheduleFeasible is polynomial-time.