main.tex

\documentclass{article}
\usepackage[logic, complexity, theorems]{commondefns}
\usepackage{csquotes}
\usepackage[style=alphabetic]{biblatex}
\addbibresource{refs.bib}
\usepackage{bussproofs}

\title{Lower Bounds for the Polynomial Calculus\\via the ``Pigeon Dance''}
\author{Imogen Hergeth}
\date{January 2023}


\newcommand{\Sn}{S_n(\KK)}
\newcommand{\Snd}{S_{n, d}(\KK)}
\newcommand{\PHP}{\ensuremath{\neg \mathcal{PHP}^m_n}\xspace}
\newcommand{\Qiij}{Q_{i_1, i_2, j}}
\newcommand{\LT}{\operatorname{LT}}
\newcommand{\Rsem}{R^\mathrm{sem}}
\newcommand{\Rsyn}{R^\mathrm{syn}}
\newcommand{\Dsem}{\Delta^\mathrm{sem}}
\newcommand{\Dsyn}{\Delta^\mathrm{syn}}
\newcommand{\fa}{\text{ for all }}
\renewcommand{\K}{\operatorname{Kill}}
\newcommand{\Is}{{I \setminus \{i_1\}}}
\newcommand{\rhoij}{\rho_{i_1 j_1}}
\newcommand{\xij}{{x_{i_1 j_1}}}


\begin{document}

\maketitle

\section{Introduction}
A major open question in complexity theory is that of $\NP \queq \co\NP$. A possible avenue to prove $\NP \neq \co\NP$ is
showing that no proof system admits a polynomial size refutation of some infinite class of unsatisfiable formulae.
So far research towards this goal has only succeeded showing much weaker lower bounds for particular proof systems.
In this article, we will discuss one such result as first presented in \cite{raz},
a linear bound on the pigeonhole principle in polynomial calculus.

The proof system we use is the \textit{polynomial calculus}. Similar to proofs in the sequence calculus or Frege systems, these consist of a directed acyclic graph where the vertices are lines and edges are inferences. The difference to the other two systems is that lines are polynomials and the two rules of inference are addition
\begin{prooftree}
    \AxiomC{$f$}
    \AxiomC{$g$}
    \BinaryInfC{$af + bg$}
\end{prooftree}
and multiplication
\begin{prooftree}
    \AxiomC{$f$}
    \UnaryInfC{$f \cdot x$}
\end{prooftree}
A polynomial calculus proof of $g$ from $f_1, \ldots, f_m$ contains $f_1, \ldots, f_m$ as axioms and ends in $g$. And a refutation of $f_1, \ldots, f_m$ is a proof of $g = 1$ from $f_1, \ldots, f_m$.\\
It is easy to see that some $g$ can be proven from $f_1, \ldots, f_m$ if and only if it is in the ideal generated by $f_1, \ldots, f_n$. Further, theorem 5.2 in \cite{buss} shows that $f_1, \ldots, f_n$ are refutable if and only if there are no 0--1 solutions to $f_0 = \cdots = f_m = 0$. From this the motivation of the polynomial calculus becomes clear: a set of ordinary propositional logic formulae can be converted into a set of polynomials whose common zeros correspond to satisfying assignments of the formula. Thus, a refutation of such a set of polynomials amounts to a proof of unsatisfiablity of the set of formulae.


\section{The pigeonhole principle}
The pigeonhole principle is a simple idea that is commonly used in mathematical reasoning which also lends itself to reasoning about proof systems. Figuratively speaking it says that if $m$ pigeons occupy $n$ pigeonholes and $m > n$ then at least two pigeons need to share one hole. We will now take the steps necessary to formalize this.

\begin{definition}
    Let $T_n$ be the set of \textit{multilinear terms} of variables $x_1, \ldots, x_n$, i.e.\ $t = x_{i_1} \cdots x_{i_d}$ with $1 \leq i_1 < \cdots < i_d \leq n$. We say that $\deg(t) = d$ is the \textit{degree} of $t$. The terms of some maximal degree $d$ are $T_{n, d} \coloneqq \{t \in T_n \mid \deg(t) \leq d\}$.
