Four hundred and seventy steps

The tartan theorem establishes a fact: lay two coin-turning games out along the two axes of a grid, and the Grundy value of a single head at square (x, y) is the nimber product of the two coordinates’ one-dimensional values. The nimbers multiply establishes that the multiplication in question is a genuine field operation, with every axiom checked.

Between them they say the theorem is true and the arithmetic is sound. Neither says what the theorem is for, and the answer to that is a number.

A grid of n squares has 2ⁿ arrangements of heads and tails, and a solver with no theory has to value every one of them. The measurement confirms that literally: on a 3 × 4 grid the brute force valued all 4,096, not one fewer, because nothing lets it skip any.

The theorem values the same grid with twelve multiplications.

Four squares: 16 against 4. Six squares: 64 against 6. Nine: 512 against 9. Twelve: 4,096 against 12. The ratio is 2ⁿ/n and it doubles with every square added, which is what an exponential saving looks like when both sides are counted rather than one described.

Twelve squares is where the brute force stops, and the shape of that ceiling is worth noticing because it is not about speed. A 3 × 4 grid holds 4,096 arrangements and a 3 × 5 holds 32,768, which a laptop would manage; 4 × 5 holds a million, which it would also manage; 5 × 5 holds thirty-three million, and 6 × 6 holds seventy thousand million million. The wall arrives between one row of the table and the next, and it arrives in the memo rather than in the clock — every arrangement has to be kept, because the search revisits them, so the limit is what fits in memory rather than what fits in an afternoon. That is the same failure mode knowing who wins and knowing what it is worth measures for value computations, arriving here two rows sooner than anybody would expect it to.

So the honest description of the situation is not that the theorem is faster. It is that on one side of a line four squares wide there is an answer and on the other side there is nothing at all, and the theorem is what moves the line to infinity.

It is worth saying what the brute force is actually doing, because the phrase “value every arrangement” hides the shape of the work. Each arrangement is a set of squares showing heads. Its value is a mex over everything one move can reach, and a move in the product game picks a head, picks a legal turn in the row game and a legal turn in the column game, and flips the whole rectangle of squares those two turns cross. So the branching is the product of the two games’ branchings, the positions are memoised so no arrangement is valued twice, and the count in the table is the size of that memo — which came out at exactly 2ⁿ every time.

That last detail is the one that makes the comparison fair. A brute force that skipped positions would be doing part of the theorem’s job by accident, and the numbers would be a comparison between the theorem and a weaker version of itself. Nothing was skipped: every arrangement of every grid was reached and valued.

The grid nobody could have solved #

The last row of that table is the point of the exercise.

An 8 × 8 grid — the size the theorem is normally illustrated at, and small enough to draw on a page — has 2⁶⁴ arrangements. That is 18,446,744,073,709,551,616, and there is no solver, no machine and no amount of patience that reaches it. It is the wheat-and-chessboard number, on a chessboard, which is a coincidence and a useful one for anybody trying to feel the size.

The theorem values every square of it with sixty-four multiplications.

That is the whole content of the rung and it is worth stating without decoration: a closed form does not make a hard computation easier, it makes an impossible one trivial, and the boundary between those is not gradual. There is no grid size at which the brute force becomes merely slow. It is fine at nine squares, marginal at twelve, and gone by twenty.

There is a version of that observation which is worth resisting, and it is the claim that the theorem “solves” the game. It does not solve the game; it values the positions. Knowing that a grid is worth 7 tells a player they should win and tells them nothing about which head to turn — that is a separate search, over the moves available, looking for one that reaches value 0. The code names the move is the essay about the cases where the value does hand over the move, and coin-turning games are unusually good at it, but the two questions are different and the ratio above is about only the first.

But the multiplication is not free either #

A comparison that counts one side’s work and ignores the other’s is the mistake knowing who wins and knowing what it is worth is about. So the theorem’s own arithmetic has to be counted too.

A nimber product is defined the way everything in this subject is defined — as the least value not forced:

