Let $M$ be a Turing Machine for SAT. We want to encode certain paths of $M$ in a very short way in order to diagonalize against the paths.
For each natural number $k$, we will have a formula $\phi$ of length $n$ that does the following: $\phi$ is satisfiable iff the assignment encodes a run of $M$ on $\phi$ of length $n^k$ that ends in the reject state.
Suppose SAT can be computed in time $n^k$, and let $\phi$ be the formula associated with $k$. If $\phi$ is satisfiable, then the satisfying assignment encodes a run of $M$ on $\phi$ ending in the reject state. If $\phi$ is not satisfiable, then by our assumption there is a run of $M$ on $\phi$ of length $n^k$ ending in the reject state. An encoding of this path satisfies $\phi$. Contradiction. Therefore, SAT cannot be computed in time $n^k$.
Any opinions? I'm curious if anyone has an immediate reason why this wouldn't work. (I'm quite aware that it would be difficult.)