\end{definition}

There are two orders of $T_n$ that are of interest to us, $\subseteq$ and $\preceq$. The former is simply the usual subset relation when viewing terms as the sets of variables occurring within them. The latter is the total degree lexicographic ordering, i.e., for some fixed arbitrary order of variables $x_1 < \cdots < x_n$ any terms $t_1, t_2 \in T_n$ with different degrees $\deg(t_1) < \deg(t_2)$ have $t_1 < t_2$ and otherwise $t_1 < t_2$ if $t_1$ occurs before $t_2$ using the usual lexicographic ordering.

\begin{definition}
    Let $\Sn$ be the \KK-algebra $\Sn = \KK[x_1, \ldots, x_n] / \{(x_i^2 - x_i) \mid i \in [n] \}\KK[x_1, \ldots, x_n]$, i.e.\ the ring of multilinear polynomials with $n$ indeterminates over some fixed field \KK.
\end{definition}
Polynomials in $\Sn$ have a unique representation as linear combinations of terms in $T_n$, so $\Sn \cong \KK T_n$.
\begin{definition}
    The \textit{leading term} $\LT$ of a polynomial is the largest (w.r.t.\ $\prec$) term of its representation as a linear combination over $T_n$. The \textit{degree} of it is $\deg(f) = \deg(\LT(f))$. The set of polynomials with degree at most $d$ is $\Snd$. Note $\Snd \cong \KK T_{n, d}$.
\end{definition}
The \textit{degree} of a polynomial calculus proof is the largest degree of a polynomial occurring within it.

With this, we can now formalize the pigeonhole principle, stating that $m$ pigeons can not be placed in $n$ holes, as a system of polynomial equations:
\begin{definition}[\PHP]
    The set of polynomials in $S_{nm}(\KK)$ over variables $x_{ij}$ with $i \in [m]$ and $j \in [n]$ denoted by \PHP is:
    \begin{align}
        Q_i &\coloneqq 1 - \sum_{j \in [n]} x_{ij} &&\text{for each $i \in [m]$}\\
        \Qiij &\coloneqq x_{i_1j} x_{i_2j} &&\text{for each $i_1 \neq i_2 \in [m], j \in [n]$}
    \end{align}
\end{definition}
Intuitively, $Q_i = 0$ expresses that pigeon $i$ is in precisely one hole $j$, and $\Qiij = 0$ says that two different pigeons can not occupy the same hole. We can immediately see that $\PHP$ is refutable if $m > n$ since the corresponding system of equations is unsatisfiable.


The proof makes heavy use of three families of polynomials, terms, and linear operators, denoted by $V$, $\Delta$, and $R$ respectively, each indexed appropriately. These are derived from:
\begin{definition}
    Define $V_{n, d}(f_1, \ldots f_m)$ to be the set of all polynomials in $\Snd$ provable from $f_1, \ldots, f_m$ with a proof of degree at most $d$. We say that a term $t \in T_{n, d}$ is \textit{reducible} if $t = \LT(f)$ for some $f \in V_{n, d}(f_1, \ldots f_m)$. Further define $\Delta_{n, d}(f_1, \ldots f_m) \subseteq T_{n, d}$ to be the set of irreducible terms. And finally, let $R_{n, d, f_1, \ldots f_m}$ be the linear operator taking any $f \in \Snd$ to some $f' \in \Delta_{n, d}(f_1, \ldots f_m)$ such that $f - f' \in V_{n, d}(f_1, \ldots f_m)$.
\end{definition}
This reduction process $R_{n, d, f_1, \ldots f_m}$ is the same as the one in the construction of Gröbner bases, though that algorithm is not relevant to us. What is important is that $\Delta_{n, d}(f_1, \ldots f_m)$ are linearly independent modulo $V_{n, d}(f_1, \ldots f_m)$ and that $\Snd$ can be written as the direct sum $\KK \Delta_{n, d}(f_1, \ldots f_m) \oplus V_{n, d}(f_1, \ldots f_m)$ with $R_{n, d, f_1, \ldots f_m}$ being the projection of $\Snd$ onto $\KK \Delta_{n, d}(f_1, \ldots f_m)$.

