Mathematical remark

Discussion note on recorded SAT-algorithm-to-lower-bound hypotheses versus the conjecture. File-verified sources: Vyas-Williams arXiv:2001.07788v1, informal Theorems 1.1 and 1.2; Williams arXiv:1212.1891, typical-class list and Theorems 1.5 and 1.6.

Vyas-Williams Theorem 1.1 (citing Wil13/Wil14): if for every k one can solve SAT on n^k-size C-circuits in O(2^n/n^k) time, then NEXP has no polynomial-size C-circuits. For general fan-in-2 circuits this is NEXP not subset P/poly. Vyas-Williams Theorem 1.2 (citing MW18): SAT on 2^{n^eps}-size C-circuits in O(2^{n-n^eps}) time implies Quasi-NP has no polynomial-size C-circuits. Williams 1212.1891 Theorem 1.5: SAT for n^{O(log^c n)}-size typical C-circuits in O(2^n/n^{10}) time, for all c, implies NE intersect io-coNE has no n^{log n}-size C-circuits. Theorem 1.6 is the same size/time for CAPP of unrestricted fan-in-2 circuits, with the same NE/coNE conclusion. Typical C in 1212.1891 is {AC0, ACC0, TC0, NC1, NC, P/poly}; usefulness is against n^k-size C-circuits. B2-SIZE(O(n)) is not on that list.

These hypotheses miss the conjecture in three independently checkable ways. (1) Hard class: NEXP, Quasi-NP, or NE intersect io-coNE, all nondeterministic, not deterministic E. (2) Circuit size in the SAT hypothesis: every polynomial n^k, or 2^{n^eps}, or n^{O(log^c n)}, not merely linear. A SAT algorithm that works only for size-cn B2 circuits does not instantiate Theorem 1.1, which quantifies over all k. (3) Conclusion size: polynomial or n^{log n}, not the linear threshold of the conjecture. Instantiating Theorem 1.1 for general B2 would prove NEXP not subset P/poly, which is stronger than, and not a route to, some L in E outside B2-SIZE(O(n)).

A separate E-time accounting, not a SAT-to-LB theorem: exhaustive SAT on one n-input size-s circuit is modelled as 2^n * s gate evaluations. For s=3n this is 2^{n+O(log n)}, which lies in E. Kannan-style enumeration of all size-3n circuits is modelled as 2^{n+3n log2(3n)} = 2^{Theta(n log n)}, which is outside every fixed DTIME[2^{c n}]. At n=256 the model gives 7617 bits versus 512 for TIME[2^{2n}] and 5120 for TIME[2^{20n}]. So a polynomial-factor Circuit-SAT speedup on a single linear-size instance, even if obtained, does not by itself let an E-machine enumerate all linear-size circuits. Finite bookkeeping: work/code/sat_lb_accounting.py (executor).

Wil13 (SICOMP 42(3):1218-1244, 2013), Wil14 (JACM 61(1), 2014), and MW18 (STOC 2018) were not file-retrieved. export.arxiv.org title searches for Wil13 and MW18 were empty; au:Murray AND au:Williams AND all:witness returned LIGO papers. Secondary pointer only: Abboud-Hansen-Vassilevska Williams-Williams arXiv:1511.06022v1 records SETH as a linear-size CNF hypothesis and notes that SAT speedups for NC circuits would imply NEXP not subset NC^1; that is still NEXP versus a polynomial-size restricted class.

Barriers: the scoping is a comparison of recorded hypotheses, not oracle diagonalization. Natural-proof usefulness in 1212.1891 is against n^k-size typical C, which is a stronger usefulness condition than usefulness only against B2-SIZE(O(n)). Algebrization of a hypothetical linear-size SAT algorithm is not analysed here. No P vs NP claim. The GKW combinatorial s_3^{16} / Open Problem 1.1 route and the affine-disperser linear bounds are unchanged.