Unimodality of Forest Independence Polynomials

For a finite forest $F$ let $i_k(F)$ be the number of independent sets of $F$ with $k$ vertices. Zhang and Li proved that the sequence $i_0(F),i_1(F),\dots,i_{\alpha(F)}(F)$ is unimodal for every finite forest $F$, which answers Erdős Problem 993. We give a second proof. It starts from their decomposition relative to a fixed independent set and from the bounds of Zhang and Li and of Fang, Lu, Nevo, Yao and Zheng that confine a valley of the sequence to an explicit window of ranks. For a forest with at least $25$ vertices, one moment argument excludes a valley at every rank of the window: at the activity where the hard-core mean equals the rank, the size of a random independent set is a mixture of binomial laws over an independent set of maximum weight, a valley is a moment inequality for this mixture, and it is excluded by duality given three bounds that hold for every forest, on the variance of the number of free vertices and on its Laplace transforms, and on the variance ratio. The variance bound is proved by hand up to finitely many interval checks and the other two bounds are verified by computer on finite interval-arithmetic coverings; on the resulting parameter domain a valley is excluded by exact tests on finitely many rational boxes while the mean number of free vertices is below an explicit starting mean between $19$ and $50$, and above it by one inequality, with explicit constants, for the fibers of a weighted valley kernel, proved by hand up to a finite list of explicit checks and averaged over the mixture. Forests with at most $24$ vertices are treated by exact counting, by hand except for exact rational evaluations of two explicit formulas at $43$ parameter triples. No forest is enumerated. A formal proof of the theorem in Lean 4 accompanies the paper. Version 2.2 (6 October 2026), by Wei Li, Kevin Vallier, and Tong Zhang. This is a provisional manuscript being rewritten before journal submission and shared for examination by the community. Substantial AI contributions to the mathematical arguments, formal proofs, and text are disclosed in the manuscript. The PDF and LaTeX source correspond to the manuscript submitted to arXiv on 6 October 2026. Supplementary data and code are available at the fixed GitHub revision cited in Section 7: https://github.com/zhangzenozhang-jpg/forest-unimodality-v2.2-supplement/tree/9f4f1ecfc439fdf43f8cfad0e888e54fe778d428. The manuscript describes the computational verification and Lean 4 formalization in Sections 7 and 8. This version follows the earlier two-author manuscript, Unimodality of Forest Independence Polynomials, by Tong Zhang and Wei Li, published on 27 September 2026 (https://doi.org/10.5281/zenodo.22999166). That earlier version remains available under its original DOI, with its original authorship and publication date. The present three-author manuscript is dated 6 October 2026 and presents a second proof.