claimroutineinferred_dep

Test-circuit runtime contradicts time hierarchy

Claim·§1 Introduction·inside corSuperlinear circuit lower bound for E^NP

Statement (paper)

C_W(dn)\le s_n

for all sufficiently large

n

, then

H

is decidable nondeterministically in time

2^{n/2}

for all sufficiently large

n

(the test circuit having at most

3s_n+O(n)

gates, hence

U_n=3s_n+Bn

variables and at most

5U_n

clauses, and being checked for unsatisfiability in time

2^{(3A\eta+o(1))n}

with

3A\eta<1/4

), and after hardwiring finitely many exceptional lengths this contradicts the choice of

H

; hence

C_W(dn)>s_n

for infinitely many

n

In plain English

C_W(dn)\le s_n

for all large

n

, then

H

can be decided nondeterministically in time

2^{n/2}

for all large

n

, contradicting the choice of

H

; hence

C_W(dn)>s_n

for infinitely many

n

Why it's here

The guessed test circuit has at most

3s_n+O(n)

gates, so it gives a 3-SAT instance with

U_n=3s_n+Bn

variables and at most

5U_n

clauses. The fast 3-SAT algorithm then checks it for unsatisfiability in time

2^{(3A\eta+o(1))n}

with

3A\eta<1/4

, which is below

2^{n/2}

. This makes the nondeterministic procedure from the previous claim too fast for the time hierarchy theorem, so the small-circuit assumption fails infinitely often, giving the corollary's lower bound.

Classified routine:

This step closes a standard Williams-style argument (faster SAT algorithms imply circuit lower bounds). It is a parameter calculation combining the two previous claims with the nondeterministic time hierarchy theorem (Cook 1972; Žák 1983), hardwiring finitely many exceptional input lengths.

Uses

claimFast 3-SAT at linear clause densityclaimSmall witness circuits give nondeterministic algorithm for H

Used by

Nothing in the paper

Sources

PaperOpen

Section: §1 Introduction
Page: —
Label: —
Line: quantitative-circuits.tex:58

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Test-circuit runtime contradicts time hierarchy" rests on claim-cor-quantitative-circuits-4
info
inferred_dep
outline: "Test-circuit runtime contradicts time hierarchy" rests on claim-cor-quantitative-circuits-5