Unrestricted Boolean Multiplicative Complexity of Four-Term Binary Polynomial Multiplication: Rational Places, Hasse Jets, and the Failure of Nonlinear Feedback

Gregory Morse

Source-linked AI summary

Unrestricted Boolean Multiplicative Complexity of Four-Term Binary Polynomial Multiplication: Rational Places, Hasse Jets, and the Failure of Nonlinear Feedback

Gregory Morse

arXiv:2608.30238v1Aug 31, 2026cs.CCcs.DS

TL;DR

The paper addresses whether the classical nine-product lower bound for four-term multiplication survives unrestricted Boolean nonlinear reuse. It proves this through rational-place and Hasse-jet arguments, showing that an eight-AND circuit cannot close, and formalizes the exact theorem in Lean 4. The result establishes unrestricted complexity nine while identifying multi-defect interaction as the remaining issue for five-term multiplication.

Problem
Classical nine-product lower bounds for degree-three multiplication do not settle unrestricted Boolean complexity, where nonlinear wires may be reused and Boolean idempotence may reduce algebraic degree.
Method
The proof normalizes a hypothetical eight-AND circuit around rational places, tracks its unique high-degree defect through Hasse jets, and uses Boolean idempotence and jet separation to block completion.
Results
9 ANDs are exactly necessary for four-term binary polynomial multiplication in the unrestricted XOR–AND model.
Takeaways & Limitations
The result shows that arbitrary Boolean nonlinear reuse does not lower the classical nine-gate value, while the same zero-defect argument gives complexity six for three-term multiplication.
Takeaways & Limitations
For five-term multiplication, the status described here is computational rather than fully algebraic, and several defects may interact across places.

Abstract

from arXiv · show

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.

1 Introduction

The paper asks whether the classical nine-gate lower bound for four-term multiplication survives unrestricted Boolean nonlinear reuse, and proves that it does. It develops an algebraic obstruction to nonlinear feedback, formalized end to end in Lean 4.

Model and problem: Unrestricted XOR–AND circuits may multiply arbitrary previous nonlinear wires, creating higher-degree terms that Boolean idempotence can contract back to degree two.This distinguishes the model from bilinear and quadratic circuits, where such nonlinear internal reuse is absent or restricted.
Model and problem: The open question is whether quadratic-circuit lower bounds remain valid for vector-valued quadratic Boolean functions under unrestricted nonlinear reuse.The paper places this question in the Boyar–Find framework and targets four-term polynomial multiplication.
Main result: 9 ANDs remain necessary for four-term multiplication: nonlinear Boolean feedback still cannot beat the classical bound.The result extends the known value from bilinear and quadratic polynomial-multiplication models to the unrestricted Boolean model.
Proof strategy: A hypothetical eight-AND circuit has one non-useful direction, whose high-degree defect can profitably act only as a rational tangent exposing the first Hasse jet.Exterior jet separation and Boolean idempotence block the second jet, so four useful suffix gates cannot complete the computation.
Formal verification: The proof is algebraic and fully formalized in Lean 4, including Boolean-ANF semantics, unrestricted circuit semantics, the lower bound, and the explicit nine-gate upper bound.The formal development uses the same unrestricted circuit model as the paper rather than checking only isolated finite cases.

3 Hankel target geometry

The target geometry is governed by rank-one Hankel directions corresponding to the three rational places of P^1(F2). Useful extensions preserve this structure by reducing nonlinear contributions into the target subspace.

Rank-one target forms: The three nonzero decomposable target forms are exactly the rank-one Hankel directions r0, r1, and r∞.Their classification identifies the three F2-rational points of the rank-one Hankel curve.
Rational-place prefix: Every useful AND extension of Aff + S adds one of the missing rational-place directions r0, r1, or r∞.Modulo S, each new target direction comes from a product of two affine forms.
Closure of the target geometry: A useful product with no new high-degree direction has dependent quadratic parts, so all nonlinear contributions reduce into S.The reduction uses Boolean idempotence and the rank properties of the rational-place forms.
Rational-place prefix: After one, two, and three useful gates, the all-useful prefix states correspond to subsets of the three rational-place directions.The state counts are determined by one-, two-, and three-element subsets of a three-element set.

