Unrestricted Boolean multiplicative complexity of four-term binary polynomial multiplication

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.

Exact FrontierDelta

proved→proved

Scope and record

Occurred: Sep 3, 2026

Delta type: REGISTRY REVISION

Assumptions: VibeMathed verification: site-confirmed. Publication: preprint. AI contribution: ai-assisted. Editorial metadata: CC BY 4.0; linked content retains its own rights.

Canonical aliases: Unrestricted Boolean multiplicative complexity of four-term binary polynomial multiplication · Unrestricted multiplicative complexity of Mul4

Confidence: Not scored

Registry verification: site confirmed · preprint · partial

Open the source record ↗

Attribution

VibeMathed
registry · event recorded by

OpenAI GPT-5.6 Sol (extra-high)
model · ai model contributor · OpenAI

Anthropic Opus 5 (high, referee)
model · ai model contributor · Anthropic

Evidence vector

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review

Named evidence

VibeMathed record: Unrestricted Boolean multiplicative complexity of four-term binary polynomial multiplication

specialist registry · passed

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.