Of particular importance to us are the versions of these objects applied to the pigeonhole principle: $\Delta_d \coloneqq \Delta_{mn, d}(\PHP)$, $V_d \coloneqq V_{mn, d}(\PHP)$, and $R_d \coloneqq R_{mn, d, \PHP}$.

We will mainly concern ourselves with variables that correspond to a subset of pigeons $I \subseteq [m]$, denoted by $X_I \coloneqq \{x_{ij} \mid i \in I, j \in [n]\}$. Let $T_I$ be the terms over variables in $X_I$ and extend these linearly to $S_I(\KK)$. Similarly define $T_{I, d}$ and $S_{I, d}(\KK)$ to be such terms and polynomials of degree at most $d$. Also, let $\dom(f) \coloneqq \{i \in [m] \mid x_{ij} \in f \text{ for some } j \in [n]\}$ be the set of pigeons that occur in $f$. Finally, let $M_I$ be the set of all assignments to variables in $X_I$ that correspond to injective total functions $I \to [n]$, i.e.\ assignments that for each $i \in I$ set precisely one $x_{ij}$ to $1$ (and all others to $0$) and for each $j \in [n]$ set only one $x_{ij}$ to $1$.


\section{A lower bound for polynomial calculus refutations of \texorpdfstring{\PHP}{PHP}}
We now have the language needed to discuss the main result:
\begin{theorem} \label{main}
    For any $m > n$, every polynomial calculus refutation of \PHP must have degree at least $n/2 + 1$.
\end{theorem}
By definition, such a refutation of degree $d$ exists if and only if $1 \in V_d$, which then implies $V_d = \Snd$ and thus $R_d = 0$. The goal of the proof is to disprove this by showing $R_d \neq 0$. The strategy we use is to first define $\Rsem_d$, which we claim is identical to $R_d$ and clearly has $\Rsem_d \neq 0$. To then we verify that $\Rsem_d$ is in fact the same operator as $R_d$ we need to further change our perspective by splitting it into operators $\Rsem_I$, which each act similar to $\Rsem_d$ but only on polynomials using variables in $X_I$.\\
The biggest challenge is to then show that each $\Rsem_I$ behaves as needed, in particular that they all agree with each other at the intersections of their domains. We achieve this by again providing a different definition which clearly has the needed property and then showing that the two operators equal each other.

\subsection{Valid pigeon arrangements}
The idea behind the definition of $\Rsem_d$ comes from the indented semantics of the polynomials we use, i.e., from the variables encoding which hole each pigeon occupies. So the goal is for it to capture injectivity of the functions $\dom(f) \to [m]$ induced by $f$.\\
Formally, let $I \subseteq [m]$ with $|I| \leq n$ be some subset of pigeons that can be properly placed into holes $[m]$. Then $M_I$ as defined above is the set of all such possible arrangements. We define $V_I$ to be the ideal in $S_I(\KK)$ that is identically zero on all assignments in $M_I$. We can now define $\Dsem_I \coloneqq \Delta_{|I| \cdot n, |I| \cdot n}(V_I)$ and $\Rsem_I \coloneqq R_{|I| \cdot n, |I| \cdot n, V_I}$. That is, $\Dsem_I$ is all terms in $T_I$ that do not occur as a leading term of any polynomial that is identically zero on assignments in $M_I$. And $\Rsem_I$ is the projection of $S_I(\KK)$ onto these, which is exactly the common Gröbner reduction process.\\
In order to obtain such a semantic description of $R_d$, we now join all $\Dsem_I$ and $\Rsem_I$ together. So $\Dsem_d \coloneqq \cup_{|I| \leq d} \Dsem_I$ and define $\Rsem_d(t) \coloneqq \Rsem_{\dom(t)}(t)$ for $t \in T_d$ and extend it to $S_d(\KK)$ by linearity.

