On importance of Stockmeyer theorem

Question

Theorem: (Stockmeyer, 1974) Any circuit that takes as input a formula (in the language of WS1S) with up to 616 symbols and produces as output a correct answer saying whether the formula is valid or not, requires at least $10^{123}$ gates.

Suppose we have generalized theorem: Any circuit that takes as input a formula with up to $n$ symbols and produces as output a correct answer saying whether the formula is valid or not, requires at least $10^n$ gates. Is this true that this theorem equivalent to statement that P is not equal to coNP?

Answer 1

The theorem is false. There is a circuit of size $\tilde{O}(2^n)$ that solves SAT. At any rate, the relevant conjectures you would be proving using statements of this form are the Exponential time hypothesis and its variants.