Exact Boolean multiplicative complexity of four-term polynomial multiplication

Source: arxiv:2608.30238v1, url:https://github.com/GregoryMorse/unrestricted-boolean-mul/tree/79a801760668f52bb00a9e1a406e841375c58a6d Authors: Gregory Morse Status: verified Main declarations: UnrestrictedBooleanMul.N4.mc_mul_four Tags: computational-complexity, boolean-circuits, polynomial-multiplication, algebraic-normal-form MSC: 68Q06, 68Q17, 68W30, 15A75, 94D10

The circuit model allows arbitrary reuse of earlier nonlinear wires, with XOR and constants free. The exact values for input lengths zero through four are proved internally. General infrastructure includes Boolean ANFs, circuit dimension bounds and rewiring, and Reed–Muller weight bounds.

This imports the published four-term result from Gregory Morse's MIT-licensed repository. The August 31, 2026 Lean release establishes eligibility; the pinned September revision ports and packages the same result. The author discloses an AI proof-development workflow under his direction and review. The project card records AI provenance and the source details. The upstream license notice is retained below.