Unrestricted Boolean multiplicative complexity of four-term binary polynomial multiplication

Let Mul4: F_2^8 -> F_2^7 output the seven coefficients of the product of two four-term binary polynomials. The manuscript proves that its unrestricted XOR--AND multiplicative complexity is exactly 9. The upper bound is a nine-AND Karatsuba--Ofman construction. The lower bound rules out every unrestricted eight-AND circuit, including circuits that reuse nonlinear intermediate wires and exploit Boolean idempotence. Thus, for this natural vector-valued quadratic function, allowing nonlinear feedback does not improve on the optimal quadratic circuit.

The exact Mul4 instance is resolved: its unrestricted XOR--AND multiplicative complexity is 9. The restricted bilinear/quadratic value 9 was classical; the new theorem proves that arbitrary nonlinear Boolean reuse cannot lower it. This is a natural positive special case of the Boyar--Find question, not a solution of the general (n,m) problem. The lower bound is a conceptual structural argument. A complete Lean 4 formalization checks the unrestricted circuit semantics and the exact equality, while the development-time Python/C++ programs remain independent regression checks rather than logical premises. The corresponding unrestricted questions for five or more terms remain open. Independent statement-fidelity review remains pending.