Concept

Proof — where it appears

An argument that a statement holds for every case, as against a sweep showing it holds for the cases tried. On this site the two are kept apart deliberately, because most of the regularities here are measured and a few of them turn out to be theorems.

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

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
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
Four moves, three arguments. Every first move in the sum, with what answers it and how many cases of each the census holds.

The case that was supposed to be hard

The mex rule for the mirror construction was to be proved by induction, and the step flagged as needing care was the one where an option is incomparable with the nimber. There is no induction: the argument is four lines, and incomparability is what makes two thirds of the cases go through — because a fuzzy sum is a first-player win and the first player is the opponent.

sums · Negation
Three orders, one of them right. The holder's rank above the crossover under three different orderings of the options.

Which top is the top

The crossover law's proof rests on the walls above the crossover being governed by the top two options, and the check was never run. Run on 23,586 heights it holds exactly — but only when the options are ranked by mean value. Ranked by the temperatures the law is stated in, it fails on a fifth of them.

temperature · Sente
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
6 turns in strict alternation, priced. One quantifier prefix taken apart into its blocks, with the size of a winning strategy computed a term at a time. A choice made after k of the opponent's turns has to be written down once for each of the 2^k lines the opponent can produce, so the total depends on where the opponent's turns sit and not merely on how many there are.

Twelve turns, and three different prices

The earlier essay prices a universal quantifier at a doubling and leaves it there. Twelve turns with six of them the opponent's cost 6, 63 or 384 decisions to write down, depending on nothing but the order the turns come in — and the cheap arrangements are cheap for only one of the two players. What a claim costs is the number of times the choosing changes hands.

complexity · Alternation
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
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
The reversing move is the follower's. For each follower under which some gift horse escapes domination, the number of escapes, how many are reversed by Right's move inside the follower, and how many by a Right move in the base part. The follower's move reverses every one.

The follower does the reversing

The gift-horse theorem for the ordinal sum needs two cases, and the second — the added option is reversible — was counted and not described. Recorded move by move, the reversing answer is always Right's move inside the follower: on all 410 escapes under five followers, and on every one of the 2,628 gift horses under every follower that gives Right a move at all. The case split is by follower, not by horse.

sums · Ordinal sum
What survived, and what did not. The gift-horse theorem, the two-case proof and the one-line description of the reversal case, each scored on the day-three sweep and its mirror and on the day-four sweep and its mirror.

The split slips one day deeper

The reversal case of the gift-horse theorem was described in one line — the follower's own move reverses every gift horse, whenever the follower has one — and tested only where it was found. In the mirror it holds exactly, with 1 and −1 trading places. One day deeper it fails: under ↑ and ½, three gift horses on built day-four bases are not reversed by the follower's move. All three are dominated, so the theorem stands; the clean split by follower does not.

sums · Ordinal sum
Even rows always reward the move. For four coin sets and rows of one to seven coins, the number of rows in which the player to move does at least as well as when the opponent moves first. Every even column is full.

Even rows always reward the move

Milnor's mean-value theory needs an incentive to move — the player to move must do at least as well as if the opponent moved first. On a coin row with an even number of coins that is not a hypothesis but a theorem: the first player can collect one whole parity class of coins, and one of the two classes holds at least half the total. So the condition excludes no even row whatever the coins, the class the earlier table called 'incentive at the top' was every row of four, and the hereditary condition is a condition on odd intervals alone.

applied · Scoring

Named alongside it

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

EnumerationInductionExhaustive searchCounterexampleCanonical formClosed formDisjunctive sumIntegerNormal playPartizanStrategyValue

All concepts