发表机构
Eötvös Loránd University（罗兰大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该研究确定四项二元多项式乘法的无限制异或-与布尔乘法复杂度为9，解决了Boyar-Find问题，其证明采用结构性方法，且有Lean 4形式化验证，还推导了三项乘法的复杂度为6。
AI 中文摘要
经典下界表明，在F₂上的两个三次多项式相乘，在双线性或二次模型中需要9个标量积，但这些下界并未解决无限制布尔乘法复杂度问题：异或-与电路可复用非线性中间线，且布尔等式按模xᵢ²=xᵢ处理，因此乘法可降低代数次数。设Mul₄: F₂⁸→F₂⁷输出两个四项二元多项式乘积的7个系数，我们证明其无限制异或-与乘法复杂度恰好为9，这针对一类自然的向量值二次函数，解决了Boyar-Find问题，即二次电路下界是否能在无限制非线性复用下保持。证明为结构性而非穷举性：F₂的射影直线P¹(F₂)的三个有理点上必须附加一个有用的纯二次前缀；在假设的8个与门电路中，唯一无用门必须承载三次高位部分，任何有用的后续部分必然迫使一个有理切线并暴露第一个Hasse射流，而外部射流分离结合布尔幂等性，阻止同一缺陷暴露第二个Hasse射流，因此所需的有用后缀不存在。完整的Lean 4形式化验证了布尔代数正规形（ANF）语义、无限制电路模型及该精确定理，未使用项目特定公理或原生判定过程；同样的零缺陷标志论证得出三项乘法的乘法复杂度为6，该方法还分离出五项乘法的多缺陷障碍。
英文摘要
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.
Comments25 pages, 1 table. Complete Lean 4 formalization and verification artifacts: https://github.com/GregoryMorse/unrestricted-boolean-mul