4 Rank-two target forms and the degree-two place

The degree-two closed place is represented by a two-dimensional plane whose nonzero members have alternating rank four, separating it from the low-rank Hankel forms.

Rank-two Hankel classification: The binary rank-two Hankel words are classified by four cases obtained through row-span elimination.The cases are derived algebraically rather than by a search, with explicit constraints on c2 through c6.
The degree-two place: The remaining three words span a two-dimensional plane D* satisfying the recurrence with minimal polynomial x^2 + x + 1.Thus D* is the degree-two closed place over F2.
The degree-two place: Every nonzero member of D* has alternating rank four, so D* misses the Grassmannian.The determinant condition is the F4/F2 norm x^2 + xy + y^2 = 1.
Support structure: The six tangent forms are supported on K0, K1, and K∞, while the degree-two forms have support Kdeg 2.The support spaces distinguish rational tangents from the degree-two place.

5 Flag normalization

Flag normalization reduces any hypothetical eight-AND circuit to a canonical form with a forced rational-place prefix, one non-useful seed gate, and a useful suffix.

First-entry replacement: A first-entry target direction can be replaced by any direct one-AND realization without changing later realizable subspaces.Later gate inputs are rewritten in the new basis using XOR only.
Normalized eight-gate form: Any eight-AND circuit can be normalized so its first three gates are r0, r1, and r∞.These gates are moved forward because each rational-place direction depends only on the original inputs.
Normalized eight-gate form: The fourth gate is the unique non-useful gate, while gates five through eight are all useful.The first three place directions are useful, and dimension counting forces every remaining gate after the seed to be useful.
The seed: If the seed had no degree-≥3 component, the first later high-degree gate would create a second non-useful gate.Therefore the seed has nonzero high part; otherwise the circuit would be quadratic and the known lower bound nine would apply.

6 A completion-capable seed is cubic

A normalized seed that admits a useful suffix cannot have a quartic high part, so its nonzero high part is purely cubic. The proof excludes both low–low and seed-using useful continuations.

Quartic exclusion: If a useful suffix gate exists, the seed’s quartic component Q ∧ C must vanish.The quartic exclusion proposition rules out Q ∧ C ≠ 0 for any completion-capable normalized seed.
Low–low child: A low–low useful child would need to cancel the seed’s quartic direction, but the resulting cubic constraints are incompatible with the rational-place support geometry.The argument reduces possible two-planes in R to S3-orbits and excludes each compatible support configuration.
Child using the seed: A useful child using the seed is likewise impossible when the seed has a nonzero quartic part.Boolean idempotence reduces products with two seed-containing factors, after which annihilator and slice arguments produce contradictions.
Conclusion: Therefore neither a low–low nor a seed-using useful child exists when π4(g) ≠ 0.This establishes the quartic exclusion needed to conclude that the seed’s high part is purely cubic.

7 Cubic seeds and feedback annihilators

A cubic seed’s annihilator is tightly constrained by the three rational places, and useful feedback can only begin through a single rational tangent. The resulting first-feedback analysis eliminates every seed-reusing gate-five branch.

A completion-capable seed must have a nonzero cubic high part.
The low-product normal form reduces any relevant seed product, modulo Aff + R, to a common rational-place component G and linear data.
An annihilator meeting T \ R is anchored at one rational place, with dimension two or three.
The rational-place classification shows that only the single-anchor cases can supply an outside-R annihilator direction.
No useful gate five can use the cubic seed, so the first useful continuation must arise from a non-seed low–low branch.
The low–low branch forces a rational tangent and leaves only the hard tangent geometry for subsequent saturation.

8 First-order feedback cannot expose the second jet

After first feedback installs the first Hasse jet, exterior jet separation and Boolean feedback identities prevent any second useful extension, whether it is low–low or seed-reusing.

No product of two wires in Aff + S is a useful gate six in the low–low branch.
No gate six using the seed is useful because the feedback identities force its linear and quadratic corrections to vanish, contradicting the seed’s nonzero high part.
Theorem 8.5 rules out a second useful AND gate after first feedback, regardless of whether the next product is low–low or reuses the seed.

