Concept

Induction — where it appears

Proving a claim about a position from the same claim about its options, which is available exactly because no play runs for ever. The quantity it descends on need not be a count: for one game on this site it is an ordinal, and no bound comes out of it.

Named by 20 essays across 8 fields — each of them below, with the objects they name alongside it.

Poker Nim from 3, 5, 7, with reserves of 4 and 4. Nim with one extra kind of move: a player may put any number of counters back onto a heap from a private reserve. It looks as though a losing player could stall for ever. They cannot, and the winner is decided by exactly the same nim-sum as ordinary Nim — checked here over every position within a stated range rather than argued.

The condition the recursion rests on

Not that the moves run out, and not that the options are few. Poker Nim's heaps can grow without bound and it ends; the game called `on` has one option and never does. What every value on this site needs is that no infinite run of moves exists — and there are three separate ways to fail it.

limits · Termination
Subtraction of 1, 3, 4 — and the window that proves the period. The Grundy values of a subtraction game, with the window that certifies the period marked. Everything after the window follows from it by induction, because a value is a mex over values at most one move back — so a finite check settles the whole infinite sequence, and the thousands of further values computed here agree with a claim that was already proved.

Four values, and the sequence is settled for ever

The Grundy values of a subtraction game repeat with period 7, and proving it needs a window of exactly four of them — one for each size of move the game allows. Everything past the window follows by induction. A finite computation has settled a claim about every heap there will ever be.

complexity · Periodicity
Hydras, and how long each takes to kill. Six small hydras with the ordinal the termination proof assigns to each and the exact number of chops it takes to finish it. Two of them are not finished here: the fight is guaranteed to end and the machine runs out of memory long before it does, which is the gap between a termination proof and a bound.

It ends, and nothing says when

The recursion this site runs needs every line of play to reach a position with no moves, and the condition is usually met by an obvious decreasing quantity. The hydra meets it with no such quantity anywhere: the tree grows at nearly every step and the fight ends regardless, because the only thing that decreases is an ordinal. A four-node hydra dies in twenty chops; one level deeper and 279 chops reach forty thousand nodes with no end in sight.

limits · Termination
Every heap up to 40, won or lost. Heap sizes with the outcome for the player who moves first. The lost ones are shaded; they are exactly the Fibonacci numbers, which is a fact about a game with one heap, no board and no geometry in it anywhere.

The heap is not the position

Fibonacci Nim bounds a move by twice the previous move, which puts the state outside the board: a heap of six with a cap of two and a heap of six with a cap of five are different games. So there is nothing to add and no Grundy value to compute — and the game is completely solved anyway. The opener loses on exactly the nine Fibonacci numbers up to 120, and the smallest term of the Zeckendorf numeral is a winning move in all 110 winnable heaps.

impartial · Fibonacci nim
Two ways to be certain and ignorant at once. Ten positions from two games that both terminate for reasons no bound comes out of. Sylver Coinage's proof counts something that goes down and can be counted; the hydra's counts an ordinal, which cannot, and the last column shows what that difference is worth.

Two ways to end with no bound

Sylver Coinage and the hydra are both guaranteed to finish and neither will say when. The difference is that one of them carries its own bound: every move in Sylver removes at least one gap, the gaps can be counted in a moment, and over ten openings the longest play uses every single one. The hydra has no decreasing quantity a solver can hold — three hydras of five nodes each take seven chops, twenty-one, and a number past two hundred and seventy-nine that this machine never reaches.

limits · Termination
How old a sum is. Every unordered pair of the twenty-two values born by day two, with nought dropped because adding it settles nothing — 231 sums. The birthday of each sum was read off its own canonical form and compared with the sum of the two parts' birthdays, which is the bound. The bound holds everywhere and is attained 163 times.

The birthday of a sum

Two values born by days m and n have a sum born by day m + n at the latest, which is the bound that stops a board made of many small parts from being unboundedly complicated. Over 231 pairs of day-two values the bound holds every time and is exact 163 times — and every pair it misses by three days or more has a sum that is a number or a nimber, so the slack is not noise but a measure of how much cancelled.

