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}.