We prove that for some constant $a > 1$, for all $k \leq a$,
$$\mathbf{MATIME}[n^{k + o(1)}] / 1 \not \subset \mathbf{SIZE}[O(n^{k})],$$
for some specific $o(1)$ function. This is a super linear polynomial circuit lower bound.

Previously, Santhanam showed that there exists a constant $c>1$ such that for all $k > 1$:
$$\mathbf{MATIME}[n^{c k}] / 1 \not \subset \mathbf{SIZE}[O(n^{k})].$$
Inherently to Santhanam's proof, $c$ is a large constant and there is no upper bound on $c$. Using ideas from Murray and Williams, one can show for all $k > 1$:
$$\mathbf{MATIME}[n^{10 k^2}] / 1 \not \subset \mathbf{SIZE}[O(n^{k})].$$

To prove this result, we construct the first $\mathbf{PCP}$ for $\mathbf{SPACE}[n]$ with quasi-linear verifier time: our $\mathbf{PCP}$ has a $\tilde{O}(n)$ time verifier, $\tilde{O}(n)$ space prover, $O(\log(n))$ queries, and polynomial alphabet size. Prior to this work, $\mathbf{PCP}$s for $\mathbf{SPACE}[O(n)]$ had verifiers that run in $\Omega(n^2)$ time. This $\mathbf{PCP}$ also proves that $\mathbf{NE}$ has $\mathbf{MIP}$ verifiers which run in time $\tilde{O}(n)$.

1. Added a tradeoff lemma showing that if for the a in the main result, for any k,
$$\mathbf{MATIME}[n^{k + o(1)}] / 1 \not \subset \mathbf{SIZE}[O(n^{ak})].$$
2. Noted that the verifier time of this PCP implies a more fine grain relationship between NEXP and MIP.
3. Change to the introduction to further emphasize the interest of this problem.
4. Updated note in open problems about improving the proof length of PCPs with this verifier time. Specifically, it seems like BGHSV MIGHT actually have this verifier time, but that PCP is harder to analyze than ours. It does NOT however have quasilinear length.
5. Various spelling fixes and bibliography fixes.

We prove that for some constant $a > 1$, for all $k \leq a$,
$$\mathbf{MATIME}[n^{k + o(1)}] / 1 \not \subset \mathbf{SIZE}[O(n^{k})],$$
for some specific $o(1)$ function. Previously, Santhanam showed that there exists a constant $c>1$ such that for all $k > 1$:
$$\mathbf{MATIME}[n^{c k}] / 1 \not \subset \mathbf{SIZE}[O(n^{k})].$$
Inherently to Santhanam's proof, $c$ is a large constant and there is no upper bound on $c$. Using ideas from Murray and Williams, for all $k > 1$:
$$\mathbf{MATIME}[n^{10 k^2}] / 1 \not \subset \mathbf{SIZE}[O(n^{k})].$$

Our proof uses a new, very efficient $\mathbf{PCP}$ for $\mathbf{PSPACE}$. We construct a $\mathbf{PCP}$ for $\mathbf{SPACE}[O(n)]$ that has a $\tilde{O}(n)$ time verifier, $\tilde{O}(n)$ space prover, $O(\log(n))$ queries, and polynomial alphabet size. Prior to this work, $\mathbf{PCP}$s for $\mathbf{SPACE}[O(n)]$ either used $\Omega(n)$ queries or had verifiers that run in $\Omega(n^2)$ time.

1. Revised and simplified introduction.
2. Added some more notes about limitations of this result.
3. Added a new section outlining a strengthening of this result to OMA versus BPP/poly.
4. Other minor grammar fixes and slight changes to the PCP proof.

We prove for some constant $a > 1$, for all $k \leq a$,
$$\mathbf{MATIME}[n^{k + o(1)}] / 1 \not \subset \mathbf{SIZE}[O(n^{k})],$$
for some specific $o(1)$ function. This improves on the Santhanam lower bound, which says there exists constant $c$ such that for all $k > 1$:
$$\mathbf{MATIME}[n^{c k}] / 1 \not \subset \mathbf{SIZE}[O(n^{k})].$$
There is inherently no upper bound on $c$ in Santhanam's proof. Using ideas from Murray and Williams, all $k > 1$:
$$\mathbf{MATIME}[n^{10 k^2}] / 1 \not \subset \mathbf{SIZE}[O(n^{k})].$$

Our proof uses a new, very efficient $\mathbf{PCP}$ for $\mathbf{PSPACE}$. We construct a $\mathbf{PCP}$ with unbounded proof length for $\mathbf{SPACE}[O(n)]$ that has a $\tilde{O}(n)$ time verifier, $\tilde{O}(n)$ space prover, $O(\log(n))$ queries, and polynomial alphabet size. Prior to this work, $\mathbf{PCP}$s for $\mathbf{SPACE}[O(n)]$ either used $\Omega(n)$ queries or had verifiers that run in $\Omega(n^2)$ time.