Circuit lower bounds and kolmogorov complexity

Question

Consider the following reasoning:

Let $K(x)$ denote the Kolmogorov complexity of the string $x$. Chaitin's incompleteness theorem says that

for any consistent and sufficiently strong formal system $S$, there exists a constant $T$ (depending only on the formal system and its language) such that for any strings $x$, $S$ cannot prove that $K(x) \geq T$.

Let $f_n$ be a Boolean function on $n$ variables s.t. the Kolmogorov complexity of its spectrum is at most $k$. Let $S(f_n)$ be the circuit complexity of $f_n$, i.e. the size of the minimal circuit computing $f_n$.

A (rough) upper bound on for $S(f_n)$ is $$S(f_n)\leq c\cdot BB(k) \cdot n$$ for a constant $c$ and $BB(k)$ is a busy beaver function (the maximum possible steps a halting Turing machine with a description of size $k$ can perform). (For every $1$ in the spectrum, construct the minterm of the corresponding truth assignment, and take OR of all these minterms together.)

Suppose now for an infinite family of Boolean functions $L = \{f_n\}_{n}$, we have a formal proof that $L$ requires superlinear size circuits, i.e.

$$S \vdash \forall n \geq n_0, \ g(n)\cdot n \leq S(f_n)$$ where $g(n)\in \omega(1)$.

If we take $n$ to be sufficiently large, we will have $$g(n) > c\cdot BB(T)$$

In particular this would be a proof that the Kolmogorov complexity of the spectrum of $f_n$ is at least $T$, which is impossible.

This leads to two questions:

1) There should be something wrong in the above reasoning. Mainly because it would make superlinear circuit lower bounds formally not provable.

2) Do you know of similar approaches to show barriers for lower bounds, that is, showing that certain types of (circuit) lower bounds are formally unprovable?

Answer 1

There is nothing wrong with your argument, but there is no contradiction. You prove that from some large enough $N$ the Kolmogorov complexity of the spectrum of $f_n$ is always at least $T$. But this statement is trivially true! Although we cannot prove that the Kolmogorov complexity of one string is large, if we have a sequence, then from some point it must contain only strings of large complexity. So what is this $N$ that you got? It must satisfy $N>g^{-1}(c \cdot BB(T))$, what is a number that we cannot compute (because of $BB$), so there is no problem at all.

Answer 2

Here is an even simpler problematic situation. Let $A(k)$ be the first string (in lexicographic order) such that $K(A(k)) \geq k$; such a string provably exists for all $k$. Then $K(A(k)) \geq k$.

The culprit might be that the formal system cannot compute $BB(T)$.

Edit: Here is a "more explicit" problematic situation. Let $\alpha(k)$ be the maximal length of a string whose Kolmogorov complexity is at most $k$; $\alpha(k)$ provably exists. Then $K(0^{\alpha(k)+1}) > k$.