Proving a loss means answering everything

The two quantifiers in a game’s prefix are not symmetric, and the asymmetry is in the rules rather than in the notation. To establish that the player to move wins, one move suffices: name it, and show the position it leads to is a loss for the other. To establish that the player to move loses, every move has to be answered, because a single unanswered move is a win.

So the two verdicts are certified by objects of different shapes. One is a path with branching only at the opponent’s turns; the other branches at every turn.

Small, and always in the same direction #

The measured ratios run from 1.07 to 2.31. A loss is dearer everywhere and it is dearer by a small constant.

That is the finding, and it is worth saying why it is not obvious. Nothing in the definition bounds the ratio. A loss’s proof is a sum over the options and a win’s is a minimum over them, and a sum over six things is not ordinarily within a factor of two and a bit of the smallest of them. The ratio could have been the branching factor; it could have grown with the board; it could have been different in kind on the partizan games and the impartial one. It is none of those.

Nor is a small constant the only possible answer. The shape that does not occur here is the one a puzzle has. Asked whether a formula is satisfiable, somebody who says yes hands over an assignment and somebody who says no hands over nothing at all — there is no short object establishing that every assignment fails, and the absence of one is why nobody expects the complement of NP to be NP. In a game the two directions are the same kind of object, differing by a constant, and that fact has a consequence the earlier essay states: the class a game question sits in is closed under complement, so a short certificate for one direction would collapse a hierarchy.

The measurement above is that closure made concrete on boards. Both sides of every verdict here are writable, and neither is writable cheaply.

What the terminal positions do #

There is one way to get the comparison backwards and it is the natural way, so it is drawn rather than avoided.

Ninety-four of the 493 turns on a three-by-four Domineering board have no move in them. Each is a loss under the normal-play convention, and each is proved by exhibiting the position and observing that there is nothing to play — a proof of one node.

Counted in, they drag the mean cost of a loss from 6.0 to 3.9 on that board, and on the three-by-three board the same arithmetic takes it from 5.0 to 1.4 — below the 2.2 a win costs there. A table built that way reports that losses are cheaper to prove than wins, which is a true statement about a population and a false statement about the asymmetry.

The trouble is that a terminal position is not a claim about play. It is a claim about the convention: the recursion has ended, and what establishes the verdict is the rule rather than any argument. Including it measures how a game ends and calls the result a fact about how a verdict is proved. So the comparison is made over turns that have a move, and the number it reverses to is printed beside it.

Thirty-eight of the ninety-two turns on the three-by-three board have no move, which is why the reversal is so violent there: the terminal positions are more than a third of the population and every one of them is a loss costing one. The larger board dilutes them to under a fifth and the reversal does not quite happen. So the size of the mistake depends on the board rather than on anything about proofs, which is the clearest sign that the wrong population is being measured.

The hazard is an old one in this subject and it has bitten here before. An average over a population that silently contains two kinds of thing reports a number about neither: the long-chain rule counted over every endgame is right on the positions it was really about and has counterexamples everywhere else, and the count that mixes them says nothing about either. The repair is the same in both cases — name the population, print the other number beside it, and let a reader see which is being claimed.

The obvious explanation, and why it fails #

If a loss answers every option and a win answers one, the cost of a loss ought to be the branching times the cost of a win. That prediction is arithmetic and it is checkable.

It is too high everywhere, which is the first thing, and it is too high by wildly different factors, which is the more interesting thing. On the partizan boards it misses by between nothing at all and twenty per cent — Domineering on three rows by four predicts 6.3 against a measured 6.0. On Nim it misses by a factor of 2.8 and 3.9.

The reason is that the prediction multiplies a branching by an average, and the positions a loser has to answer for are not average positions. They are the positions reached by one move from a position the mover loses, so they are one move smaller, and they are positions the opponent wins — which is the cheap verdict. A loss’s proof is a sum of six cheap things rather than six typical ones.

Where the games differ is in how much smaller one move smaller is. Taking a counter off a Nim heap can take the position most of the way to nothing; there is a move from heaps of 3, 4 and 5 to heaps of 3, 4 and nothing, and the proof on the other side of it is tiny. A Domineering move covers two squares of twelve and the position after it is very nearly the position before it. So Nim’s losing turns look expensive and are not, and Domineering’s are exactly as expensive as they look.

That is a difference between the games that no count of positions or moves would show. It is about how fast a move shrinks the object, and it is visible only when the cost of a proof is being tracked rather than the size of a tree.

One more thing follows from it, and it bears on how the two verdicts should be thought of at all. If a loss’s proof were the branching times a win’s, then the cost of a proof would be exponential in its depth and the two verdicts would separate further with every move of the game. They do not separate: the ratio on Domineering is 1.33 on two rows by three, 2.31 on three by three and 2.15 on three by four, which is not a trend. Whatever the ratio is a function of, it is not the size of the board.

That is worth holding against the doubling at every universal quantifier. Both are true, and they are true of different objects. A strategy — an answer to every line, held in advance — doubles with each of the opponent’s turns. A proof of a verdict does not, because it may appeal to a position once and re-use it, and the positions it appeals to are shared between the two verdicts. The first is a tree and the second is a subgraph, and the whole of the difference between an exponential and a small constant is in that word.

The two extremes of the ratio #

The widest and the narrowest gaps are both worth a look, because they fail in opposite ways.

The Nim figure holds a number the means conceal: the largest proof of a loss is 597 nodes and the largest proof of a win is 598. The two extremes are within one node of each other.

