Unrestricted Boolean Multiplicative Complexity of Four-Term Binary Polynomial Multiplication: Rational Places, Hasse Jets, and the Failure of Nonlinear Feedback
2026-08-31 • Computational Complexity
Computational ComplexityData Structures and Algorithms
AI summaryⓘ
The authors studied how hard it is to multiply two special kinds of polynomials using XOR and AND gates in circuits. They proved that for multiplying two polynomials with four terms over a simple number system, you need exactly nine AND gates, even if you can reuse parts of the circuit in complex ways. Their proof uses advanced algebraic and geometric concepts instead of checking all possibilities. They also confirmed their results with computer-aided formal verification. This work answers a known open question about circuit complexity for these polynomial multiplications.
Boolean multiplicative complexityXOR-AND circuitspolynomial multiplicationfinite field F2algebraic normal form (ANF)Hasse jetcircuit lower boundsformal verificationprojective line P1(F2)Boolean idempotence
Authors
Gregory Morse
Abstract
Classical lower bounds show that multiplying two degree-three polynomials over $\mathbb F_2$ requires nine scalar products in bilinear or quadratic models. They do not settle unrestricted Boolean multiplicative complexity: an XOR--AND circuit may reuse nonlinear intermediate wires, and Boolean equality is taken modulo $x_i^2=x_i$, so a multiplication can lower algebraic degree. Let $\operatorname{Mul}_4:\mathbb F_2^8\to\mathbb F_2^7$ output the seven coefficients of the product of two four-term binary polynomials. We prove that its unrestricted XOR--AND multiplicative complexity is exactly nine. This resolves, for a natural vector-valued quadratic function, the Boyar--Find question of whether a quadratic-circuit lower bound can persist against unrestricted nonlinear reuse. The proof is structural rather than exhaustive. A useful purely quadratic prefix is forced onto the three rational places of $\mathbb P^1(\mathbb F_2)$. In a hypothetical eight-AND circuit, the unique non-useful gate must carry a cubic high part. Any useful continuation then forces a rational tangent and exposes a first Hasse jet, while exterior jet separation together with Boolean idempotence prevents the same defect from exposing the second Hasse jet. The required useful suffix therefore cannot exist. A complete Lean 4 formalization verifies the Boolean-ANF semantics, the unrestricted circuit model, and the exact theorem; it uses no project-specific axiom or native decision procedure. The same zero-defect flag argument gives multiplicative complexity six for three-term multiplication, and the method isolates the multi-defect obstruction for five terms.