values · Numbers
Running products, and where to stop. Six Maundy Cakes with the prime factors of the longer side, the running products those primes make, and the value the sum of them gives.

The short side only says how many

The rung below settled which cut to make in a Maundy Cake and left the value open. With the cut settled the recursion is a walk, the walk unrolls, and what it unrolls into is the running products of the long side's prime factors, largest first. The short side never enters the products at all — it decides how many of them there are and nothing else, so sixty-two different short sides give one value.

positions · Cutcake
Five premises, and the step. The claims an induction would need, with what checks each. The last row is the step and nothing here checks it.

The premises an induction would need

The rung below settled by a grouping test that a position's crossover depends on its own temperature and its answer's and on nothing below them, and asked for the induction. The four paragraphs are not written here; the checking they would rest on is. The law holds at five levels, survives translation, heating and cooling — and none of that is the step.

temperature · Sente
Term by term. Every cut of one long side, with its value written as running products beside the terms of the largest-prime cut.

The short side is not in the lemma

The closed form for a two-sided Maundy Cake rested on one unproved statement: that no divisor beats the largest prime. Written out, that statement never mentions the short side — it is an inequality between a multiset of primes and a term count — and once it is stated that way it has a two-line proof, term by term. The ladder ends in a theorem rather than a grid.

positions · Cutcake
Two statements, two routes. The two measured identities the rung below left unproved, with the argument each was expected to need.

One proof, and one wrong lemma

Two measured identities were left for a proof: the move rule by induction, the gap condition from the reply bound. The induction is exact on 31,731 heaps at eight factors. The reply bound holds at c = 2 and on one index pair in twenty-seven at c = 3 — and the inequality that does the work is a third one nobody proposed.

impartial · Fibonacci nim
The two proofs, beside each other. Maundy Cake's rule was proved by restating its lemma so the short side vanished into a multiset of primes and a term count. Cutcake's rule takes the same five steps, with the multiset replaced by a binary length — one integer instead of a multiset — and the closing argument correspondingly shorter. The one line where they differ is which cut a reader would guess.

The obvious cut is the wrong one

Maundy Cake's rule was proved by restating its lemma so the short side vanished. Cutcake's collapses the same way — into a binary length instead of a multiset of primes — but the cut the argument needs is not the one the ladder predicted. Halving is wrong on a third of all cakes, and the smallest counterexample is six squares by two.

positions · Cutcake
Five kinds of empty square. Every empty square in a hopless Toads and Frogs strip falls into one of five kinds, and the value follows from which. Three of them are free moves for one player or the other, one of them is where a position stops being a number, and one is a wall that splits the strip into independent pieces.

The square that cannot be halved

Every number in hopless Toads and Frogs is a whole number, which the rung below measured on seven thousand strips and could not explain. The reason is that every empty square is either one player's alone or split evenly between them — except one, and that one is where the numbers stop.

positions · Toads and Frogs
Two ways to be certain and ignorant at once. Ten positions from two games that both terminate for reasons no bound comes out of. Sylver Coinage's proof counts something that goes down and can be counted; the hydra's counts an ordinal, which cannot, and the last column shows what that difference is worth.

Which games end at which level

Between a game that ends within a computable bound and one that ends with no bound at all there are levels, each corresponding to a strength of induction. This site's games sit at three of them, and which level a game is at is decided by exhibiting its termination measure and checking that every move lowers it.

limits · Termination
The condition has to hold underneath, not on top. Pairs of coin rows sorted by where the incentive condition holds, with Milnor's bound checked on each pair. Rows that satisfy the condition at every subposition never break the bound. Rows that satisfy it only at the top break it on a counted fraction — and a reader who tested the row rather than the row's insides would have called those safe. The distinction is invisible from the position and decides whether the theorem applies to it.

A hypothesis has to hold all the way down

Milnor's bound is proved by induction over the play, so the condition it needs has to hold at every position the play can reach. Checked on the row instead, ninety-two pairs pass the test and twenty-four of them break the bound. Checked at every subposition, twenty-eight pairs pass and none breaks it.

