Research · Papers · Adders, counters and the heap law · MF-083
An eight-product circuit for the low four bits of four four-bit numbers
The low four bits of x₀ + x₁ + x₂ + x₃ are computed by an acyclic XAG with 8 products
Published 2026-08-29
For everyone
Plain summary
Adding four four-bit numbers to get the low four bits of their sum takes eight multiplication steps in an acyclic circuit. In this model, each product is an AND operation on two affine combinations of inputs, constants, and earlier products. An exhaustive check across all 65,536 16-bit inputs produced zero mismatches, confirming that the 4op_w4_p8 instance is satisfiable. This circuit matches the carry-save baseline from MF-082 without improving on it. It leaves open whether a seven-product circuit exists. The register takes no position on external prior art for this witness.
Result
Let x₀, x₁, x₂, x₃ be four four-bit operands given as 16 operand-major little-endian input bits. The low four bits of x₀ + x₁ + x₂ + x₃ are computed by an acyclic XAG containing eight products. Each product multiplies two affine factors over {1, inputs, earlier products}, and each output is an affine readout. The explicit circuit matches the target across all 65,536 input assignments, establishing that 4op_w4_p8 is SAT under the discriminator model.
This witness establishes feasibility at eight products. It provides neither a lower bound at seven products nor a seven-product witness.
Setting and definitions
The instance 4op_w4_p8 specifies the low-four-bit modular sum of four four-bit operands in an acyclic XAG model. Product factors are affine combinations of 1, primary inputs, and earlier products; outputs are affine readouts over the full signal pool. The parameter p = 8 bounds the product count, and SAT marks the existence of a valid circuit over the full domain.
Method
MF-082 provides a carry-save circuit using 3·4−4 = 8 products. The eight-gate list and four affine readouts were generated and recorded in a witness certificate. Replaying this certificate against the discriminator truth table over all 65,536 points yielded zero mismatches.
An independent verifier parsed the gate strings, checked acyclicity, verified that all factors are affine, and evaluated the full domain using plain integers without sharing code with the bitmask emitter. Its verification receipt logs 8 gates, 65,536 points, 0 mismatches, and passing status.
The circuit also functions as a regression canary, confirming witness_validated=true, mismatches=0, and domain_points=65536. The discriminator configuration and raw verification receipts are provided in this paper's downloadable evidence pack.
Discussion
This witness resolves p = 8 without relying on SAT search. The corresponding CNF encoding contained 19,727,307 variables and 73,338,610 clauses (1.77 GB), but three solver attempts returned UNKNOWN_OR_ERROR.
The open question is p = 7. An UNSAT certificate at p = 7 would establish that 8 products are optimal, whereas a SAT assignment would beat the carry-save baseline and mark the program's first multi-operand addition improvement. An initial kissat run at p = 7 aborted with UNKNOWN_OR_ERROR on out-of-memory, and an active cadical run with DRAT logging was unresolved at ledger entry time. The register contains no resolved verdict for p = 7.
The witness demonstrates feasibility at 8 products, matching the baseline without establishing optimality or asserting external prior art.
For everyone — the takeaway
What this means
You can add four 4-bit numbers and get the bottom four bits using only eight multiplication steps. We verified this circuit against all 65,536 possible inputs with zero errors, settling the question of whether an eight-product solution exists. What remains is finding out if seven products can do the job. Finding a seven-product circuit would beat the standard carry-save method, while proving none exists would show eight is optimal. This paper doesn't settle that question; it provides the verified eight-product circuit and its independent test receipts.
Register references
Entry: MF-083.
Receipt artifacts: emit_4op_w4_p8_witness.py (SHA-256 827a1fd6…77ee); 4op_w4_p8_witness_certificate.json (SHA-256 df675452…af5de); independent_witness_verifier.py (SHA-256 cd5ac487…26bd); independent_witness_replay.json (SHA-256 60d2565c…1179); factory/discriminators/DISCRIMINATOR-4OP.md.
Prior art: the register does not record this.
Every artifact named above is bundled in, or hashed by, this paper's evidence pack below.
Evidence pack
Everything needed to check this entry against its receipts: the register text, a manifest with a SHA-256 hash for every named receipt, and 4 of 6 receipt files bundled (6 KB). Anything not bundled is still hashed in the manifest and lives in the compute-box working trees.
Changelog
Last reviewed 2026-08-29
- 2026-08-29Published on this site.