Our goal now is to show that this $\Rsem_d$ is equal to $R_d$ and that its image is nonzero. The latter is easily done:
\begin{lemma}
    $\Rsem_d \neq 0$.
\end{lemma}
\begin{proof}
    Let $I \subseteq [m]$ with $|I| \leq n$ and $f \in V_I$. Then $f + 1$ is identically 1 on $M_I$, so $f + 1 \not\in V_I$. By construction $S_I(\KK) = \KK \Dsem_I \oplus V_I$ and $\Rsem_I$ is the projection onto the first component, so $\Rsem_d(f + 1) = \Rsem_I(f + 1) \neq 0$.
\end{proof}

In order to prove $\Rsem_d = R_d$, we provide a characterization of $R_{n, d, f_1, \ldots, f_m}$ as a linear operator on $\Snd$:
\begin{theorem} \label{charR}
    Let $f_1, \ldots, f_m \in \Snd$ and $R: \Snd \to \Snd$ be a linear operator.

    \begin{enumerate}
        \item If
            \begin{align}
                R(f_i) &= 0 &&\fa i \in [m], \label{p34}\\
                \deg(R(f)) &\leq \deg(f) &&\fa f \in \Snd, \label{p35}\\
                R(f \cdot x_i) &= R(R(f) \cdot x_i) &&\fa f \in S_{n, d-1}(\KK), i \in [n] \label{p36}
            \end{align}
            then
            \begin{equation*}
                V_{n, d}(f_1, \ldots, f_m) \subseteq \Ker(R).
            \end{equation*}
        \item If additionally
            \begin{equation}
                f - R(f) \in V_{n, d}(f_1, \ldots, f_m) \fa f \in \Snd \label{p37}
            \end{equation}
            then
            \begin{equation}
                V_{n, d}(f_1, \ldots, f_m) = \Ker(R). \label{p38}
            \end{equation}
        \item If \eqref{p38} holds, $\Ima(R) = \KK\Delta$ for some $\Delta \subseteq T_{n, d}$, $R$ is a projection onto $\Delta$, i.e.,
        \begin{equation}
            R(f) = f \fa f \in \KK \Delta, \label{p39}
        \end{equation}
        and it also satisfies
        \begin{equation}
            \LT(R(f)) \preceq \LT(f) \fa f \in \Snd, \label{p310}
        \end{equation}
        then $\Delta = \Delta_{n, d}(f_1, \ldots, f_m)$ and $R = R_{n, d}(f_1, \ldots, f_m)$.
    \end{enumerate}
\end{theorem}
\begin{proof}
    See \cite{raz} lemma 3.2.
\end{proof}
Of this characterization part 3 is the most important. We can use it here to show $\Rsem_d = R_d$ and we will use it again later to show $\Rsem_I = \Rsyn_I$. But in order to use it we first need to show \eqref{p38}, which is easiest to do by proving \eqref{p34} through \eqref{p37}.

Properties \eqref{p35}, \eqref{p37}, \eqref{p39}, and \eqref{p310} follow directly from the construction of $\Rsem_d$ (a more complete explanation can be found in \cite{raz}). Property \eqref{p34} holds since all $Q \in \PHP$ are identically zero on $M_{\dom(Q)}$ and thus are in $V_{\dom(Q)}$, so $\Rsem_d(Q) = \Rsem_{\dom(Q)}(Q) = 0$. We show \eqref{p36} for terms $t \in T_d$, the proof extends to all $f \in S_d(\KK)$ by linearity. First rearrange:
\begin{align*}
    &\Rsem_d(t \cdot x_{ij}) = \Rsem_d(\Rsem_d(t) \cdot x_{ij})\\
    \Leftrightarrow \quad &\Rsem_d(t \cdot x_{ij}) - \Rsem_d(\Rsem_d(t) \cdot x_{ij}) = 0\\
    \Leftrightarrow \quad &\Rsem_d((t \cdot x_{ij}) - (\Rsem_d(t) \cdot x_{ij})) = 0\\
    \Leftrightarrow \quad &\Rsem_d((t - \Rsem_d(t)) \cdot x_{ij}) = 0.
