An exponential lower bound for the bit pigeonhole principle in resolution over parities

What the AI did

GPT-6 Astra was the principal contributor to the mathematical development, manuscript drafting, and Lean formalization. Earlier exploration involved Claude Sonnet 5, Fable 5.1, and Opus 5. Later revised using Fable 5.1. Kamil Braun designed and directed the Noemesis research framework, supplied goals and steering, and organized the verification and publication effort. Section 10.3 of the revised manuscript describes the contributions and development history.

Verification

Held on 15 September 2026 for one reason: nothing outside the author's machine had compiled the proof. Lifted on 22 September. GitHub Actions run 34953139115 (commit 3979e0c, fresh ubuntu-24.04 runner, mathlib cache for dependencies only, .lake/build deleted) ran `lake --wfail build claims.BitPHPSuperpolynomial` & replayed the module in a fresh leanchecker kernel. Run 35282748811 (17 September UTC, commit e4c7723, same setup) did the same for `claims.BitPHPPreprintRevision1`, which adds the revised version's MathResearch.bitPHP_exponential: for $l >= 32$, more than $exp(2^l/(32768 l^2))$ nodes. Both theorems use only propext, Classical.choice and Quot.sound. Audit at 54f0937, byte-identical to 3979e0c: the superpolynomial theorem quantifies over every AffineDAG over the standard bit-PHP initial clauses with a node deriving the empty clause; AffineDAGStep allows initial clauses, semantic weakening, resolution on a parity literal against its complement & any sound two-premise rule, nodes reference any earlier node, no regularity or depth constraint, a superset of dag-like $\mathrm{Res}(\oplus)$; usualCNFClause is the standard bit-PHP axiom over all pairs & all $2^l$ labels; the chessboard homology is proved, not assumed. e4c7723 only adds files, & the exponential theorem uses the same definitions. No sorry, custom axiom or native_decide at either commit. Kernel-checked on a machine other than the author's, statement audited: Lean-verified. No specialist has read the argument.

Sources

• PaperAn exponential lower bound for the bit pigeonhole principle in resolution over parities
• Lean proofkbr-/math-research: whitepaper at commit 652e617, Lean claim BitPHPPreprintRevision1.lean built by CI at e4c7723 · Final Lean theorem
• Independent workGitHub Actions build on a fresh runner: axioms and kernel replay