AI 中文总结
本文研究树上贪心最大独立集算法的输出分布与均匀分布的偏差，证明精确均匀仅出现在平凡情形，并构造近均匀的蜘蛛图族，给出偏差上界，且定理已在Lean中形式化验证。
AI 中文摘要
选取有限树顶点的均匀随机排序，并运行通常的贪心最大独立集算法。我们将所得最大独立集上的分布与均匀分布进行比较。我们证明，精确均匀性仅出现在单顶点树和单条边这两种情形。证明是结构性的：直径端点暴露出一颗悬挂星，而剩余的单个悬挂叶情形通过一个严格单射解决，该单射在交换悬挂叶与其支撑顶点后于精确排列纤维之间建立。因此，精确均匀性是刚性的，但可以接近。对于一个显式的混合蜘蛛图族 $T_{k,l}$，我们计数最大独立集并计算每个输出的精确概率。当 $l=2^k-k$ 时，全变差偏差为正且满足 [ b(T_{k,2^k-k})=O!\bigl(\frac{\sqrt{k}}{4^k}\bigr)=O!\bigl(\frac{\sqrt{\log n_k}}{n_k^2}\bigr), \qquad n_k=2^k+k+1. ] 该定理包也已在 Lean 中形式化并注册于 Palomar。这些记录记录了机器检查的形式验证和已检查的公理边界；它们不是同行评审或新颖性证明。
英文摘要
Choose a uniformly random ordering of the vertices of a finite tree and run the usual greedy maximal-independent-set algorithm. We compare the resulting law on maximal independent sets with the uniform law. We prove that exact uniformity occurs only for the one-vertex tree and the single edge. The proof is structural: a diameter endpoint exposes a pendant star, and the remaining one-pendant-leaf case is resolved by a strict injection between exact permutation fibres obtained by swapping the pendant leaf with its support vertex. Exact uniformity is therefore rigid, but it can be approached closely. For an explicit mixed-spider family $T_{k,l}$ we count the maximal independent sets and compute the exact probability of every output. With $l=2^k-k$ the total-variation bias is positive and satisfies [ b(T_{k,2^k-k})=O!\left(\frac{\sqrt{k}}{4^k}\right) =O!\left(\frac{\sqrt{\log n_k}}{n_k^2}\right), \qquad n_k=2^k+k+1. ] The theorem package has also been formalised in Lean and registered with Palomar. These records document machine-checked formal verification and the checked axiom boundary; they are not peer review or a certificate of novelty.
Comments10 pages; no figures