\end{align*}
Observe that if $i \in \dom(t)$, \eqref{p36} holds since $t - \Rsem_d(t) = t - \Rsem_{\dom(t)}(t) = f$ is some polynomial that is identically zero on $M_I$ by definition, so the same must be true for $f \cdot x_{ij}$ and thus $f \cdot x_{ij} \in V_d$ and $\Rsem_d(f \cdot x_{ij}) = 0$.\\
The difficulty in proving \eqref{p36} comes from showing that this still holds even if $i \not\in \dom(t)$. Specifically what we need is that all $\Rsem_I$ behave identically on their intersection, i.e., that for any $t \in T_d, I \subseteq [m]$ with $\dom(t) \subseteq I$
\begin{equation}
    \Rsem_I(t) = \Rsem_{\dom(t)}(t). \label{inteq}
\end{equation}
Then we can simply set $I = \dom(t) \cup \{x_{ij}\}$ in order to write
\begin{equation*}
    \Rsem_d((t - \Rsem_d(t)) \cdot x_{ij}) = \Rsem_I((t - \Rsem_{\dom(t)}(t)) \cdot x_{ij}) = \Rsem_I((t - \Rsem_I(t)) \cdot x_{ij})
\end{equation*}
and conclude similarly as above that this is $0$.

\subsection{The pigeon dance}
What we have seen so far is that if \eqref{inteq} holds, then $\Rsem_d = R_d$ and since $\Rsem_d \neq 0$ there ca not be a polynomial calculus refutation of \PHP with degree at most $d$. The strategy for proving that \eqref{inteq} holds if $d \leq n / 2 + 1$ is to describe $\Rsem_I$ through what is called the pigeon dance.

Given some partial assignment of pigeons to holes, the \textit{pigeon dance} is a process where, starting with the leftmost pigeon, each one flies to a free hole to its right. We say the dance is \textit{aborted} if any pigeon has no free hole to its right when it starts its flight, and \textit{completed} otherwise.\\
Formally, we define $\tilde T_I$ to be those elements of $T_I$ that correspond to partial injections $I \to [n]$, i.e.\ terms of the form $x_{i_1 j_1} \cdots x_{i_d j_d}$ where all $i$ and all $j$ are pairwise different. Then $\Dsyn_I$ is defined to be the set of all such $\tilde T_I$ that let the pigeons complete their dance. We can already see that $t \in \Dsyn_I$ does not depend on $I$ since the pigeons not occurring in $t$ play no role in the dance. Finally we define $\Rsyn_I(t)$ to be some polynomial $f \in \KK \Dsyn_I$ such that $\LT(f) \preceq t$ and $t - f \in V_I$.

\begin{theorem} \label{RsynDef}
    $\Rsyn_I(t)$ is well defined. That is, for every $t \in T_I$ there exists a $f \in \KK \Dsyn_I$ such that $\LT(f) \preceq t$ and $t - f \in V_I$.