That is not a coincidence and it is the sharpest form of the symmetry. The most expensive win on the board is a win from a position whose winning move leads to the most expensive loss there is, so its proof is that loss’s proof plus one node for the move. The two objects are nested. Whatever the means do, the worst cases of the two verdicts on this board are the same object seen from two sides.

Clobber is the other extreme: twenty-seven against six. The reason is the one the earlier essay found on the same board — not one of its 114 turns decides anything, so a win is never a matter of finding the right move, and the cheapest winning option is always available immediately. The loss, meanwhile, still has to answer everything.

A board where nothing decides is therefore a board where the two verdicts are least alike in cost, which is the opposite of what one would guess. If no choice matters, a win should be trivial to certify and it is; a loss still needs the full accounting, because nothing matters is itself a claim about every option.

What this says about the prefix #

The asymmetry has an exact counterpart in the quantifier arithmetic, and it is the same arithmetic twelve turns and three prices is built on.

A strategy’s size is a sum of $2^k$ over the chooser’s decisions, with $k$ counting the opponent’s turns before each. The chooser’s own turns contribute nothing to the exponent and the opponent’s contribute everything, which is the same statement as one option suffices for a win and all of them for a loss — a chooser’s turn is a minimum and an opponent’s turn is a product.

So the prefix arithmetic predicts the shape of the asymmetry and says nothing about its size, because it assumes every turn offers two options and every line runs to the end. A board offers between one and a dozen options a turn, and its lines end at different depths; those two facts are what turn a clean exponential into a factor of 1.07 on one strip and 2.31 on one board.

Which positions are dear #

Averages over a population hide where the cost sits, and on these boards it sits in a few places.

The distribution of proof sizes is extremely uneven. On Nim heaps of 3, 4 and 5 the mean win costs 68.3 nodes and the dearest costs 598 — nearly nine times the mean — and most positions are far below it. The reason is that a proof’s cost is roughly the size of the subgraph below the position, and a Nim position two moves from the end has almost no subgraph. So the expensive proofs are concentrated near the start and the cheap ones near the end, and a population weighted by position count is weighted towards the end.

This has a consequence for how the ratio should be read. It is a ratio of means over a population dominated by small positions, so it is largely a statement about endgames. A ratio taken over openings alone would be a different number, and on Nim heaps of 3, 4 and 5, whose opening proof is 598 nodes against a mean of 68.3, the opening is where the two verdicts come closest rather than where they separate.

None of that undermines the finding; it narrows it. What is established is that a loss is dearer than a win by a factor that stays small over every position of these boards, endgames included. What is not established is that any particular position’s two verdicts stand in that ratio, and the Clobber board is the standing reminder that they need not.

It also says which games would be worth looking at next. A game whose moves shrink the position a great deal — Nim, where a move can empty a heap — has cheap losing options and a ratio well below its branching. A game whose moves shrink it barely at all — Domineering, where a move covers two squares of twelve — has a ratio that tracks its branching almost exactly. Nim is easy in the sense that a formula answers it, and it turns out to be easy in this quite separate sense as well, for a reason that has nothing to do with the formula: its moves are large.

The convention this is computed under #

Normal play throughout: the player who cannot move loses. The verdicts are the ordinary who-wins verdicts, computed by the same recursion the other essays here use, and the proof sizes are computed over the position graph rather than over the tree — so a position reached by several routes contributes one node to the proofs that need it, not one per route.

That last choice is the one worth stating plainly, because it is generous and it is generous to both verdicts equally. The tree and the graph prices the difference between them, and it is enormous. Sizing a proof over the graph means counting a proof as the set of positions it appeals to rather than as a tree with repetitions, which is what somebody checking the proof would actually store. A proof counted as a tree would be larger on both sides and the ratio would move, and nothing here measures by how much.

A proof here is also the smallest one, not the one a search finds. At a winning turn the recursion takes the cheapest winning option rather than the first, which is a minimum over the options and needs every one of them evaluated. So the object is small and the work of identifying it is not, which is the same gap a strategy and a solution are separated by.

What the measurement cannot reach #

Four games and eight positions. The ratio being a small constant is a statement about these boards. The construction gives a reason to expect it to hold — both verdicts recurse over the same graph and neither can escape it — and no reason at all to be certain, and the Nim rows are a warning that families differ by factors of three in the quantity that drives it.

Nothing here is about a player. A proof of a loss is what somebody would have to be handed to be convinced; it is not what a losing player does, which is to play on and hope. The two have been confused often enough in this subject to be worth separating: a theorem can name a winner and no move, and a proof can certify a loss without being anything a person would sit down with.

And the proofs of the terminal positions are a convention rather than a measurement. One node for a position with no move is the cheapest defensible number and it could be nought — the position is the proof — or two, counting the observation as well as the position. Nothing above depends on which, because the reversal is reported rather than relied on, but a table that quoted the terminal means as its headline would depend on it entirely.

Still open: what a bad proof costs #

Every number here is the smallest proof there is. A player, a program or a textbook produces something much worse, and the gap has not been measured.

The measurement that would begin to settle it is the proof a depth-first search produces: the first winning option it finds rather than the cheapest, with whatever subtree that option drags in. On a board where the options are ordered badly the difference could be large, and the order the moves are tried in has already shown what ordering is worth to a search on the same family — 1,125 positions expanded against 30,202, from nothing but the order.

Whether the same ratio applies to the object rather than to the work is a different question with the same instruments, and it is the one that would say whether the small constant above is a fact about games or a fact about taking minima.