a ⊗ b = mex { (a′ ⊗ b) ⊕ (a ⊗ b′) ⊕ (a′ ⊗ b′) : a′ < a, b′ < b }

which looks at a·b pairs, each of them another product. So the multiplication is a small search in its own right, and calling it “one operation” would be exactly the sleight of hand this essay exists to avoid.

Counted properly: the sixty-four squares of the 8 × 8 grid need only twenty-six different products, because the one-dimensional value sequences repeat values and the same product turns up in many squares. Computing all twenty-six by the defining rule looks at 470 pairs in total, the largest single product accounting for 64 of them.

Four hundred and seventy elementary steps against eighteen quintillion positions. The theorem is still ahead by 3.5 × 10¹⁶ to one after its own costs are charged to it, and the reason to do the accounting anyway is that this is the one place where it could conceivably have come out differently — a closed form defined by its own mex is not obviously cheaper than the thing it replaces, and here it is, by sixteen orders of magnitude.

Which half of the theorem is doing the work #

There is a second thing hiding in the brute-force check, and it is the more interesting half of the theorem.

The theorem as usually stated is about one head: the value at (x, y) is the product. But a table of one-head values is worth nothing unless a grid of several heads is the nim-sum of them, and that is a second claim.

On a 3 × 4 grid there are 4,096 arrangements. Twelve of them hold exactly one head. One holds none. The remaining 4,083 — 99.7 per cent — hold two or more, and every one of them is a test of the addition rather than of the product.

So the check that appears to be verifying the tartan theorem is, by count, almost entirely verifying that heads add. That is the right emphasis rather than an accident of the arithmetic: the product rule is the surprising half and the addition is the load-bearing half, because without it the per-square table answers questions about positions nobody plays.

The sum is the object is the general statement of why a decomposition is worth more than a value, and this is that argument arriving with a ratio attached: one part of the check tests the headline and three hundred and forty parts test the thing the headline needs.

The ratio also says something about how a check of this kind should be read when it passes. A verification that runs over 4,096 positions and reports no disagreement sounds like a strong result and could be a weak one, if 4,083 of those positions were trivially satisfied. Here the opposite holds: the twelve easy ones are the single heads, and the 4,083 are the ones where two independent claims have to combine correctly. So the check is strongest exactly where it is largest, which is not automatic and is worth knowing before quoting the number.

What twenty-six products means #

The count of distinct products is worth a moment, because it is the only number in this essay that is smaller than anybody would guess.

Sixty-four squares, and only twenty-six different products between them. The reason is that the one-dimensional value sequences are not injective — Turning Turtles gives a square its coordinate and Ruler gives the largest power of two dividing it, so the eight column values are 1, 2, 1, 4, 1, 2, 1, 8, with three ones and two twos among them. Any two squares sharing a row and sharing a column value need the same product.

That repetition is worth having and it is worth not over-reading. It is a saving of about a factor of two on an already negligible cost, so it changes nothing about the comparison. What it does show is that the theorem’s arithmetic is structured rather than arbitrary — the grid is not sixty-four unrelated multiplications but a small multiplication table applied many times, which is exactly what a field operation should look like when it turns up in a real problem.

It also means the cost of the theorem grows more slowly than the grid. Doubling the grid to 16 × 16 quadruples the squares and does not quadruple the distinct products, because the value sequences keep repeating. So the two sides of the comparison do not merely diverge; the gap widens faster than the square count.

Where the saving comes from #

It is worth being clear about which structural fact produces the exponent, because it is not the multiplication.

The saving is a decomposition saving. A grid of heads is a sum of independent one-head games; a sum’s value is the nim-sum of its parts; so the whole 2ⁿ-position problem reduces to n one-position problems and an exclusive-or. That much would be true of any game with the same decomposition property, and it is where the 2ⁿ/n comes from.

What the multiplication adds is that the n one-position problems are themselves free. Without the theorem, valuing the head at (5, 6) means solving the two-dimensional game from that position, which is its own search; with it, that value is a product of two numbers already in hand from the one-dimensional games. So the theorem removes a linear number of searches, not an exponential one.

