Papers With

← All papers
First page of The multiplicative complexity of the three-bit low-half multiplier

The multiplicative complexity of the three-bit low-half multiplier

Bshara Alhodali, Gregory Morse

cs.CC Nov 11, 2026 · v1 cs.LO math.CO
formalization combinatorics logic
Read PDF arXiv abstract Code
TL;DR
The full theorem MC(M3)=6, both the upper and lower bounds, is formalized in Lean 4, with finite-computation lemmas checking individual proof steps.
Abstract
We prove that the multiplicative complexity of the three-bit low-half multiplier is six, giving a structural, enumeration-free lower-bound proof valid against unrestricted nonlinear reuse in Boolean XOR-AND circuits. The value was previously established by SAT searches of the second author. An explicit six-AND circuit supplies the upper bound. The lower bound combines derivatives, quadratic products, complementary minors, and extraction modulo a Boolean ideal. Independent finite checks accompany the arguments. $\mathrm{MC}(M_3)=6$ is fully formalized in Lean 4. The kernel-checked proof uses only the axioms propext, Classical.choice and Quot.sound.
Problem

Determine the exact multiplicative complexity (number of AND gates in XOR-AND circuits with unrestricted nonlinear reuse) of the three-bit low-half multiplier M3. Earlier SAT searches gave the value six; a structural, enumeration-free lower-bound proof was missing.

Approach

An explicit six-AND circuit gives the upper bound. The lower bound normalizes a putative five-gate circuit by its number of initial linear gates and excludes each case. The tools are derivatives along good directions, quadratic products, exterior-form and complementary-minor arguments, and extraction modulo a Boolean ideal. The theorem is formalized in Lean 4, with named finite-computation lemmas checking individual case steps.

Results

MC(M3)=6 is proved by a hand-checkable structural argument. The Lean 4 proof is kernel-checked using only the axioms propext, Classical.choice and Quot.sound.