Following the paper of Alekhnovich, Ben-Sasson, Razborov, Wigderson \cite{ABRW04} we call a pseudorandom generator $\mathcal{F}\colon \{0, 1\}^n \to \{0, 1\}^m$ hard for a propositional proof system $\mathrm{P}$ if $\mathrm{P}$ cannot efficiently prove the (properly encoded) statement $b \notin \Img(\PRG)$ for any string $b \in \{0, 1\}^m$.

In \cite{ABRW04} the authors suggested the ``functional encoding'' of the considered statement for Nisan--Wigderson generator that allows the introduction of ``local'' extension variables. These extension variables may potentially significantly increase the power of the proof system. In \cite{ABRW04} authors gave a lower bound of $\exp\left[\Omega\left(\frac{n^2}{m \cdot 2^{2^{\Delta}}}\right)\right]$ on the length of Resolution proofs where $\Delta$ is the degree of the dependency graph of the generator. This lower bound meets the barrier for the restriction technique.

In this paper, we introduce a ``heavy width'' measure for Resolution that allows us to show a lower bound of $\exp\left[\frac{n^2}{m 2^{\mathcal{O}(\varepsilon \Delta)}}\right]$ on the length of Resolution proofs of the considered statement for the Nisan--Wigderson generator. This gives an exponential lower bound up to $\Delta \coloneqq \log^{2 - \delta} n$ (the bigger degree the more extension variables we can use). In \cite{ABRW04} authors left an open problem to get rid of scaling factor $2^{2^{\Delta}}$, it is a solution to this open problem.

The notion of ``Canonical representation'' is replaced by the notion of ``Functional representation''. The new notion is stable under partial assignments (Lemma 3.3), which was not held for the Canonical representation.

Minor corrections.

Following the paper of Alekhnovich, Ben-Sasson, Razborov, Wigderson \cite{ABRW04} we call a pseudorandom generator $\mathrm{PRG}\colon \{0, 1\}^n \to \{0, 1\}^m$ hard for for a propositional proof system $\mathrm{P}$ if $\mathrm{P}$ cannot efficiently prove the (properly encoded) statement $b \notin \mathrm{Im}(\mathrm{PRG})$ for any string $b \in \{0, 1\}^m$.

In \cite{ABRW04} authors suggested the ``functional encoding'' of considered statement for Nisan--Wigderson generator that allows the introduction of ``local'' extension variables. These extension variables may potentially significantly increase the power of the proof system. In \cite{ABRW04} authors gave a lower bound $\exp\left[\frac{n^2}{m \Omega\left(2^{2^{\Delta}}\right)}\right]$ on the length of Resolution proofs where $\Delta$ is the degree of the dependency graph of the generator. This lower bound meets the barrier for the restriction technique.

In this paper, we introduce a ``heavy width'' measure for Resolution that allows showing a lower bound $\exp\left[\frac{n^2}{m 2^{O(\varepsilon \Delta)}}\right]$ on the length of Resolution proofs of the considered statement for the Nisan--Wigderson generator. This gives an exponential lower bound up to $\Delta := \log^{2 - \delta} n$ (the bigger degree the more extension variables we can use). It is a solution to an open problem from \cite{ABRW04}.