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.