\end{theorem}
\begin{proof}
    If $t \not\in \tilde T_I$ then let $f \coloneqq 0$. Trivially, $0 \preceq t$, and $t \in V_I$ since $t$ contains some $x_{i j_1}$ and $x_{x i j_2}$, one of which always is zero on all assignments in $M_I$, thus $t$ also is.\\
    If $t \in \Dsyn_I$, then let $f \coloneqq t$. Clearly, $t \preceq t$ and $t - f = 0 \in V_I$.\\
    If $t \in \tilde T \setminus \Dsyn_I$, write $t = x_{i_1 j_1} \cdots x_{i_d j_d}$ with $i_1 < \cdots < i_d$. Since $Q_{i_1} \in V_I$ we can use $Q_{i_1} = 0$ to derive equations modulo $V_I$:
    \begin{align*}
        t = \ &(x_{i_1 j_1} - 0) x_{i_2 j_2} \cdots x_{i_d j_d}\\
        = \ & \left(x_{i_1 j_1} - \sum_{j \in [n]} x_{i_1 j}\right) x_{i_2 j_2} \cdots x_{i_d j_d} \mod V_I\\
        = \ &x_{i_2 j_2} \cdots x_{i_d j_d} - \sum_{j' < j_1} x_{i_1 j'} x_{i_2 j_2} \cdots x_{i_d j_d}\\
        &- \sum_{j' > j_1} x_{i_1 j'} x_{i_2 j_2} \cdots x_{i_d j_d} \mod V_I.
    \end{align*}
    Any terms $x_{i_1 j'} x_{i_2 j_2} \cdots x_{i_d j_d}$ with $j' \in \{j_2, \ldots, j_d\}$ are equal to $0$ and thus can be removed from the polynomial. The terms in either of the first two summands are strictly smaller than $t$ (w.r.t.\ $\prec$) and thus can remain in the constructed polynomial. The remaining terms are larger than $t$, but we can iteratively apply the same construction to them, which again yields some $0$ terms, some smaller terms, and potentially some larger terms.\\
    To see that this will eventually remove all larger terms, notice that this construction is simulating the pigeon dance. At each step, the leftmost pigeon that has not moved yet moves to a different hole. The $0$ terms are potential moves that would lead to it flying to an already occupied hole. The ignored terms are ones where it would fly to the left. The larger terms are all the legal moves, where it flies to a previously unoccupied hole to its right. Since $t \not\in \Dsyn_I$ the pigeon dance gets aborted for any strategy of the pigeons, i.e., when continually expanding terms all will be cancelled out eventually.\\
    This lets us construct a polynomial $f' \in S_I(\KK)$ with $f' = t \mod V_I$ and $f' \prec t$. In order to obtain $f \in \KK \Dsyn_I$, we recursively apply this process to all terms in $f'$ not in $\Dsyn_I$. This eventually terminates since the newly constructed terms are always strictly smaller. And because $t = f \mod V_I$, we have $t - f \in V_I$.
\end{proof}
We can now extend $\Rsyn_I$ to $S_I(\KK)$ by linearity to obtain the final characterization of the reduction process.

The goal of this construction was to prove \eqref{inteq}, since we already know $\Rsyn_I = \Rsyn_{\dom(t)}$ we only need to verify $\Rsem_I = \Rsyn_I$. Because of $$\Rsem_I = R_{|I| \cdot n, |I| \cdot n, \{Q \in \PHP \mid \dom(Q) \subseteq I\}},$$ we can use part 3 of \autoref{charR} for this with $d = |I| \cdot n$ and
$$f_i \in \{Q \in \PHP \mid \dom(Q) \subseteq I\}.$$
By construction, $\Rsyn_I$ is a projection onto $\Dsyn_I$, we have $\Ima(\Rsyn_I) = \Dsyn_I$, $\LT(\Rsyn_I(f)) \preceq \LT(f)$, and $\Ker(\Rsyn_I) \subseteq V_I$. So the only property left to check is $\Ker(\Rsyn_I) \supseteq V_I$. Since $S_I(\KK) = \KK \Dsyn_I \oplus \Ker(\Rsyn_I)$ we can rephrase this as $\KK \Dsyn_I \cap V_I = \emptyset$, and further as $\Dsyn_I$ being linearly independent when viewed as functions $M_I \to \KK$.

To do this we need to define a new operator $\K: T_I \to \tilde T_I$ that represents removing the leftmost pigeon from its hole and moving the hole to the leftmost position. Formally, if $t \in \tilde T_I$ then $t = x_{i_1 j_1} \cdots x_{i_d j_d}$ with $i_1 < \cdots < i_d$ and $\K(t) = x_{i_2 j'_2} \cdots x_{i_d j'_d}$ with
$$
j'_k \coloneqq \begin{cases}
    j_k + 1, &\text{if } j_k < j_1\\
    j_k, &\text{if } j_k > j_1.
\end{cases}
$$
Otherwise we set $\K(t) = 0$.

\begin{theorem} \label{killdefn}
    For $t = x_{i_1 j_1} \cdots x_{i_d j_d} \in \tilde T_I$, $t \in \Dsyn_I$ if and only if there is a $j' > j_1$ such that $\K(x_{i_1 j'} x_{i_2 j_2} \cdots x_{i_d j_d}) \in \Dsyn_I$.
