What this programme is about
When digital circuits compute two independent mathematical operations at once, we expect the total number of multiplications to equal the sum of their individual costs. This programme tests whether shared intermediate products can beat that additive baseline in Boolean logic over GF(2). It concentrates on two concrete problems: whether batching independent operations like 2×2 matrix multiplication or polynomial multiplication can share nonlinear gates, and whether a 26-input Cartesian period-two carry circuit can run in 14 AND gates. In cryptographic proof systems and hardware design, multiplications over GF(2) dominate runtime and circuit area. Settling these bounds tells engineers exactly when parallel tasks can compress into smaller circuits and when searching for further gate reductions is mathematically futile.
What has been settled
MF-163 proves that unrestricted multiplicative complexity is strictly additive when one function meets its linear rank floor or both functions have complexity two; the rank floor carries folklore prior art, while the two-function case is new. Exhaustive DRAT proofs settle MC(x1x2x3 ⊕ y1y2y3y4) = 5 in ML-077. Binary polynomial multiplication MC(polymul_3 over F2) = 6 is proved in MF-148, matching Karatsuba benchmarks. For 2×2 matrix multiplication over GF(2), MF-149 and MF-180 narrow complexity to [6,7], establishing the first unrestricted lower bound of 6, while MF-086 credits Alder and Strassen for the 7s bound in bilinear models. In ML-061, tensor rank fails to transfer lower bounds to unrestricted circuits, noting prior art by Mirwald–Schnorr, Find–Boyar, and Ballet et al. for GF(4) cost 3.
MF-084 proves the separated-product theorem holds over any field under square closure, correcting the field-general reading in MF-032. The mixed-image tax in MF-085 proves that computing an r-dimensional separated quotient in r gates forces every independent target gate to be copy-local. MF-097 confirms that degree r+1 outputs in XOR–AND circuits have decomposable top forms, recording that an earlier scope flag on MF-001 was withdrawn. A four-product counterexample in MF-074 disproves the laminar multiplication-tree normal form.
On the p14 frontier, MF-037 and MF-047 prove standalone wedges intersect the ten-dimensional target in dimension 4, forcing at least six non-input-only gates. MF-034 eliminates all 11-wedge variants, all 8-wedge seeds, and 130 rank-tight 7-wedge seeds. Across affine codes, ML-043 closes all 68 p7-eligible directed edges under zero-catalyst rank-tight rules, aggregating MF-070, MF-071, and MF-072. Finally, MF-121 refutes the general carry-bond tensor floor at J_2, and MF-178 proves tensor slice rank cannot beat the linear dimension floor.
What is still open
The existence of a 14-product circuit for the Cartesian period-two carry target remains unsolved. In MF-124, which supersedes the 817-cell count in MF-105, automated search eliminated 596 candidate cells, leaving 221 surviving decomposition cells alongside the unresolved 12 named frontiers from ML-026. Conjectured structures for this target include a rank-two bilinear bridge gate MF-035, persistent savings under period doubling MF-038, and a lower bound of 15 products MF-039. For matrix multiplication, deciding whether 2×2 matrices over GF(2) require 6 or 7 AND gates ML-088 leaves functional direct-sum additivity open in unrestricted Boolean logic ML-051; the decision instance stands at 155,669 CNF clauses. Other open targets include whether extension-field batching can beat direct-sum additivity MF-014, the unproved summation steps of the FCNS reduction chain MF-112, and the 3-form quadratic transfer gap at 6 variables ML-075.
How to read the evidence
Exhaustive checks and computational receipts dominate this programme's settled results, supported by certified DRAT proofs and written mathematical arguments. Exhaustive checks provide absolute certainty across finite search spaces by ruling out every candidate assignment for specific gate counts and affine-code edges. Receipts log verified solver runs and Gröbner basis reductions. Certified proofs guarantee mechanical auditability. Readers can trust the finite impossibility results completely. Open cells remain unresolved computational bottlenecks awaiting larger searches or new reductions.