In this paper, we obtain new size lower bounds for proofs in the
Polynomial Calculus (PC) proof system, in two different settings.

1. When the Boolean variables are encoded using $\pm 1$ (as opposed
to $0,1$): We establish a lifting theorem using an asymmetric gadget
$G$, showing that for an unsatisfiable formula $F$, the lifted
formula $F \circ G$ requires PC size $2^{\Omega(d)}$, where $d$ is
the degree required to refute $F$. Our lower bound does not depend
on the number of variables $n$, and holds over every field. The
only previously known size lower bounds in this setting were
established quite recently in [Sokolov, STOC 2020] using lifting
with another (symmetric) gadget. The size lower bound there is
$2^{\Omega((d-d_0)^2/n)}$ (where $d_0$ is the degree of the initial
equations arising from the formula), and is shown to hold only over
the reals.

2. When the PC refutation proceeds over a finite field
$\mathbb{F}_p$ and is allowed to use extension variables: We show
that there is an unsatisfiable formula with $N$ variables for which
any PC refutation using $N^{1+\epsilon(1-\delta)}$ extension
variables, each of arity at most $N^{1-\epsilon}$ and size at most
$N^c$, must have size $\exp(\Omega(N^{\epsilon\delta}/\poly\log
N))$. Our proof achieves these bounds by an XOR-ification of the
generalised PHP$^{m,r}_n$ formulas from [Razborov, CC 1998].

The only previously known lower bounds for PC in this setting are
those obtained in [ImpagliazzoMouliPitassi, CCC 2023]; in those
bounds the number of extension variables is required to be
sub-quadratic, and their arity is restricted to logarithmic in
the number of original variables. Our result generalises these,
and demonstrates a tradeoff between the number and the arity of
extension variables.

In this paper, we obtain new size lower bounds for proofs in the
Polynomial Calculus (PC) proof system, in two different settings.

1. When the Boolean variables are encoded using $\pm 1$ (as opposed
to $0,1$): We establish a lifting theorem using an asymmetric gadget
$G$, showing that for an unsatisfiable formula $F$, the lifted
formula $F \circ G$ requires PC size $2^{\Omega(d)}$, where $d$ is
the degree required to refute $F$. Our lower bound does not depend
on the number of variables $n$, and holds over every field. The
only previously known size lower bounds in this setting were
established quite recently in [Sokolov, STOC 2020] using lifting
with another (symmetric) gadget. The size lower bound there is
$2^{\Omega((d-d_0)^2/n)}$ (where $d_0$ is the degree of the initial
equations arising from the formula), and is shown to hold only over
the reals.

2. When the PC refutation proceeds over a finite field
$\mathbb{F}_p$ and is allowed to use extension variables: We show
that there is an unsatisfiable formula with $N$ variables for which
any PC refutation using $N^{1+\epsilon(1-\delta)}$ extension
variables, each of arity at most $N^{1-\epsilon}$ and size at most
$N^c$, must have size $\exp(\Omega(N^{\epsilon\delta}/\poly\log
N))$. Our proof achieves these bounds by an XOR-ification of the
generalised PHP$^{m,r}_n$ formulas from [Razborov, CC 1998].

The only previously known lower bounds for PC in this setting are
those obtained in [ImpagliazzoMouliPitassi, CCC 2023]; in those
bounds the number of extension variables is required to be
sub-quadratic, and their arity is restricted to logarithmic in
the number of original variables. Our result generalises these,
and demonstrates a tradeoff between the number and the arity of
extension variables.