applied · Scoring
How long a win takes, against how long the argument allows. Ordinary impartial games with the size of their position graphs, the number of rounds the backward labelling takes, and the number of moves the longest win actually lasts. The round a position settles in is the length of the play from it, which is computed here a second way so the two must agree. The rounds are a handful and the positions are many, which is the gap Zermelo's 1913 paper is about — his question was how many moves a forced win needs, and the answer he could prove was the size of the whole graph.

The paper was about how long

Zermelo's 1913 paper is remembered for a theorem it proves in passing. The question it actually asks is how many moves a forced win takes, the answer it can prove is the size of the whole position graph, and the round counter in the procedure is the real answer — a quantity nobody named for another forty years.

history · Determinacy
Two solutions to one set of equations. The winning condition written as a single predicate and solved twice: once as the least solution of its own equations and once as the greatest. The least says Left can force a win; the greatest says Left cannot be forced to lose, which admits the positions where Left can keep the game going for ever. On a graph with no cycle in it the two coincide and the equations determine an answer. Where they differ, the difference is exactly the set the backward propagation never reaches — so a draw is not a leftover of the algorithm, it is the equations failing to have one answer.

The gap between two answers

A draw is usually described as what the backward labelling never reached, which makes it sound like a shortfall of the algorithm. Written as one predicate the winning condition is an equation, the equation is monotone, and it has a least solution and a greatest one — and the set the two disagree about is exactly the drawn set, on every game checked.

history · Determinacy
A game every play of which ends, and no round settles. A game whose first move chooses how long the game will be, cut off at several sizes. Every play of it is finite and no position is drawn, so the fourth outcome class has nothing to do with what goes wrong. What goes wrong is the round counter: the opening is a loss, a loss settles only when the last of its options is known, and there is no last option. Cut the game off larger and the round grows, so no number in the column is the answer for the untruncated game — and the induction that labels it has to run past every finite stage.

Every play ends and no round settles

Take the finiteness hypothesis away carefully — not by adding a cycle, which has already been priced twice, but by adding infinitely many positions to a game every play of which still ends. Nothing is drawn, every line finishes, and the round the opening settles in grows with every cut: two, four, six, eight, twelve, sixteen, and no number in the column is the answer.

history · Determinacy
A win is proved by one move and a loss by all of them. The smallest proof of each position's verdict, averaged by verdict. At a node the mover wins the proof takes the cheapest single option; at a node the mover loses it has to answer every option, which is the existential and universal quantifiers of the prefix showing up as two different objects.

Proving a loss means answering everything

A win is established by one move and a loss by every move, so the two verdicts are certified by objects of different shapes. Measured over every position of four games, a loss costs between 1.07 and 2.31 times a win — a small constant, never an exponential. The obvious explanation is the branching and it is wrong: Nim answers six options at a losing turn and pays 2.18, not six.

complexity · Alternation
Bouton's argument, indexed by a value. Bouton's two closure properties stated for every Grundy value rather than for nought alone: no move stays inside a value class, and every class above a value can reach it. Checked on each game and each value in range.

The picture Bouton's proof leaves behind

His argument is two closure properties of one set, and the Sprague–Grundy theorem is the same two sentences with nought replaced by a variable — checked here on five games and every value in range, with no move staying inside a class and no class failing to be reachable from above. What the argument also leaves behind is a picture in which the values descend, and that is false: 99 of 444 moves here raise a value, and none of them is in Nim.

history · Bouton
Lasker's Nim in sixteen cells. A four-by-four table. Each row and column is a residue mod 4 of one part of a split heap, with the residue of that part's Grundy value beside it; each cell is the residue mod 4 of the split's value, the nim-sum of the two parts. Every split of every heap to four hundred lands in the cell its residues name.

The proof is sixteen cells

Lasker's Nim has a four-clause formula that was checked on two thousand heaps and never proved. The proof fits in a four-by-four table: the last two bits of a split's value are fixed by the last two bits of its parts, so no split can land in its own heap's class — except at 3 mod 4, where it lands exactly on the one value the takes leave missing and pushes the answer up by one.

impartial · Lasker

Named alongside it

The objects these essays reach for when they reach for this one.

Exhaustive searchClosed formEnumerationProofTerminationBoundGrundy valueRecursionBackward inductionClosureDisjunctive sumInteger

All concepts