Law of the Excluded Middle in complexity theory

Question

A recent blog post by Lance Fortnow discusses non-constructive proofs, where "non-constructive" here means that the law of the excluded middle is used in a substantive way. That is, one takes some proposition $P$ whose truth is unknown, and splits the proof into two cases: (1) $P$ is true, and (2) $P$ is false. In both cases we deduce the desired theorem, but by totally different arguments. Fortnow gives an example from complexity theory:

In complexity, a well-known non-constructive theorem is by Kannan, showing that $\Sigma_2^P$ does not have $n^2$-size circuits.

1. SAT doesn't have $n^2$-size circuits. Since SAT is in $\Sigma_2$, we are done.
2. SAT has $n^2$-size circuits. Then by Karp–Lipton, $\Sigma_4 = \Sigma_2$ so L is in $\Sigma_2$ and we are done.

My question is, are there other proofs of results in complexity theory that are non-constructive in this sense?

Sometime in the past five years, I remember seeing such a paper, but unfortunately I can't remember anything else about it. I think it was a paper that had been recently published (though there's a chance it was an older paper that I had only just learned about). I also think the topic was circuit lower bounds, though I'm even less sure about that. Anyway, I'm interested in any examples, not just the one that I'm struggling to recall.

Answer 1

There are several other non-constructive arguments that work along similar Karp-Lipton-esque lines, such as Santhanam's proof (STOC 2009) that $PromiseMA$ is not in $SIZE(n^k)$ for some $k$, and Kabanets-Impagliazzo-Volkovich's proof (CCC 2018) that $ZPEXP^{MCSP}$ is not in $P/poly$.

For a slightly different kind of example (but still regarding types of circuit lower bounds), Rahul Santhanam and I proved (CCC 2013):

$P$ is not in $P$-uniform $SIZE(n^k)$ for every fixed $k$.

(Paper at: https://people.csail.mit.edu/rrw/WeakUniformity-journal-rev.pdf)

The proof is not constructive: it does not name any function in P that exhibits the lower bound. We don't even know a time upper bound on the hard $P$-function (otherwise, we could take some generic simulation language as the hard function).

I've tried off and on for some years to give a specific function satisfying the lower bound. The best I could do so far is with Cody Murray, where we showed that there is a function in time $n^2$ that isn't in $LOGSPACE$-uniform $SIZE(n^{1+o(1)})$. See https://drops.dagstuhl.de/opus/volltexte/2017/7542/