Unrestricted Boolean multiplicative complexity of four-term binary polynomial multiplication
partialconfidence 70%
VibeMathed reports this item as partial. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
Precise statement
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 source statement is reproduced for indexing with attribution. Mathematical correctness requires domain-expert or mechanical review. VibeMath has not independently audited statement
fidelity, correctness, priority, or novelty.
What AI did
OpenAI GPT-5.6 Sol (extra-high); Anthropic Opus 5 (high, referee)
OpenAI GPT-5.6 Sol in extra-high thinking mode was used for research, proof exploration and development, computational checking, Lean 4 formalization and formal-proof engineering, literature and citation verification, manuscript drafting and revision, and release and submission preparation. Anthropic Opus 5 in high thinking mode was used as a critical referee, not as the discovery model. The public disclosure does not attribute a named essential lemma or the central informal proof solely to a model, so the conservative AI-assisted tier is retained rather than AI co-developed or AI-discovered. Gregory Morse directed and reviewed the mathematical claims, informal and formal proofs, computations, citations, code, and manuscript text and assumes full responsibility.
Site-confirmed: rebuilt here on 3 September 2026, not taken from the author's CI badge. This site's verify-lean workflow checked out release n4-arxiv-v2 (commit 2ebc0cf4) of GregoryMorse/unrestricted-boolean-mul, installed the toolchain the repository pins (leanprover/lean4:v4.32.1), ran $\texttt{lake build}$ over every module, then the project's own AxiomAudit.lean, then $\texttt{lake env leanchecker}$ replaying the whole UnrestrictedBooleanMul environment. 24m40s, every step green.
All six headline theorems - the exact values for $n = 0,1,2,3$, the eight-gate impossibility and $\mathrm{MC}(\mathrm{Mul}\,4) = 9$ - report $\texttt{propext}$, $\texttt{Classical.choice}$ and $\texttt{Quot.sound}$ and nothing else. No $\texttt{sorryAx}$, no project axiom, no $\texttt{native\_decide}$, no $\texttt{bv\_decide}$.
The release tag is one commit ahead of 1533276b, which the author's own run used; that commit touches only READMEs, a citation file and checksum lists, no Lean source.
Not Lean-verified. The kernel checks the proof against the statement the author wrote; whether that statement expresses the Boyar-Find question is the anchoring half, and nobody without a stake has audited it.
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.
Known method families
argument (source-reported)
Source-reported tools: argument.
Independent: unknown · difference confidence: 0
What remains uncertain
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.
VibeMath has not independently verified the mathematical claim.
AI-attempt independence and training-data exposure are unknown unless explicitly documented.
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.