\documentclass[11pt]{article}
\usepackage[T1]{fontenc}
\usepackage[margin=1in]{geometry}
\usepackage{amsmath,amssymb,amsthm,mathtools,booktabs,microtype,xcolor}
\usepackage{xurl}
\usepackage[colorlinks=true,allcolors=blue!50!black]{hyperref}
\setlength{\emergencystretch}{2em}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newcommand{\lean}[1]{{\small\path{#1}}}
\DeclareMathOperator{\RePart}{Re}
\title{A Nonunimodal Acyclic Polynomial\\with All Roots in the Left Half-Plane}
\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}
Let $A(G,x)$ count vertex subsets of a graph $G$ that induce forests,
by their cardinalities. Barton, Brown, and Pike asked whether failure
of coefficient unimodality forces $A(G,x)$ to have a root with positive
real part. We give a negative answer. The join of $K_{46}$ with three
disjoint copies of $P_3$ has a nonunimodal acyclic polynomial of degree
nine, yet all its complex roots have strictly negative real part.
We derive the polynomial by classifying induced forests and give its
exact positive Hurwitz determinants. A Lean formalization verifies the
graph-to-polynomial identity and the full counterexample, using an
exact rational Lyapunov certificate for strict stability.
\end{abstract}

\section{Introduction}
For a finite simple graph $G$, define its \emph{acyclic polynomial} by
\begin{equation}\label{eq:def}
 A(G,x)=\sum_{\substack{S\subseteq V(G)\\G[S]\text{ is a forest}}}x^{|S|}
       =\sum_{j=0}^{|V(G)|}a_j(G)x^j.
\end{equation}
The induced subgraph on the empty set is included. A finite sequence
$(a_0,\ldots,a_N)$ is \emph{unimodal} if there is an index $m$ such
that it is weakly increasing up to $m$ and weakly decreasing thereafter.
A real polynomial is \emph{strictly Hurwitz stable} if each of its
complex roots has strictly negative real part.

Barton, Brown, and Pike~\cite{BBP} study the coefficients and root
locations of \eqref{eq:def}. In Question~3.4 of the published version,
they ask whether a nonunimodal acyclic polynomial must have a root with
positive real part. The following 55-vertex graph disproves this
implication, even when the conclusion is weakened to a root with
nonnegative real part.

\begin{theorem}\label{thm:main}
Let $H$ be the disjoint union of three copies of the three-vertex path
$P_3=K_{1,2}$, and let $G=K_{46}\vee H$ be the join. Then
\begin{equation}\label{eq:p}
\begin{split}
 A(G,x)={}&1+55x+1485x^2+1464x^3+2196x^4\\
          &\quad+1506x^5+498x^6+82x^7+9x^8+x^9.
\end{split}
\end{equation}
Its coefficient sequence is not unimodal, but every root $z$ satisfies
$\RePart z<0$.
\end{theorem}

The construction uses a clique and is not bipartite. The theorem
addresses Question~3.4 alone; it does not establish a classification of
nonunimodal acyclic polynomials or a minimum order for counterexamples.

\section{Counting the induced forests}
For a graph $H$, let
$I(H,x)=\sum_{S\subseteq V(H),\,S\text{ independent}}x^{|S|}$
be its independence polynomial. The join $K_c\vee H$ adds all edges
between the clique and $H$.

\begin{lemma}\label{lem:join}
For every finite simple graph $H$ and integer $c\geq0$,
\begin{equation}\label{eq:join}
 A(K_c\vee H,x)=A(H,x)+cxI(H,x)+\binom c2x^2.
\end{equation}
\end{lemma}
\begin{proof}
Partition a selected vertex set by the number of vertices it contains
from the clique. If that number is zero, its induced subgraph is a
forest precisely when the selected subgraph of $H$ is a forest. This
contributes $A(H,x)$.

If exactly one clique vertex is selected, any selected edge of $H$
would form a triangle with it. Thus the selected vertices of $H$ must
be independent. Conversely, an independent selection together with
one clique vertex induces a star, so the contribution is $cxI(H,x)$.

If exactly two clique vertices are selected, any selected vertex of
$H$ forms a triangle with them. Hence $H$ must contribute no vertex,
giving $\binom c2x^2$. Three or more clique vertices already contain
a triangle. These cases are disjoint and exhaust all possibilities.
\end{proof}

For a forest on nine vertices every induced subgraph is a forest,
so $A(H,x)=(1+x)^9$ for the $H$ in Theorem~\ref{thm:main}.
The independent sets of $P_3$ give $I(P_3,x)=1+3x+x^2$.
Independence polynomials multiply over disjoint unions, hence
\begin{equation}\label{eq:factored}
 A(G,x)=(1+x)^9+46x(1+3x+x^2)^3+1035x^2.
\end{equation}
Expansion gives \eqref{eq:p}. In particular,
\[
 a_2=1485>1464=a_3<2196=a_4.
\]
A descent at indices $2,3$ forces any unimodal mode to be at most 2,
whereas an ascent at indices $3,4$ forces it to be at least 4.
This contradiction proves nonunimodality. Including the zero
coefficients above degree nine does not alter this conclusion.

\section{Exact strict stability}\label{sec:hurwitz}
We recall the Hurwitz criterion~\cite{Hurwitz}. For a real polynomial
\[
 p(x)=b_0x^d+b_1x^{d-1}+\cdots+b_d,\qquad b_0>0,
\]
extend the coefficient list by $b_j=0$ for $j<0$ or $j>d$.
Its Hurwitz matrix has entries $H_{ij}=b_{2j-i}$ for
$1\leq i,j\leq d$. All roots of $p$ have negative real part if and
only if all leading principal determinants
$\Delta_r=\det H[1\!:\!r,1\!:\!r]$, $1\leq r\leq d$, are positive.

For the polynomial in \eqref{eq:p}, the descending coefficient list is
\[
 (b_0,\ldots,b_9)=(1,9,82,498,1506,2196,1464,1485,55,1).
\]
In particular, the matrix to be checked is explicitly
{\small
\[
\setlength{\arraycolsep}{3pt}
H=\begin{pmatrix}
9&498&2196&1485&1&0&0&0&0\\
1&82&1506&1464&55&0&0&0&0\\
0&9&498&2196&1485&1&0&0&0\\
0&1&82&1506&1464&55&0&0&0\\
0&0&9&498&2196&1485&1&0&0\\
0&0&1&82&1506&1464&55&0&0\\
0&0&0&9&498&2196&1485&1&0\\
0&0&0&1&82&1506&1464&55&0\\
0&0&0&0&9&498&2196&1485&1
\end{pmatrix}.
\]
}
Exact determinant evaluation gives the following certificate.
\begin{center}
\begin{tabular}{cr}
\toprule
$r$ & $\Delta_r$\\
\midrule
1&9\\
2&240\\
3&17298\\
4&10581516\\
5&17654863239\\
6&3903814488441\\
7&4104634643529867\\
8&221412068364709627\\
9&221412068364709627\\
\bottomrule
\end{tabular}
\end{center}
Every entry is positive, so the criterion proves strict stability.
Together with Section~2, this completes the proof of
Theorem~\ref{thm:main}. These are integer determinant identities, not
approximations to roots near the imaginary axis.

\section{The formal root certificate}
The Lean development uses a rational Lyapunov certificate rather than
assuming the Hurwitz criterion as a formal premise. We explain the
argument to specify exactly what is checked.

Let $c_j$ be the ascending coefficients of $p$ in \eqref{eq:p}, so
$c_9=1$. Define $C\in\mathbb R^{9\times9}$ by
\[
 C_{0j}=-c_{8-j}\quad(0\leq j\leq8),\qquad
 C_{i,i-1}=1\quad(1\leq i\leq8),
\]
with other entries zero. At a root $z$ of $p$ the vector
$v=(z^8,z^7,\ldots,z,1)^{\mathsf T}$ satisfies $Cv=zv$.
The formal certificate supplies a rational symmetric matrix $P$, a
rational unit lower triangular matrix $L$, and a positive diagonal
matrix $D$ such that
\begin{equation}\label{eq:lyapunov}
 P=LDL^{\mathsf T},\qquad
 C^{\mathsf T}P+PC=-\delta e_8e_8^{\mathsf T},
 \qquad \delta=442824136729419254.
\end{equation}
The matrices and exact entrywise identities are in
\lean{Acyclic/Certificate.lean}; their rational data are also recorded
in \lean{documentation/direct-certificate.json}.

For completeness, the diagonal entries used there are
\begin{align*}
 &4104634643529867,\quad3903814488441,\\
 &\frac{434333309604785204292411317}{456070515947763},\quad
   \frac{780958447998089584484844}{1301271496147},\\
 &\frac{425553995396971903094}{1961651471},\quad
   \frac{4428241367294192540}{881793},\\
 &\frac{221412068364709627}{1922},\quad
   \frac{221412068364709627}{240},\quad
   \frac{221412068364709627}{9}.
\end{align*}
They are strictly positive, and the factorization in \eqref{eq:lyapunov}
implies $v^*Pv\geq0$. Multiplying the second identity by $v^*$ and
$v$, and using $Cv=zv$ and $v_8=1$, yields
\[
 2\RePart(z)\,v^*Pv=-\delta<0.
\]
If $\RePart z\geq0$, the left side is nonnegative, a contradiction.
Thus the certificate proves $\RePart z<0$ for every root. All
certificate identities and positivity statements are checked in Lean
over exact rationals and complex numbers.

\section{Formal scope and reproducibility}
The project \lean{acyclic-hurwitz-counterexample} defines the actual
55-vertex graph, vertex-induced acyclicity, and the coefficient counts
in \eqref{eq:def}. Its graph classification proves the cases of
Lemma~\ref{lem:join} for the witness, and
\lean{AcyclicCounterexample.candidateGraph_polynomial} proves
\eqref{eq:p} with the actual graph semantics. The endpoints
\lean{AcyclicCounterexample.question34_counterexample} and
\lean{AcyclicCounterexample.question34_false} combine nonunimodality
with the strict root bound. They do not assume a graph-counting bridge
or use numerical root finding.

The 15-module verification uses Lean 4.27.0 and mathlib revision
\lean{a3a10db0e9d66acbebf76c5e6a135066525ac900}; all
package revisions are pinned in \lean{lake-manifest.json}. With the
dependencies provisioned, run
\texttt{\small python3 scripts/verify.py --packages /path/to/packages}.
Successful logs, source identities, and transitive axiom audits are
recorded in \lean{verification/result.json}. Only \lean{propext},
\lean{Classical.choice}, and \lean{Quot.sound} occur in the audited
final dependencies. There are no proof placeholders, additional
mathematical axioms, or native-computation certificates. The pinned
compiler and cached library proofs remain trusted. This formal result
does not assert a minimum counterexample order or bibliographic priority.

\begin{thebibliography}{9}
\bibitem{BBP}
C. Barton, J. I. Brown, and D. A. Pike,
\emph{Acyclic polynomials of graphs}, Australas. J. Combin.
\textbf{82}(2) (2022), 146--181.
\url{https://ajc.maths.uq.edu.au/pdf/82/ajc_v82_p146.pdf}.
\bibitem{Hurwitz}
A. Hurwitz, \emph{Ueber die Bedingungen, unter welchen eine Gleichung
nur Wurzeln mit negativen reellen Theilen besitzt}, Math. Ann.
\textbf{46} (1895), 273--284.
\url{https://doi.org/10.1007/BF01446812}.
\end{thebibliography}
\end{document}