The pairing the formula hides

No two heaps alike established Welter’s closed form: the Grundy value of coins on distinct squares is the exclusive-or of $\langle a \mid b \rangle = (a \oplus b) - 1$ over every pair of them, with the plain nim-sum of the squares added when the number of coins is odd. It closed by naming what a formula is not:

The rung above is the structure behind it: why a function of pairs should describe a game at all, which is Conway’s mating theory and is a construction rather than a formula.

The construction is a perfect matching of the coins, and once it is in hand the parity clause stops being a clause.

The picture the formula suggests #

The animating function is nought exactly when $a \oplus b = 1$ — when the two coins sit on adjacent squares $2k$ and $2k+1$. So the reading a reader takes from the formula is that a lost position is one whose coins have settled into such pairs, each pair contributing nothing.

It is sound. Every strictly mated position is a second-player win, on all 66 two-coin positions, all 210 four-coin ones and all 84 six-coin ones — and the soundness is not a coincidence of small boards but an identity, since each pair contributes a term of nought and the whole sum is therefore nought.

And it is not the whole story.

At two coins the strict mating is complete — the only lost positions are the mated ones. At four it accounts for 10 of the 18 second-player wins, and at six for 4 of 8. So the picture is right about the positions it describes and describes about half of them.

That is the ordinary fate of an intuition read off a formula’s special case. $\langle a \mid b \rangle = 0$ is one way for a sum of animating values to vanish and it is not the only way, and the formula never claimed otherwise.

Why a mated pair is worth nothing is arithmetic before it is a strategy. The animating function of a pair on $2k$ and $2k+1$ is $(2k \oplus (2k+1)) - 1 = 1 - 1 = 0$, because two squares differing only in their last bit exclusive-or to one. So a fully mated position has every term of the closed form equal to nought, its value is nought, and it is a second-player win — which is what the figure above measures on every even count.

What the picture then suggests is a pairing strategy: answer each slide inside the pair it was made in, keep the pairs mated, and walk the whole configuration down the strip until it is packed against the wall. That is a pairing argument of exactly the kind the strategy that is a symmetry is about, and it has the property those arguments always have — it names a winner and no move until the opponent has moved. Nothing on this page verifies that the answer is always available, and it is worth flagging as an argument the reader is being offered rather than a measurement: what is measured here is that mated positions are lost, not how to win them.

What makes the pairing unusual is that it is not a symmetry of anything. The coins are paired by their squares — by the last bit of a number — rather than by any reflection or rotation of the strip, so none of the geometric machinery this site has built for pairings applies, and the involution is on the numbering rather than on the board.

The pairs that cancel #

The construction allows what the picture forbids: pairs whose animating values are not nought, arranged so that they exclusive-or away.

Some perfect matching of the coins has its animating values exclusive-or to the position’s Grundy value, on every position measured — all 606 of them across five coin counts. That is not a fact about lost positions; it holds for every value, so the matching is a reading of the whole game rather than a certificate for half of it.

And it is usually the only one.

At three coins the matching is unique on all 120 positions; at four, on 160 of 210. So the mating of a position is a well-defined object most of the time, and the exceptions are positions where several pairings happen to agree.

The falling share is worth reading as arithmetic rather than as a weakening. Four coins offer three matchings and six offer fifteen, so the chance that two of them land on the same value rises steeply with nothing about the game changing. What would be informative is the count of working matchings staying at one as the coin count grows — it does not — or the positions with several agreeing being a recognisable class, which is a question this sweep can ask and has not.

That is what makes the construction a construction rather than an existence claim. A reader handed a position can find its pairing, and on most positions there is nothing to choose.

The odd coin is the odd coin #

The rung below found the parity clause surprising, and said so:

The parity clause is the surprise: a rule about pairs that only composes when there is an even number of things to pair.

Read as a matching there is no clause and no surprise. An odd number of coins cannot be paired. One is left over, it contributes its own square rather than an animating value, and that is the whole of the correction.

A matching of $n-1$ coins together with the left-over coin’s square gives the Grundy value on all 120 three-coin positions and all 126 five-coin ones. Five coins cannot be paired and neither can three, so the correction is not an extra rule the odd case needs — it is what is left when the pairing has done as much as a pairing can. At three coins the choice of which coin to leave out is forced on every position.

So the closed form’s extra nim-sum term and the matching’s left-over coin are the same fact in two notations. The formula sums over all pairs, which loses the information about which pairing, and it has to put the odd coin’s contribution back by hand because summing over all pairs has no way to leave one out.

The eight positions the picture misses #

The eight four-coin second-player wins that are not strictly mated are worth looking at as a class, because they are what the cancelling matching is for.

They are lost positions whose coins cannot be split into adjacent pairs at all — so no answering strategy of the kind above is available, and a player holding one has to win some other way. The matching that gives their value pairs coins whose animating values are not nought and which cancel: two pairs each worth some $v \neq 0$, exclusive-oring to nought.

That is a different kind of certificate and it is worth naming as one. The strict mating says answer inside the pair and the pairs survive. The cancelling matching says only that a bookkeeping identity holds, and it does not obviously correspond to any strategy — nothing in it tells a player which coin to slide. So the construction is complete as an account of the value and is not, on those eight, an account of how to win.

Whether it can be made into one is the sort of question this ladder should ask next, and it has a sharp form: on a position whose matching cancels rather than mates, does answering inside the pair preserve the cancellation? If it does, the pairing is a strategy everywhere and the strict mating was only its easiest case. If it does not, then Welter’s game has two quite different reasons for a position to be lost, and the formula has been hiding the difference.

