\documentclass[11pt]{article}
\usepackage[T1]{fontenc}
\usepackage[margin=1in]{geometry}
\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage{microtype}
\usepackage[hidelinks]{hyperref}
\hypersetup{pdftitle={A Three-Polynomial Counterexample to the Generalized Effective Hypercube Nullstellensatz},pdfauthor={Yuran Xiu},pdfkeywords={Hypercube Nullstellensatz, Boolean cube, certificate degree, multilinearization, polynomial certificates, proof complexity}}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{remark}[theorem]{Remark}
\newcommand{\R}{\mathbb R}
\newcommand{\red}[1]{\overline{#1}}
\newcommand{\code}[1]{\texttt{\small\detokenize{#1}}}
\title{A Three-Polynomial Counterexample to the\\Generalized Effective Hypercube Nullstellensatz}
\author{Yuran Xiu\\IIIS, Tsinghua University\\\texttt{xiuyr23@mails.tsinghua.edu.cn}}
\date{15 October 2026}
\begin{document}
\maketitle
\begin{abstract}
We give a counterexample to the proposed extension of the effective
Hypercube Nullstellensatz from two polynomials to an arbitrary fixed number
of polynomials. For every $n\geq1$, we construct three real polynomials
in $2n+1$ variables, of degrees $2,2,1$, respectively. Each is nonzero as
a function on the Boolean cube, their product vanishes on the cube, and
they have no common Boolean zero. Nevertheless, every polynomial
certificate $\sum_{i=1}^3 h_i g_i=1$ on the cube satisfies
$\deg\red{h_1g_1}\geq n+1$, where the bar denotes multilinearization.
The construction applies a fresh selector variable to the hard pair of
Kothari, Kovacs-Deak, Wang, and Yang. Thus its new ingredient is a short
transfer of their existing degree obstruction to the product-zero setting.
The full unbounded-degree counterexample has been formalized and checked
in Lean~4.
\end{abstract}

\section{Introduction}

Let $g_1,\ldots,g_m$ be real polynomials with no common zero on the
Boolean cube $\{0,1\}^N$. There are polynomial multipliers
$h_1,\ldots,h_m$ such that
\begin{equation}\label{eq:certificate}
 \sum_{i=1}^m h_i(x)g_i(x)=1\qquad(x\in\{0,1\}^N).
\end{equation}
Indeed, at each point one may choose a nonzero $g_i(x)$, assign its
multiplier the reciprocal value and all other multipliers zero, and
interpolate these functions on the finite cube. The effective question is
whether such a certificate can be chosen with low degree.

For a polynomial $p$, write $\red p$ for its unique multilinear
representative modulo the relations $X_j^2=X_j$. We consider the
degrees of the \emph{separate reduced products} $\red{h_i g_i}$.
These are distinct from the unreduced product degrees and from the
degree of the sum in~\eqref{eq:certificate}.

Kothari, Kovacs-Deak, Wang, and Yang proved an effective theorem for two
generators under the additional hypothesis that their product vanishes
on the cube~\cite[Theorem~10]{KKWY26}. They proposed that, for every
fixed $m\geq2$, the same hypotheses should give a bound on
$\max_i\deg\red{h_i g_i}$ polynomial in the input degrees
\cite[Conjecture~1]{KKWY26}. We disprove this extension already for
$m=3$, with a fixed tuple of input degrees.

\begin{theorem}\label{thm:main}
For $n\geq1$, use variables $t,X_1,\ldots,X_n,Y_1,\ldots,Y_n$ and set
\begin{align}
 A(X)&=\sum_{j=1}^n X_j,&
 B(X,Y)&=\sum_{j=1}^n X_j+\sum_{j=1}^n Y_j-(n+1),\label{eq:pair}\\
 g_1&=tA,&g_2&=tB,&g_3&=1-t.\label{eq:generators}
\end{align}
The ordinary degrees of $g_1,g_2,g_3$ are $2,2,1$. Each is nonzero
on the Boolean cube. Their product vanishes on the cube, and they have
no common Boolean zero. For all real polynomial multipliers $h_1,h_2,h_3$,
the identity~\eqref{eq:certificate} on $\{0,1\}^{2n+1}$ implies
\begin{equation}\label{eq:lower}
 \deg\red{h_1g_1}\geq n+1.
\end{equation}
\end{theorem}

\begin{corollary}\label{cor:unbounded}
There is no finite real-valued bound depending only on
$(\deg g_1,\deg g_2,\deg g_3)$ for the maximum reduced-product degree
of a certificate, even when the three generators are nonzero as Boolean
functions, have no common Boolean zero, and have product identically
zero on the cube. In particular, Conjecture~1 of~\cite{KKWY26} is false.
\end{corollary}

\paragraph{Attribution and scope.}
The pair $A,B$ in~\eqref{eq:pair} and its degree obstruction are exactly
the example in~\cite[Fact~7]{KKWY26}. Their argument shows why removing
the product-zero hypothesis fails for two generators. We use that
existing example and its symmetrization proof. The observation here is
that adjoining a selector $t$ and the third generator $1-t$ imposes the
product-zero hypothesis while preserving the obstruction on the face
$t=1$. This is a negative-answer note about the stated multigenerator
conjecture. It does not contradict the two-generator theorem or the main
rational-degree theorem of~\cite{KKWY26}.

\section{Multilinearization and the known hard pair}

A multilinear polynomial in $N$ variables has the form
$\sum_{S\subseteq[N]}c_S\prod_{j\in S}X_j$. Replacing every positive
exponent in a monomial by one and then collecting coefficients gives
$\red p$. It agrees with $p$ on $\{0,1\}^N$ and cannot have larger
total degree. Uniqueness follows by induction on $N$: write a multilinear
polynomial as $P_0+X_NP_1$ and evaluate first at $X_N=0$ and then at
$X_N=1$. A polynomial vanishing on the entire cube is therefore zero
if it is multilinear. We use this observation also on coordinate faces.

The following form of the hard-pair obstruction is the claim proved in
\cite[proof of Fact~7]{KKWY26}. We give the proof to make the transfer
self-contained.

\begin{lemma}[Hard-pair obstruction]\label{lem:hardpair}
Suppose a real multilinear polynomial $R(X,Y)$ satisfies
\begin{align}
 R(0,y)&=0 &&(y\in\{0,1\}^n),\label{eq:zero-face}\\
 R(x,y)&=1 &&(x,y\in\{0,1\}^n,\ |x|+|y|=n+1).\label{eq:one-line}
\end{align}
Then $\deg R\geq n$.
\end{lemma}

\begin{proof}
Suppose, to the contrary, that $d:=\deg R<n$. Average $R$ independently
over permutations of its $X$ coordinates and of its $Y$ coordinates.
The value of this average on a Boolean input of weights $(u,v)$ is given
by a bivariate polynomial $S(U,V)$ of total degree at most $d$.
Here is a direct construction. For a multilinear monomial using $a$
distinct $X$ coordinates and $b$ distinct $Y$ coordinates, its average
at weights $(u,v)$ is
\begin{equation}\label{eq:average}
 \frac{\binom{u}{a}}{\binom{n}{a}}
 \frac{\binom{v}{b}}{\binom{n}{b}}.
\end{equation}
This is the probability that a uniformly chosen set of $u$ positions
contains the prescribed $a$ positions, times the analogous probability
for the other block. Interpret $\binom{U}{a}$ as the falling-factorial
polynomial $U(U-1)\cdots(U-a+1)/a!$, with $\binom{U}{0}=1$.
The denominators in~\eqref{eq:average} are positive because $a,b\leq n$.
Expanding $R$ by monomials and replacing each monomial by this polynomial
defines $S$. Each contributing term has degree $a+b\leq d$.

Both boundary conditions are constant on the relevant weight layers,
so averaging preserves them. In particular,
\[
 S(0,v)=0\quad(0\leq v\leq n),\qquad
 S(u,n+1-u)=1\quad(1\leq u\leq n).
\]
The univariate polynomial $S(0,V)$ has degree at most $d<n$ and has
$n+1$ distinct zeros. Thus it is identically zero. Also
\[
 H(U):=S(U,n+1-U)-1
\]
has degree at most $d<n$ and vanishes at $1,\ldots,n$. It too must be
identically zero. But $H(0)=S(0,n+1)-1=-1$, a contradiction.
\end{proof}

The argument applies to arbitrary real coefficients. Neither symmetry
of $R$ nor any sign restriction is assumed; symmetrization is used only
inside the proof.

\section{The selector transfer}

\begin{proof}[Proof of Theorem~\ref{thm:main}]
Since $n\geq1$, both $tA$ and $tB$ have nonzero degree-two monomials,
and $1-t$ has degree one. These generators are also nonzero as functions
on the cube: for $g_1$ take $t=1$, $X_1=1$ and the remaining coordinates
zero; for $g_2$ take $t=1$ and $X=Y=0$; for $g_3$ take $t=0$.
Their product has a factor $t^2(1-t)$, which vanishes at both Boolean
values of $t$.

There is no common zero. If $t=0$, then $g_3=1$. If $t=1$ and $g_1=0$,
all the Boolean $X$ coordinates are zero. In that case
$B=|Y|-(n+1)\leq-1$, so $g_2\ne0$.

Now take any certificate~\eqref{eq:certificate} and put
$P=\red{h_1g_1}$. Since $g_1$ vanishes on the face $t=0$,
$P(0,x,y)=0$ for every Boolean $(x,y)$. Write the multilinear polynomial
$P$ uniquely as
\[
 P(t,X,Y)=P_0(X,Y)+tR(X,Y).
\]
Multilinear uniqueness on the face implies $P_0=0$. Hence $P=tR$.

On $t=1$ and $X=0$, the first generator is zero, so
$R(0,y)=P(1,0,y)=0$. On $t=1$ and $|X|+|Y|=n+1$, the second and
third generators are zero. The certificate then forces
$R(x,y)=P(1,x,y)=1$. Thus $R$ satisfies the two conditions of
Lemma~\ref{lem:hardpair}, and $\deg R\geq n$.

In particular $R\ne0$; the second condition has witnesses for every
$n\geq1$, for example $|X|=n$ and $|Y|=1$. Since $t$ is a fresh
variable, multiplication by $t$ increases every nonzero monomial degree
by one and causes no cancellation. Therefore
\[
 \deg\red{h_1g_1}=\deg(tR)=1+\deg R\geq n+1.
\]
\end{proof}

\begin{proof}[Proof of Corollary~\ref{cor:unbounded}]
Let $F$ be any proposed real-valued function of the three input degrees.
Choose an integer $n\geq1$ with $n+1>F(2,2,1)$. The generators of
Theorem~\ref{thm:main} satisfy all the hypotheses, but every certificate
has a reduced product of degree greater than $F(2,2,1)$. This excludes
every such function $F$, and hence every polynomial bound.
\end{proof}

\begin{remark}
For more than two generators, requiring the product to vanish means that
at least one generator vanishes at each point. It does not require at
most one generator to be nonzero. On the face $t=1$, the third generator
vanishes identically while the first two retain the original hard pair.
This distinction is what permits the transfer. The individual nonzero
Boolean-function witnesses above ensure that the construction does not
rely on adding a generator that vanishes everywhere on the cube.
\end{remark}

\section{Formal verification}

The associated Lean development proves the all-$n$ lower bound and its
dimension-independent consequence. Its multilinearization operator
replaces positive monomial exponents by one and collects coefficients;
the equality of Boolean evaluations, uniqueness, and degree properties
are proved. The multipliers range over all real multivariate polynomials.
There are no symmetry, coefficient-sign, or multiplier-degree restrictions.

The principal declarations are in namespace \code{HypercubeNS}:
\begin{itemize}
\item \code{selector_certificate_degree} proves
Theorem~\ref{thm:main}'s certificate lower bound for every $n\geq1$.
\item \code{unbounded_certificate_degree} gives a triple in an ordinary
finite indexed variable space exceeding every prescribed natural degree
threshold. The formal proof includes the variable-renaming equivalence.
\item \code{no_dimension_independent_bound} proves
Corollary~\ref{cor:unbounded}, for every real-valued function of the
three input degrees.
\end{itemize}
The generator hypotheses and exact degrees are proved separately and
included in the final counterexample. The hard-pair lemma is proved
from layer counting and univariate root bounds, rather than introduced
as an axiom. The development does not assert a matching upper certificate
degree or a general theorem about exact selector degree shifts.

Verification used Lean~4.27.0 and mathlib commit
\begin{center}\code{a3a10db0e9d66acbebf76c5e6a135066525ac900}.\end{center}
A separate reproduction rebuilt all twelve local modules, including the
aggregate statement and axiom audit, from saved sources. The associated
records preserve the dependency manifest, source hashes, successful build
logs, and transitive axiom reports. From the formal artifact's root,
\code{sh lean/verify.sh} performs the local-source rebuild; the saved
helper paths must be configured for the pinned compiler and dependency
cache on another machine. The accepted main declarations depend only on
\code{propext}, \code{Classical.choice}, and \code{Quot.sound}.
No admitted lemma, additional mathematical axiom, native decision
procedure, or unchecked numerical certificate is used. The reproduction
reused the pinned compiler and dependency caches; it did not rebuild
Lean or all of mathlib. The checked statements concern the counterexample
and do not constitute a formal audit of the entire cited paper.

\begin{thebibliography}{9}
\bibitem{KKWY26}
Robin Kothari, Matt Kovacs-Deak, Daochen Wang, and Rain Zimin Yang.
\newblock Rational degree is polynomially related to degree.
\newblock \href{https://arxiv.org/abs/2601.08727v3}{arXiv:2601.08727v3},
28 September 2026. Section~5.1, Theorem~10, Conjecture~1, and Fact~7.
\end{thebibliography}
\end{document}