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

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 ${\mathrm{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.