9 The unrestricted Boolean nine-AND theorem

The paper proves that four-term binary polynomial multiplication has unrestricted XOR–AND multiplicative complexity nine. The lower bound excludes every eight-gate circuit structurally, while a two-level Karatsuba–Ofman construction supplies nine gates.

The unrestricted XOR–AND multiplicative complexity of four-term binary polynomial multiplication is 9.
An assumed eight-gate circuit normalizes to three rational-place gates, one nonlinear non-useful seed, and four required useful suffix gates.
The lower-bound contradiction follows because gate five forces first-order rational feedback, while Theorem 8.5 forbids a useful gate six.
A two-level Karatsuba–Ofman construction uses nine AND gates and reconstructs the output coefficients.
The theorem extends classical tight value nine results from polynomial, bilinear, and quadratic models to unrestricted Boolean circuits.

Lean formalization and reproducibility

The complete Lean 4 development formalizes Boolean-ANF semantics, unrestricted circuits, and the exact four-term theorem. Its locked build, axiom audit, declaration replay, and continuous integration support reproducibility without project-specific axioms or native decision procedures.

The formalization represents squarefree monomials by finite variable sets and defines Boolean-ANF multiplication by set union.
Unrestricted circuits are modeled as sequences of products whose factors lie in the span of affine inputs and earlier gate outputs.
The exported proof covers the seven-gate dimension obstruction, eight-gate normalization, cubic seed, first-jet forcing, feedback saturation, and explicit nine-gate upper bound.
The pinned release specifies Lean v4.32.1, a locked mathlib revision, and a clean replay procedure.
Continuous integration performs builds, axiom audits, declaration replays, and a weekly fresh-source replay.
The source contains no sorry, admit, project-specific axiom, native_decide, or bv_decide; the audit reports only standard Lean axioms.

AI assistance disclosure

The paper reports extensive AI assistance across research, development, verification, drafting, and submission preparation, while the author retains responsibility for the final work.

AI systems supported research, proof exploration, development, checking, literature verification, drafting, revision, and submission preparation.
The author reviewed the mathematical claims, proofs, computations, citations, code, and manuscript text and assumes responsibility for the final work.

10 Toward five terms and beyond

The paper frames five-term multiplication as a multi-defect extension of the four-term obstruction, proposing place-degree profiles and a program for determining whether defects can interact.

13 products are optimal in the quadratic or bilinear five-term model, but the unrestricted Boolean optimum is not inferred from that restricted result.
The method is intended to extend beyond n=4 as higher-degree closed places and higher Hasse jets enter the target.
The three-defect Boolean envelope remains a conjecture, and its associated finite-geometry value is computational rather than fully algebraic.
Three non-useful dimensions create a defect budget that mixes purely quadratic and genuinely high-degree defects.
A place-degree profile records the exposed jet order at each closed place and charges higher jets against the corresponding local algebra's multiplicative cost.
The n=4 obstruction indicates that a single rational first-order defect cannot simulate degree-two or second-order local multiplication for free.
The proposed n=5 program normalizes rational-place gates, classifies defect support, proves a multi-defect feedback lemma, and tests whether defects cooperate across places.
If interaction is possible, identifying its minimal local algebra would provide a genuinely new mechanism rather than another exhaustive lower bound.

11 Conclusion

The paper proves that unrestricted XOR–AND multiplication of two four-term binary polynomials requires nine gates, using a structural obstruction to nonlinear reuse. The accompanying Lean 4 formalization kernel-checks the unrestricted theorem, while the paper identifies multi-defect interaction as the next problem.

An eight-gate circuit cannot close because its cubic rational tangent exposes one Hasse derivative, while Boolean idempotence and exterior jet separation block the second.
Nine is classical in bilinear and quadratic models, but its optimality against unrestricted Boolean nonlinear reuse is the paper's new lower-bound statement.
Lean 4 independently kernel-checks the unrestricted semantics and the complete lower- and upper-bound chain.
The structural message is that a first-order rational-place defect buys one first-order jet and no more, leaving multi-defect interaction as the next question.