Two savings, then, of very different sizes and very different characters, and the reason to separate them is that only one of them is special to this game. The exponential comes from the sum structure, which is the subject’s standard machinery. The linear comes from the tartan theorem, which is an unusual and specific fact about products of coin-turning games. It is the smaller of the two and it is the one that had to be discovered.

The check that could have failed #

One more thing is worth extracting, because it is the reason any of these numbers can be quoted.

The brute force in this measurement knows nothing about the theorem. It builds the product game’s moves from the two rulesets, walks every arrangement, and takes a mex. The theorem side computes the two one-dimensional sequences and multiplies. The two share no arithmetic and no code path, and they are compared on every arrangement of every grid that fits.

If the theorem were false — or, far more likely, if it were being applied with the wrong convention about which corner a move turns, or with the row and column games swapped — the comparison would produce a list of disagreeing squares rather than a saving. It produces an empty list, on 4,096 arrangements of two different 12-square grids and every smaller one, and the function refuses to return anything if it does not.

It is also worth knowing which mistakes such a check would not catch, since a green result is only as informative as the ways it could have gone red. It would not catch an error shared by both sides — a wrong reading of a ruleset’s legal turns feeds the brute force and the one-dimensional sequences alike, and both would be consistently wrong together. Guarding against that is what the one-dimensional decomposition check in the rung below is for, and it is why the two checks are worth keeping separate rather than merging into one sweep that reports a single number.

That is what makes the ratio a measurement rather than an estimate. The expensive side was actually run. A bound instead of an answer is the usual compromise when the expensive side cannot be run, and the point of stopping at twelve squares is that up to there it can.

What the ratio is not #

Two disclaimers, both of which the measurement makes rather than avoids.

The brute-force column counts positions valued, not seconds. A real solver would be slower per position than the theorem is per product by a further large factor, so the ratio understates the practical difference — and it understates it in a way that cannot be quantified without picking an implementation, which is why the count is in positions.

And the ratio at the 8 × 8 row is a projection rather than a measurement. Nothing here valued 2⁶⁴ arrangements; the number is 2⁶⁴ because a grid of n squares has that many, which is arithmetic rather than a claim. Every row above it was actually run both ways and agreed. That is the honest structure of the argument: the theorem was checked where checking is possible, the cost model was measured where measuring is possible, and the headline number is what those two extrapolate to at a size the theorem was built for and the check cannot reach.

What to take from it #

The number in the title is small on purpose. Four hundred and seventy is not an impressive quantity of computation; it is what a person could do by hand over an afternoon with a multiplication table beside them. That is the point.

Three things generalise past this game.

A closed form is worth measuring against the thing it replaces, in the same units. The tartan theorem is usually presented as a striking identity, and it is one, but “striking” is not a quantity. Positions valued against products computed is a quantity, and it comes out at 3.5 × 10¹⁶ to one after the closed form’s own arithmetic is charged against it. Nobody would have guessed that number, and the reason to compute it is that the closed form is defined by a mex and could plausibly have been expensive.

Count both savings separately. The decomposition is worth 2ⁿ/n and applies to any game that decomposes. The product identity is worth a further linear factor and is specific to this construction. Reporting them together makes the specific one look far more powerful than it is, and it is the specific one that took a theorem to find. Turning turtles is where the decomposition arrives in one dimension, and the exponential is already there before anybody multiplies anything.

Check the half that carries the weight. The measurement found that 99.7 per cent of the verification is testing the addition rather than the product. A check designed around the headline claim would have run twelve cases; the one that runs is three hundred and forty times larger, and it is larger in the direction that matters.

A period is a proof is the same shape in a different corner of the subject — a finite computation licensed by a lemma to speak about infinitely many cases. Here the lemma is the tartan theorem and the finite computation is 470 steps, and what it speaks about is a board somebody could put on a table.