比特鸽巢原理在奇偶校验上的消解中的指数下界
An exponential lower bound for the bit pigeonhole principle in resolution over parities
AI总结：
本文证明比特鸽巢原理在奇偶校验消解中具有指数级子句数下界，通过转换为多项式演算并利用棋盘复形同调，且证明在 Lean 4 中形式化。
AI中文摘要：
奇偶校验上的消解，即 $\mathrm{Res}(\oplus)$，是线性方程消解的特征二版本：子句是 $\mathbb F_2$ 上仿射方程的析取。此前，超多项式规模下界仅对受限反驳已知：树状、正则或有界深度。我们证明，对于 $n+1$ 只鸽子和 $n=2^\ell$ 个洞的比特鸽巢原理，每个 DAG 状 $\mathrm{Res}(\oplus)$ 反驳，在 $\ell\ge32$ 时，都有超过 $\exp(n/(32768\ell^2))=2^{\Omega(n/\log^2 n)}$ 个子句，且对正则性或深度无任何限制。证明将任意具有 $S$ 个子句的反驳转换为 Buss、Impagliazzo、Krajicek、Pudlak、Razborov 和 Sgall 风格的多项式演算反驳，其度为 $O(\log n)$，涉及 $O(S+n^2)$ 组扩展变量。一次替换即可同时移除所有扩展变量，并留下一个非零低次多项式，该多项式仅由鸽巢公理在至多 $n/2$ 次度下导出；Razborov 风格的度下界（通过棋盘复形的同调证明）表明不存在这样的推导。该论证还给出了 $\mathrm{Res}(\oplus)$ 规模下界的一般充分条件。主定理、该条件及其所有依赖均在 Lean 4 中形式化，每个陈述都链接到其形式化证明。该证明是在最后一部分描述的开放研究框架内，借助大量 AI 辅助开发的。
英文摘要：
Resolution over parities, $\mathrm{Res}(\oplus)$, is the characteristic-two version of resolution over linear equations: clauses are disjunctions of affine equations over $\mathbb F_2$. Superpolynomial size lower bounds were previously known only for restricted refutations: tree-like, regular, or of bounded depth. We prove that every DAG-like $\mathrm{Res} (\oplus)$ refutation of the bit pigeonhole principle with $n+1$ pigeons and $n=2^\ell$ holes has more than $\exp(n/(32768\ell^2))=2^{Ω(n/\log^2 n)}$ clauses, for every $\ell\ge32$, with no restriction on regularity or depth. The proof translates an arbitrary refutation with $S$ clauses into a polynomial calculus refutation of degree $O(\log n)$ over $O(S+n^2)$ groups of extension variables in the style of Buss, Impagliazzo, Krajicek, Pudlak, Razborov, and Sgall. One substitution then removes all extension variables at once and leaves a nonzero low-degree polynomial derived from the pigeonhole axioms alone at degree at most $n/2$; a degree lower bound in the style of Razborov, proved through the homology of chessboard complexes, shows that no such derivation exists. The argument also yields a general sufficient condition for $\mathrm{Res}(\oplus)$ size lower bounds. The main theorem, this condition, and all their dependencies are formalized in Lean 4, and every statement links to its formal proof. The proof was developed with substantial AI assistance within an open research framework described in the final section.