What a formula loses #

The relationship between the two is worth stating exactly, because the formula is the construction summed up is nearly right and is not quite what happens.

The closed form exclusive-ors $\langle a \mid b \rangle$ over all $\binom{n}{2}$ pairs. A matching uses $n/2$ of them. At four coins that is six terms against two, and the six-term sum is not any of the three two-term sums — it is a different expression that happens to have the same value.

So the formula is not the construction with the choice summed away; it is a second exact expression, arrived at independently, which needs no choice and therefore needs a parity patch. The construction needs a choice and therefore needs no patch. Each pays for what the other gets free.

That is the answer to the rung below’s question. A function of pairs describes the game because a pairing of the coins does, and the closed form is what survives when the pairing is refused. Nim and the nim-sum is the standing contrast: there the decomposition is into single heaps and the formula is the decomposition, with nothing lost and nothing to choose. Welter’s clause — no two coins on one square — is exactly what stops the coins being independent, and what replaces independence is a pairing rather than a partition into singletons.

What this says about the clause #

Welter’s game is Nim with one clause added — no two coins on the same square — and the two rungs of this anchor now say something fairly precise about what that clause costs.

It destroys the partition. No two heaps alike measured that directly: over the 45 two-coin positions inside the first ten squares the nim-sum is the Grundy value on none of them, and over the 120 three-coin positions on none either. Two heaps that may not be equal are not two independent heaps, and the whole apparatus Sprague–Grundy provides for adding independent components stops applying.

And it replaces the partition with a pairing. That is the finding of this rung, and it is a weaker structure in a specific way. A partition into singletons is canonical — a position is its heaps, there is nothing to choose, and the decomposition is visible on the board. A pairing has to be chosen, it is unique on most positions and not all, and nothing about the board displays it.

So the cost of the clause is one level of structure. The game still decomposes; what it decomposes into are pairs rather than parts, and the pairs are a fact about the position rather than a feature of it. The move that gives counters back is the standing contrast on this anchor — a clause added to Nim that changes nothing at all — and the difference between the two is exactly whether the clause can make two components interact.

And the interaction is the point. Two coins may not share a square, which is a constraint between them, so any account of the game has to carry information about pairs of coins. That is not a discovery about Welter’s game; it is what the rule says. What is a discovery is that pairs are enough — that no term involving three coins at once is ever needed, at any coin count measured. A rule constraining pairs might have produced a game needing triples to describe, and it does not.

What the solver computed, and how #

Every position of two to six coins on distinct squares below a cap chosen so each sweep is affordable — 66, 120, 210, 126 and 84 positions. Each is evaluated by the ordinary recursion: a move slides one coin to any lower empty square, and the Grundy value is the mex over the results, memoised on the sorted square list.

The strict mating is tested by repeatedly taking the lowest coin and looking for its partner at the square differing in the last bit; a position is strictly mated when that succeeds all the way down.

The matchings are enumerated in full — one for two coins, three for four, fifteen for six — and for odd counts every choice of left-out coin is tried against every matching of the rest, so a five-coin position has five times three. Each is scored by exclusive-oring the animating values of its pairs, plus the left-over coin’s square where there is one, and compared against the value from the recursion.

Three things are asserted rather than reported. Some matching must give the value on every position, since that is the construction the page reports. No strictly mated position may be a first-player win, since the sufficiency is the first finding. And some second-player win must fail to be strictly mated, or the strict reading is complete and there is nothing for the cancelling version to be needed for.

Where the model stops #

Six coins and a cap of nine or ten squares. The number of matchings grows as the double factorial — 1, 3, 15, 105 — so eight coins is 105 matchings on many more positions, and the uniqueness figure in particular would be worth having there: the share of positions with a unique matching falls from 100 per cent at three coins to 29 at six, and where it goes is not visible from four points.

And the construction is exhibited rather than derived. The page shows that a matching exists on every position measured and that it is usually unique; it does not show which matching, as a rule, nor why one exists. Conway’s own account supplies that and this site does not quote it — no two heaps alike evaluates the formula rather than repeating it, and the same discipline applies here, which means the theorem behind the existence is outside what has been checked.

Normal play throughout, and the whole apparatus depends on it: the coins run out of moves when they are packed against the wall, and it is the last player to slide who wins.

And the figures cannot show a matching. Six tables of counts describe a pairing, and the object — a strip of squares with coins on it and arcs joining the paired ones — is a picture, one per position. That drawing would make the strict mating obvious in a glance and would make the cancelling case obvious too, since the arcs would visibly not join adjacent squares. It is one figure per position and this page counts across six hundred of them.

Where the ladder goes next #

The welter anchor has two rungs: the closed form with its parity condition, and now the pairing behind it.

The rung above is the rule for choosing the matching. On most positions there is exactly one, so the mating is a function from positions to pairings and nothing here computes it except by trying all of them. A rule would be a genuine strategy: told which coins are paired, a player answers a slide inside one pair with a slide inside the same pair, which is the argument the strict mating makes and which the cancelling matching ought to support in some modified form. Finding that rule means asking what the unique matching has in common across positions — whether it pairs coins agreeing in their high bits, or coins whose squares are close, or something the squares do not show — and the population is already built.

Two neighbours are worth the trip. The move that gives counters back is the other essay here about a clause added to Nim, and the contrast is now sharper than the rung below could make it: there the clause changes nothing and the decomposition survives intact, and here it replaces a partition into singletons with a pairing. And a row of coins is already a sum is the other game on this site whose position is coins on a strip, where the decomposition the picture suggests turns out to be the right one — which is exactly what does not happen here.