\end{theorem}
\begin{proof}
    By definition $t$ is in $\Dsyn_I$ if and only if there is an unoccupied hole $j'$ for pigeon $i_1$ to fly to such that the rest of the pigeons can complete the dance. After $i_1$'s flight the only effect it has on the dance is blocking hole $j'$. This results in the same configuration of available holes as removing $i_1$ and making hole $j'$ inaccessible to the others by moving it all the way to the left, which is precisely what $\K(x_{i_1 j'} x_{i_2 j_2} \cdots x_{i_d j_d})$ does.
\end{proof}

\begin{theorem} \label{closedsubset}
    $\Dsyn_I$ is closed downward w.r.t.\ $\subseteq$. That is, if $t \in \Dsyn_I$ and $t' \subseteq t$, then $t' \in \Dsyn_I$.
\end{theorem}
\begin{theorem} \label{closedkill}
    $\Dsyn_I$ is closed under $\K$. That is, if $t \in \Dsyn_I$ then $\K(t) \in \Dsyn_I$.
\end{theorem}
\begin{proof}
    A formal proof for both theorems can be found in \cite{raz}, claim 3.7. Intuitively, removing pigeons can only make it easier for the others to complete the dance since the missing ones won't be there to block any holes. So if pigeons $\dom(t)$ can successfully complete the dance, so can a subset of them. This still is true even if you remove a pigeon and also the hole it was occupying since any pigeon that wanted to fly to it can instead just fly to the hole the missing one would have flown to.
\end{proof}

\begin{theorem} \label{emptyhole}
    If $|I| \leq (n + 1) / 2$, $t \in \Dsyn_I$, and the minimal element $i$ of $I$ is not in $\dom(t)$, then there exists a $j \in [n]$ such that $\K(x_{i j} t) \in \Dsyn_I$.
\end{theorem}
\begin{proof}
    There are at most 
    $$|\dom(t)| \leq |I \setminus \{i\}| = |I| - 1 \leq \frac{n + 1}{2} - 1 = \frac{n - 1}{2}$$
    pigeons involved in the dance, and each will occupy $2$ holes. So the total number of holes is at most $n - 1$, meaning that there is at least one hole $j$ not used at all. $\K(x_{i j}t)$ results in the same arrangement of holes and pigeons as $t$ modulo the missing hole $j$. Since $j$ was not used during the successful dance the pigeons can perform the same dance for $\K(x_{i j}t)$ and successfully complete it.
\end{proof}

We finally are ready to put all the pieces together and prove the crucial missing link:
\begin{theorem}
    For $|I| \leq (n + 1) / 2$, terms in $\Dsyn_I$ are linearly independent as functions on $M_I$.
\end{theorem}
\begin{proof}
    By induction on $|I|$:\\
    \textbf{Base case}: If $|I| = 0$ then $\Dsyn_I = \emptyset$ and the claim vacuously holds.\\
    \textbf{Inductive step}: Let $i_1$ be the smallest element of $I$ and assume the claim has already been proved for $\Is$. Given some non-trivial linear combination of terms in $\Dsyn_I$ we can write it as:
    \begin{equation} \label{lincomp}
        \sum_{t \in \Gamma} t A_t
    \end{equation}
    with $\Gamma \subseteq \tilde T_\Is$ and $A_t \in \KK \tilde T_{\{i_1\}} \setminus \{0\}$. This works because each term $t$ in the linear combination contains at most one variable in $X_{\{i_1\}}$, so we can factor out common terms $t \in \tilde T_\Is$ and be left with a factor that is a non-zero affine polynomial with variables in $X_I$. By construction each $t \in \Gamma$ has $t \subseteq t'$ for some term $t'$ in the linear combination, so $\Gamma \subseteq \Dsyn_\Is$ by \autoref{closedsubset}. Let $t_1$ be the largest term in $\Gamma$ (w.r.t.\ $\preceq$), and
    $$A_{t_1} = \alpha_0 + \sum_{j \in [n]} \alpha_j x_{i_1 j}.$$
    Finally, define $\rhoij$ to be the restriction that sends $x_{i_1 j_1}$ to $1$ and all other $x_{i j}$ with $i = i_1$ or $j = j_1$ to $0$. Note that the effect of $\rhoij$ on $\tilde T_\Is$ is the effectively the same as that of $t \mapsto \K(x_{i_1 j_1} t)$, intuitively they both prevent hole $j$ from being used by the pigeons.
    
    Our goal now is to find a $j_1$ such that $\rhoij(A_t) \neq 0$ and $\K(x_{i_1 j_1} t) \in \Dsyn_I$. We distinguish two cases:\\
    $\mathbf{\alpha_0 = 0}$:\\
    Since $A_t$ is non-zero there is some summand with $\alpha_j \neq 0$, choose $j_1$ to be one of them. Because $\alpha_{j_1} \xij t_1$ is a term in \eqref{lincomp}, we have $\xij t_1 \in \Dsyn_I$ and thus $\K(\xij t_1) \in \Dsyn_\Is$ by \autoref{closedkill}. Clearly, $\rhoij(A_t) = \alpha_{j_1} \neq 0$ since all other summands are $0$.\\
    $\mathbf{\alpha_0 \neq 0}$:\\
    By \autoref{emptyhole} there are $j$'s satisfying $\K(x_{i_1 j_1} t) \in \Dsyn_I$, let $j_1$ be the largest of them. Then $\xij t_1 \not\in \Dsyn_I$ by \autoref{killdefn} and thus $\xij t_1$ can not be in \eqref{lincomp}. So $\alpha_{j_1} = 0$ and thus $\rhoij(A_t) = \alpha_0 \neq 0$.

    If we now apply $\rhoij$ to \eqref{lincomp} we obtain
    \begin{align*}
        \rhoij\left(\sum_{t \in \Gamma} t A_t\right) &= \rhoij(t_1 A_{t_1}) + \rhoij\left(\sum_{t \in \Gamma \setminus \{t_1\}} t A_t\right)\\
        &= \alpha \cdot \rhoij(t_1) + f.
    \end{align*}
    By definition $\rhoij(t_1) \in \Dsyn_\Is$, so $g = \alpha \cdot \rhoij(t_1) + \Rsyn_\Is(f)$ is a linear combination from $\Dsyn_\Is$. It is non-trivial because $\LT(\Rsyn_\Is(f)) \prec t_1$, by construction and \autoref{RsynDef}. By the inductive assumption there exists some assignment $a \in M_\Is$ evaluating $g$ to some $k \in \KK$. We extend this to $a'$ by setting $a(\xij) \coloneqq 1$ and $a(x_{i j}) \coloneqq 0$ for all other $x_{i j}$ with $i = i_1$ or $j = j_1$.\\
    We have $a(f) = a(\Rsyn_\Is(f))$ since $f = \Rsyn_\Is(f) \mod V_I$ by \autoref{RsynDef} and all $h \in V_I$ have $a(h) = 0$ by definition. So $a'(g) = k$ and thus $a'$ also evaluates \eqref{lincomp} to $k \neq 0$.
\end{proof}

With $|I| = d \leq (n + 1) / 2$ this tells us that $\Ker(\Rsyn_I) = V_I$ and thus $\Rsyn_I = \Rsem_I$ holds. So we observe that $\Rsyn_I(t)$ is independent of $I$ (as long as $\dom(t) \subseteq I$) since pigeons not participating in the dance do not affect its success. This in turn implies that $\Rsem_d$ satisfies all properties \eqref{p34} through \eqref{p310} and thus $\Rsem_d = R_{nm, d, \PHP}$. Since $\Rsem_d \neq 0$, the same is true for $R_{nm, d, \PHP}$, which means that $V_{nm, d, \PHP} \neq S_{nm, d}(\KK)$. This implies $1 \not\in V_{nm, d}(\KK)$ and thus \autoref{main}.

\newpage
\printbibliography
\end{document}