Circuit lower bounds and kolmogorov complexity 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) &gt; 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?
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&gt;g^{-1}(c \cdot BB(T))$, what is a number that we cannot compute (because of $BB$), so there is no problem at all.