\documentclass[11pt]{article}
\usepackage[T1]{fontenc}
\usepackage[margin=1in]{geometry}
\usepackage{amsmath,amssymb,amsthm,mathtools,booktabs,microtype}
\usepackage{xurl}
\usepackage[colorlinks=true,allcolors=blue!50!black]{hyperref}
\setlength{\emergencystretch}{2em}
\usepackage{xcolor}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\theoremstyle{remark}\newtheorem{remark}[theorem]{Remark}
\newcommand{\R}{\mathbb R}\newcommand{\Z}{\mathbb Z}
\newcommand{\lean}[1]{{\small\path{#1}}}
\title{An Arbor Polytope with Nonreal Ehrhart Roots}
\author{Yuran Xiu\\IIIS, Tsinghua University\\
\texttt{xiuyr23@mails.tsinghua.edu.cn}}
\hypersetup{pdfauthor={Yuran Xiu}}
\date{14 October 2026}
\begin{document}
\maketitle
\begin{abstract}
We construct a singleton-labeled arbor on 243 vertices whose Ehrhart
polynomial has a nonreal root. This disproves the conjecture that the
Ehrhart roots of every arbor polytope are real and lie in $[-1,0]$.
The polynomial factors as $(m+1)^{230}(7m+2)^8 f(m)/6144$, where $f$ is
an explicit quintic. We derive this identity by counting lattice points
for every nonnegative integer dilation, using three moments of subtree
deficits. A negative value of $f'^2-ff''$ at $-3/10$ gives an exact
nonreal-root certificate. The lattice-count identity and the resulting
counterexample have been formalized and checked in Lean.
\end{abstract}

\section{Introduction and the counterexample}
Chapoton introduced polytopes associated with arbors, rooted trees whose
vertices carry disjoint nonempty sets of labels~\cite{Chapoton}.
The real-rootedness conjecture for their Ehrhart polynomials is also
stated as Conjecture~1.2 by Athanasiadis and Chapoton~\cite{AC}.
We disprove it within the subclass in which each vertex has one label.

For a rooted tree $T$, write $T_v$ for the set consisting of $v$ and all
its descendants. The singleton-labeled arbor polytope is
\begin{equation}\label{eq:polytope}
 Q_T=\left\{x\in\R_{\geq0}^{V(T)}:
       \sum_{u\in T_v}x_u\leq |T_v|\quad(v\in V(T))\right\}.
\end{equation}
This is a lattice polytope~\cite{Chapoton}. Its Ehrhart polynomial $E_T$
is characterized by
$E_T(m)=|mQ_T\cap\Z^{V(T)}|$ for every integer $m\geq0$.
The tree used here is described without any implicit identifications:
its root $a$ has one child $b$, and $b$ has eleven children. One of these
children is the center of a star with 180 leaves; each of the other ten
is the center of a star with five leaves. Every vertex receives a distinct
singleton label. Thus $T$ has $2+181+10\cdot6=243$ vertices and 230 leaves.

\begin{theorem}\label{thm:main}
For this tree $T$,
\begin{equation}\label{eq:E}
 E_T(m)=\frac{(m+1)^{230}(7m+2)^8}{6144}\,f(m),
\end{equation}
where
\begin{equation}\label{eq:f}
\begin{split}
 f(m)={}&24+5852m+400056m^2+8533751m^3\\
        &\quad+44368122m^4+67184474m^5.
\end{split}
\end{equation}
The polynomial $f$, and hence $E_T$, has a nonreal complex root.
\end{theorem}

The theorem concerns the Ehrhart polynomial itself. It makes no claim
about the real-rootedness of the $h^*$-polynomial and no minimality claim
for the dimension 243. Nonreal Ehrhart roots for general lattice
polytopes were already known. For example, Higashitani~\cite{Higashitani}
constructed counterexamples to a conjectured strip bound on the real
parts of Ehrhart roots. The issue here is the more restrictive arbor
family and its proposed real-rootedness property.

\section{Lattice points and subtree deficits}
Fix an integer $m\geq0$. For a lattice point in a subtree with $N$
vertices, define its \emph{deficit} to be $mN$ minus the sum of its
coordinates. This is a nonnegative integer by the subtree constraint.
For a finite collection of configurations with deficits $d$, let
$M_0$ denote its cardinality and, for $r\geq1$, let $M_r=\sum d^r$.
For disjoint subtrees the configurations are independent and deficits add.

\begin{lemma}\label{lem:root}
Suppose the configurations in all child subtrees of a new singleton
root have total deficit $s$. There is exactly one choice of the root
coordinate for each new deficit $d\in\{0,\ldots,m+s\}$.
\end{lemma}
\begin{proof}
The root coordinate is $m+s-d$. Its nonnegativity and the new subtree
inequality are equivalent to $0\leq d\leq m+s$. The child inequalities
are unchanged, so this correspondence is a bijection.
\end{proof}

A leaf has deficits $0,\ldots,m$. Put $h=m+1$. Dividing its first three
raw moments by $h$ gives
\begin{equation}\label{eq:leaf}
 \mu_1=\frac m2,\qquad
 \mu_2=\frac{m(2m+1)}6,\qquad
 \mu_3=\frac{m^2(m+1)}4.
\end{equation}
These follow from the sums of the first three powers. If $S$ is the sum
of $k$ leaf deficits, its moments divided by the number $h^k$ of leaf
configurations are
\begin{align}
 s_1&=k\mu_1,\nonumber\\
 s_2&=k\mu_2+k(k-1)\mu_1^2,\label{eq:leafsum}\\
 s_3&=k\mu_3+3k(k-1)\mu_1\mu_2
          +k(k-1)(k-2)\mu_1^3.\nonumber
\end{align}
Indeed, expand $S^r$ and separate tuples of indices according to their
equalities. The formulas include $k=0,1,2$ with the vanishing factors
interpreted in the usual way.

Let $\operatorname{Star}(k)$ consist of a singleton root and $k$ singleton
leaves. Denote its cardinality, first deficit moment, and second deficit
moment divided by $h^k$ by $P_k,D_k,W_k$, respectively.
\begin{lemma}\label{lem:star}
For every $m\geq0$ and $k\geq0$,
\begin{align}
 P_k&=h+s_1=1+\frac{k+2}{2}m,\label{eq:P}\\
 D_k&=\frac{m(m+1)+(2m+1)s_1+s_2}{2},\label{eq:D}\\
 W_k&=\frac{1}{6}\bigl(2m^3+3m^2+m+(6m^2+6m+1)s_1
                    \nonumber\\[-2pt]
    &\hspace{42mm} +(6m+3)s_2+2s_3\bigr).\label{eq:W}
\end{align}
\end{lemma}
\begin{proof}
For fixed leaf deficits of sum $S$, Lemma~\ref{lem:root} says that the
new deficit ranges from 0 to $m+S$. Its cardinality, sum, and sum of
squares are, respectively,
\[
 m+S+1,\quad
 \frac{(m+S)(m+S+1)}2,\quad
 \frac{(m+S)(m+S+1)(2m+2S+1)}6.
\]
Sum over the $h^k$ leaf configurations, expand, and apply
\eqref{eq:leafsum}. In particular, $W_k$ is a raw second moment, rather
than a binomial moment or a variance.
\end{proof}

\section{The Ehrhart polynomial of the witness}
Write the coordinates of $T$ as $a,b,u,y_i,v_j,z_{j,i}$, where
$1\leq i\leq180$ for the leaves below $u$, and $1\leq j\leq10$,
$1\leq i\leq5$ for the leaves below $v_j$. Besides nonnegativity, the
conditions in $mQ_T$ are exactly
\begin{align*}
 y_i&\leq m,& z_{j,i}&\leq m,\\
 u+\sum_{i=1}^{180}y_i&\leq181m,&
 v_j+\sum_{i=1}^{5}z_{j,i}&\leq6m,\\
 b+u+\sum_i y_i+\sum_j(v_j+\sum_i z_{j,i})&\leq242m,\\
 a+b+u+\sum_i y_i+\sum_j(v_j+\sum_i z_{j,i})&\leq243m.
\end{align*}
Fix configurations in the eleven stars and let $s$ be the sum of their
deficits. The remaining coordinates satisfy
$0\leq b\leq m+s$ and $0\leq a\leq2m+s-b$. Their number is
\begin{equation}\label{eq:top}
 \sum_{b=0}^{m+s}(2m+s-b+1)
 =\frac{(m+s+1)(3m+s+2)}2.
\end{equation}
The bounds are valid also at $m=0$.

Abbreviate
\[
 P=P_{180},\quad D=D_{180},\quad W=W_{180},\qquad
 Q=P_5,\quad d=D_5,\quad w=W_5.
\]
The combined moments of the eleven stars, after extracting the common
factor $h^{230}Q^8$, are
\begin{align}
 N_0&=PQ^2,\nonumber\\
 N_1&=DQ^2+10PQd,\label{eq:combined}\\
 N_2&=WQ^2+10PQw+90Pd^2+20DdQ.\nonumber
\end{align}
For instance, the factor 90 counts ordered pairs of distinct small
stars; the factor 20 counts the two orders of a large--small pair.
All three identities are polynomial factorizations, so no division at
a possibly vanishing value of $Q$ is required.

Summing \eqref{eq:top} using \eqref{eq:combined} gives
\begin{equation}\label{eq:unsimplified}
 E_T(m)=\frac{h^{230}Q^8}{2}
 \bigl((m+1)(3m+2)N_0+(4m+3)N_1+N_2\bigr).
\end{equation}
Substitution from Lemma~\ref{lem:star}, followed by expansion, yields
\eqref{eq:E}--\eqref{eq:f}; here $Q=(7m+2)/2$.
This proves the identity by counting every dilation, not by interpolating
a finite list of values. Alternatively, the count and the right side
agree for infinitely many integers, which identifies the Ehrhart
polynomial uniquely. As checks on normalization, the right side has
degree 243 and constant term $2^8\cdot24/6144=1$.

\section{An exact obstruction to real-rootedness}
For a real polynomial $p$, put $\mathcal L(p)=(p')^2-pp''$.
\begin{lemma}[Laguerre inequality]\label{lem:laguerre}
If a nonzero real polynomial has only real complex roots, then
$\mathcal L(p)(x)\geq0$ for every $x\in\R$.
\end{lemma}
\begin{proof}
The fundamental theorem of algebra factors $p$ into a real constant
and real linear factors, with multiplicities. The product identity
\[
 \mathcal L(pq)=q^2\mathcal L(p)+p^2\mathcal L(q)
\]
follows by differentiation. A constant has $\mathcal L=0$, and a monic
linear polynomial has $\mathcal L=1$. Induction proves the assertion,
including evaluations at repeated roots; no division by $p(x)$ is used.
\end{proof}

For the quintic in \eqref{eq:f}, exact rational arithmetic gives
\begin{align*}
 f(-3/10)&=-716031/50000,\\
 f'(-3/10)&=-854809/1000,\\
 f''(-3/10)&=-2922684,
\end{align*}
and consequently
\begin{equation}\label{eq:negative}
 \mathcal L(f)(-3/10)
 =-\frac{41123948517599}{1000000}<0.
\end{equation}
Lemma~\ref{lem:laguerre} implies that $f$ has a nonreal root. Equation
\eqref{eq:E} makes this a root of $E_T$, proving
Theorem~\ref{thm:main} and disproving the arbor real-rootedness conjecture.
No numerical approximation to a root is needed.

\section{Formal verification and reproducibility}
The accompanying project \lean{arbor-ehrhart-counterexample} formalizes
the actual rooted tree, its descendant inequalities, and a bijection
with the configurations counted above. In particular,
\lean{ArborCounterexample.E_counts_all_dilations} counts every dilation;
\lean{ArborCounterexample.ehrhart_unique} identifies the polynomial;
and \lean{ArborCounterexample.complete_counterexample} combines the
count with the nonreal-root obstruction. The universal conclusion is
\lean{ArborCounterexample.not_all_arbor_ehrhart_roots_real}.

The seven-module verification uses Lean 4.27.0 and mathlib revision
\lean{a3a10db0e9d66acbebf76c5e6a135066525ac900}.
With the dependencies in \lean{lake-manifest.json} provisioned, run
\texttt{\small python3 verify.py}; use \lean{--package-root} for another
dependency location. Reproduction instructions and successful logs are
in \lean{REPRODUCE.txt} and \lean{verification/result.json}.
The final transitive axiom lists contain only \lean{propext},
\lean{Classical.choice}, and \lean{Quot.sound}; there are no proof
placeholders, additional mathematical axioms, or native-computation
certificates. The compiler and pinned library proof objects are trusted.
Lean checks the formal declarations, not the manuscript's prose or
bibliographic claims.

\begin{thebibliography}{9}
\bibitem{Chapoton}
F. Chapoton, \emph{On posets and polytopes attached to arbors},
\href{https://arxiv.org/abs/2503.04247v2}{arXiv:2503.04247v2} (2025).
\bibitem{AC}
C. A. Athanasiadis and F. Chapoton,
\emph{Polytopes and posets associated to preorders},
\href{https://arxiv.org/abs/2605.26916v1}{arXiv:2605.26916v1} (2026).
\bibitem{Higashitani}
A. Higashitani, \emph{Counterexamples of the conjecture on roots of
Ehrhart polynomials},
\href{https://arxiv.org/abs/1106.4633}{arXiv:1106.4633} (2011).
\end{thebibliography}
\end{document}