发表机构
School of Mathematics and Statistics Northwestern Polytechnical University; University of Toledo（西北工业大学数学与统计学院; 托莱多大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对森林独立多项式序列的单峰性，给出第二个证明，结合分解、矩论证与计算机辅助验证，并附Lean 4形式化证明。
AI 中文摘要
对于有限森林 $F$，令 $i_k(F)$ 为 $F$ 中具有 $k$ 个顶点的独立集的个数。Zhang 和 Li 证明了对于每个有限森林 $F$，序列 $i_0(F),i_1(F),\n\dots,i_{\alpha(F)}(F)$ 是单峰的，这回答了 Erdős 问题 993。我们给出第二个证明。该证明始于他们相对于一个固定独立集的分解，以及 Zhang-Li 和 Fang、Lu、Nevo、Yao 和 Zheng 的界，这些界将序列的一个谷值限制在一个显式的秩窗口内。对于至少有 $25$ 个顶点的森林，一个矩论证排除了窗口内每个秩处的谷值：在硬核均值等于秩的活动度下，随机独立集的大小是最大权独立集上二项分布的混合，谷值是该混合的一个矩不等式，并且通过给定对每个森林都成立的三个界（关于自由顶点数的方差及其拉普拉斯变换，以及方差比）的对偶性将其排除。方差界通过手工证明直到有限多个区间检查，另外两个界通过计算机在有限区间算术覆盖上验证；在所得参数域上，通过有限多个有理盒上的精确检验排除谷值，而自由顶点的平均数量低于显式起始均值（介于 $19$ 和 $50$ 之间），高于该均值则通过一个不等式（带显式常数）对加权谷值核的纤维成立，该不等式手工证明直到有限个显式检查列表，并在混合上取平均。至多有 $24$ 个顶点的森林通过精确计数处理，除在 $43$ 个参数三元组上对两个显式公式进行精确有理求值外，其余均为手工。没有森林被枚举。论文附带了 Lean 4 中该定理的形式化证明。
英文摘要
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_{α(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.
Comments81 pages, 0 figures. Provisional manuscript being rewritten before journal submission. A Lean 4 formalization is described in Section 8. Supplementary data and code are available at the fixed GitHub revision cited in Section 7. Substantial AI contributions are disclosed
