A fast algorithm pays twice
It costs multiplications, and it costs additions, and the two are counted by different questions. tensor-rank-toolkit answers both exactly on the maps small enough to answer, where exactly means proved rather than found: a rank closed from both sides, and a nonzero count that is the least any change of basis can leave.
Two costs, not one
An algorithm for a bilinear map is three operators: L and R encoding the two operands, P combining the products. Its multiplications are the rank of the map, which is what a decomposition of the tensor counts. Its additions are set by how many nonzero entries those three operators carry, which the multiplication count never sees. Both are minimised here, by different mathematics, and they are reported as two numbers rather than folded into one. Sources: README.md, what-it-computes.md.
What makes a number here a fact
Nothing in the library is ever a float, so a reported rank is a fact about the map rather than an artefact of rounding, and every decomposition is rebuilt and multiplied back out against the map before it is printed. The solver route writes its refutations as DRAT and has drat-trim check them, so a lower bound from a solver is verifiable rather than trusted, and the theorems the routes rest on are stated and proved in article/bilinear-rank.pdf. Every count the repository can re-derive is re-derived from the built binaries on every push, by reproduce/measure.py --check. The few it cannot are named one at a time, with what each would cost to run, in reproduce/questions.py, so a carried number says on its own row that nothing re-derives it.
Multiplications, and one map settled at 13
Multiplying two 5-coefficient polynomials over GF(2) takes 25 multiplications done naively, and the cheap descent brings that to 14. Nine, ten and eleven products are then refused by rank_lower_bound before the search opens a single node. Twelve is ruled out by exhaustion, 146 402 553 nodes walked to the end of the tree. lower-the-bound then exhibits a thirteen in 80 nodes. Floor and ceiling meet, so the rank is exactly 13, and both halves of that are now proved inside the repository. Barbulescu, Detrey, Estibals and Zimmermann published the same 13 in 2012, so nothing here beats it; what changed is that the line no longer rests on their reporting it. Sources: descent_search/results.json, descent_search/what-the-exact-search-decides.md, incumbent_search/what-it-reaches.md.
descent_search/what-the-exact-search-decides.md and incumbent_search/what-it-reaches.md.Additions, and 221 nonzeros brought to a proved 128
The other cost is set by the operators. Given U, the question is which invertible change of basis V leaves U V with the fewest nonzero entries. Strassen’s two encoding operators go from 12 nonzeros to 10, and an alternative-basis operator from 21 to 10, which takes Strassen’s 18 additions to 12 and the leading coefficient of 7·N^log₂7 − 6·N² from 7 to 5. Ten is not the best found but the least any change of basis can leave: choosing the sparsest basis of a subspace is a matroid problem, and a greedy returns a minimum-weight basis of any matroid. On the three encoding operators of a published rank-23 ⟨3,3,3⟩ scheme that is 221 nonzeros to 128, in about a third of a second, and 128 is again the proved minimum rather than the best found. Every entry those three matrices are left with is 0, +1 or −1, so the count hides no multiplication: an entry outside that alphabet would cost one on top of its addition, and there is none. Sources: matrix_sparsification/README.md, matrix_sparsification/what-it-is-worth.md.
matrix_sparsification/results.json.One ⟨4,4,4⟩ operator is past searching altogether, at fourteen million column subsets at weight six, and is answered by not searching: one linear programme per coordinate, in exact rationals, reaching a verified basis at 100 nonzeros in a third of a second. That route returns an upper bound rather than a proof, and it reaches the proved minimum anyway on every operator where a proof exists, between four and fifteen times faster than the search that proves it. Why it should is an open question, since the theorem that suggested it turns out to apply to none of the operators measured. Source: matrix_sparsification/method/answering-without-searching.md.
And fewer nonzeros is not the same as fewer additions. Hand the output of the exact stage to a pass that finds common subexpressions and a raw scheme improves by 23%, two already-polished ones by 2% and 7%, and one operator of nine goes the wrong way: six more zeros there cost two additions. A basis of least weight is not a basis with the most shared subexpressions, so the proxy is measured rather than assumed and the two counts are reported apart. The published record shows the size of that gap: evaluated naively those 128 entries over 55 rows cost 73 additions, where Karunaratne and Idamekorala give a 55-addition circuit for a rank-23 ⟨3,3,3⟩ tensor (arXiv:2607.28676, 2026), over the alphabet 0, +1, −1 and provably optimal for that orientation. The two count different things, one a circuit sharing subexpressions in the standard basis and the other a nonzero count under a change of basis, so neither is a score against the other. Sources: matrix_sparsification/measured-with-other-tools/before-a-subexpression-pass.md, matrix_sparsification/what-it-is-worth.md.
Both halves, in a browser
A decomposition is not the deliverable; the algorithm is. The rank search recovers the three operators from the decomposition it finds and writes them out, and the sparsification is what they are for: minimise-rank fixtures/f2_5x5.tensor --emit-operators out takes 25 multiplications to 14, and sparsify-operator out_L.sms then takes that operator from 31 nonzeros to 27. Fewer multiplications, then fewer additions, from one map, in two commands.
The same two run in that order from a browser, as the console’s decompose-then-sparsify flow: one press, four runs, each an ordinary run with its own command, its own card and its own exit code. Twelve of the thirteen tools are on it, each stating what it asks, and the command is shown before it runs and again beside the answer as a line that can be retyped at a terminal. It listens on the loopback address, so only that machine can reach it, and it needs Python 3’s standard library and nothing else, which is exactly what building the toolkit needed. Source: web_interface/README.md.
What is proved, and what is not
Each proof here is an exhaustion over one map at one size, or a minimum over one operator. The bilinear rank problem itself is still open, no upper bound on this page proves anything on its own, and exact arithmetic makes an answer trustworthy rather than optimal. The descent proves nothing at all: what it returns is a decomposition, not a claim about the true rank. Timings are the other kind of number, taken on one core of an i5-12450H, fastest of three runs on a quiet machine, and worth an order of magnitude rather than a digit: no test asserts one and CI checks none, because a shared runner would turn a real regression and a noisy afternoon into the same red tick. The counts are exact, asserted by the test suite, and rerun on every push. Protocol: MEASURING.md.