← 研踪 PaperTrailarXiv:2611.15992 · v1
The multiplicative complexity of the three-bit low-half multiplier
首次提交 2026-11-12 04:44
版本更新 2026-11-12 04:44
雷达观测 2026-11-13 14:16
摘要
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. is fully formalized in Lean 4. The kernel-checked proof uses only the axioms propext, Classical.choice and Quot.sound.
作者备注：21 pages, 1 table. Lean formalization and verification artifacts: https://github.com/bishara74/lowhalf-mul3
观测到的版本
相邻记录可能跳过中间版本；首次发现 v2 及以上也会标为版本更新。
v1 · 2026-11-12 04:44 · 最新观测版本
The multiplicative complexity of the three-bit low-half multiplier
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. is fully formalized in Lean 4. The kernel-checked proof uses only the axioms propext, Classical.choice and Quot.sound.
查看此版本解读 →查看此版本原文 ↗