Impartial games

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.

Assumes: What the numerals knew · The family the Fibonacci numbers belong to

What the numerals knew found the family’s numeral systems carrying a condition the family’s recurrences do not predict: expand a heap greedily over the losing positions of the factor-cc game, and consecutive terms sit at least cc indices apart. At c=2c = 2 that is Zeckendorf’s non-adjacency and the losers are the Fibonacci numbers; at the other seven factors it is a new condition, measured and not derived.

It closed by saying the two open statements were unusually well posed:

The gap condition should follow from the reply bound in a few lines, and the move rule from an induction on the number of terms; both are statements this page has data for at eight factors and neither is stated as anything but a measurement.

One of the two goes through exactly as proposed. The other proves Fibonacci Nim and nothing else.

Two statements, two routes. The two measured identities the rung below left unproved, with the argument each was expected to need.
Fig. 1 The two identities and the route each was expected to take. The induction holds at every factor; the reply bound holds at c=1c = 1 and c=2c = 2 and collapses immediately after. The figure refuses to draw unless the induction is exact everywhere and both proposed routes to the gap condition fail somewhere, since the page needs one of each.

The one that works

The move rule says a player wins from a heap of nn with a cap of \ell exactly when the smallest term of nn’s greedy expansion is at most \ell. The winning move is to take that term.

The induction is on the number of terms, and its step is a single statement: after taking the smallest term tt, the heap that remains has a smallest term of its own, and that term is larger than ctc \cdot t — which is exactly the cap the opponent now faces.

The induction goes through. The move rule's induction step, checked on every heap with more than one term at each factor.
Fig. 2 The step, checked at every factor on every heap with more than one term. It holds on all 31,731 of them without exception. So the opponent inherits a position of the same kind with a cap too small to reach its smallest term, which is the losing side of the very rule being proved.

That is the whole argument. The base case is a heap that is a single term — a loser, where the mover with any cap below it can do nothing useful — and the step hands the opponent a position of the same shape one term shorter, with the cap too small.

The step is exact on 31,731 heaps across the eight factors and there is no exception at any of them. So the move rule stops being a measurement. The rung below’s table of states and agreements is now a check on an argument rather than the evidence for a claim, which is the promotion this rung was for.

Why the step is the whole content is worth one paragraph, because an induction that hides its difficulty in a checked step has not hidden much. The rule to prove is a biconditional: the mover wins exactly when the smallest term is within the cap. The forward half is the move — take that term — and the reverse half is that nothing else works, and both come out of the same statement. If the smallest term is within reach, taking it hands over a position whose smallest term is not; if it is not within reach, every move the mover can make takes fewer counters than the smallest term, which leaves a heap whose expansion has gained a term small enough for the opponent to take. The step is the first of those and the second is its mirror.

So the induction is genuinely one statement wide, which is what made the rung below expect it to work. What is worth noticing is that it works at every factor without modification — the statement mentions cc only in the bound ctc \cdot t, and the argument never asks how fast the losers grow. That is the property the other proof turns out to lack.

The one that does not

The gap condition was expected to fall out of the game’s own bound. After a player takes tt counters the opponent may take up to ctc \cdot t, so a gap of cc would follow if the next cc losers outran that — if Lk+c>cLkL_{k+c} > c \cdot L_k, the loser cc places up were beyond what the cap allows.

The reply bound proves c = 2 and stops. The inequality the proposed proof of the gap condition rests on, checked at every factor.
Fig. 3 That inequality checked at every factor. It holds at c=1c = 1 and c=2c = 2 and then collapses: one index pair in twenty-seven at c=3c = 3, one in sixty at c=8c = 8. The failures start immediately — at c=3c = 3 the fourth loser is 6 and three times the second is 6, so the very first pair the argument needs is already an equality rather than a strict inequality.

It is false. At c=3c = 3 it holds on one of twenty-seven index pairs; at c=8c = 8, one of sixty. The losers of the wider family grow far too slowly for the cap to outrun them, and the argument that establishes the gap condition for Fibonacci Nim establishes it for Fibonacci Nim.

The single pair that does hold at each factor is the first one, which is worth noting because it is how the failure stays hidden. A reader checking the argument on the smallest case sees it work; the second index pair is where it stops, and by c=8c = 8 it has stopped fifty-nine times out of sixty. The heap is not the position makes the same point about this game from the other end — the small cases of Fibonacci Nim are misleading about the state, and here they are misleading about the proof.

That is a specific and ordinary failure mode: an argument written where the numbers are the Fibonacci numbers, whose growth rate is the golden ratio, transplanted to a family whose members grow much more slowly. The family the Fibonacci numbers belong to is where that slowing was established from the other direction — the growth rate is the real root of xc=xc1+1x^{c} = x^{c-1} + 1, and it falls toward one as cc rises.

The obvious repair is the other natural route, and it fails in the same place.

The recurrence does not generalise. The generalised Fibonacci recurrence checked against the losers at each factor.
Fig. 4 The Fibonacci recurrence generalised the way the gap condition suggests — each loser the previous one plus the one cc places back. Exact at c=2c = 2, which is Fibonacci’s own recurrence, and wrong from the fourth loser onward at every larger factor. The two routes fail at the same factor and at nearly the same index.

The inequality that does the work

The greedy step needs something, and what it needs is neither of those.

Take the greedy expansion of nn and suppose it has just taken LkL_k. The remainder is nLkn - L_k, and because greedy took LkL_k rather than Lk+1L_{k+1}, that remainder is below Lk+1LkL_{k+1} - L_k. The next term is the largest loser at most the remainder. So the next term’s index is below kc+1k - c + 1 — which is the gap condition — as soon as

Lk+1LkLkc+1.L_{k+1} - L_k \leq L_{k-c+1}.

The increment bound holds everywhere. The inequality on consecutive losers that the greedy argument needs, checked at every factor and index.
Fig. 5 That inequality checked at every factor and every index over the losers to twenty thousand. It holds without exception, on all eight factors — the only one of the three candidates that does. It is a statement about the losers’ increments, where the two proposed routes were about their ratios and their recurrence.

It holds everywhere: every factor, every index, no exception.

The gap condition, in five lines. The derivation of the gap condition from the increment bound, step by step.
Fig. 6 The gap condition assembled from it. Five lines, of which four are arithmetic on what greedy means and one is the inequality above. The figure is the argument rather than a table of measurements, which is what this rung was asked for — and the honest reading is in its last line.

So the gap condition does have a short derivation, and it is five lines rather than a few, and it rests on a lemma nobody proposed.

The five lines are worth reading once more for what is doing the work. Four of them are restatements of what greedy means — it takes the largest loser it can, so the remainder is smaller than the step it declined — and one is the inequality. Nothing in the derivation mentions the cap, the reply bound, or the factor except through the index offset, which is why it survives the change of factor that killed the other two arguments. An argument that never consults the growth rate cannot be broken by the growth rate changing.

And the honest statement of what has been achieved is a reduction rather than a proof. The increment bound is itself measured — 285 index pairs across eight factors, no exception — and not derived. What this rung has done is replace one measured identity with a simpler and more local one: from the terms of a greedy expansion sit cc apart to consecutive losers differ by at most the loser cc places back. The second is a statement about two numbers rather than about an algorithm, and it is the thing a proof should now be attempted on.

Why the increments and not the ratios

The three candidate inequalities are worth setting beside each other, because which one works is the finding rather than an accident.

The reply bound is about a ratio: it asks whether the losers grow faster than the factor multiplies. That is a question about growth rate, and the family’s growth rate falls toward one as the factor rises, so the inequality gets harder exactly where the gap condition gets stronger. It was always going to fail in that direction.

The recurrence is about structure: it asks whether each loser is a fixed sum of earlier ones. It is not, past c=2c = 2, and the rung below already knew that from the other side — its recurrence-lag reading matched 2(c1)2(c-1) for four factors and then stopped.

The increment bound is about differences, and differences are what a greedy algorithm actually consults. Greedy never asks how fast the losers grow or what recurrence they satisfy; it asks how far it is from one loser to the next, because that is what bounds the remainder. The inequality that works is the one stated in the quantity the algorithm reads, and the two that fail are stated in quantities that describe the sequence from outside it.

That is a transferable reading rather than a fact about this family, and it is the same shape as the correction one anchor over: the short side is not in the lemma found a formula stated with a variable it did not depend on, and the way out was to write the statement in the terms its own proof would use.

It also explains why the failure was invisible at c=2c = 2. When the losers are the Fibonacci numbers, the ratio, the recurrence and the increments all say the same thing — Fk+1Fk=Fk1F_{k+1} - F_k = F_{k-1} is simultaneously an increment bound, a recurrence and a statement that the ratio tends to φ\varphi — so any of the three arguments works and there is nothing to choose between them. The three quantities come apart only in the family, and the family is where the rung below found the condition. The generalisation and the disambiguation arrived together, and the proposal was written before anybody had reason to notice they were three questions.

What this does to the anchor’s ledger

Three of the anchor’s four rungs are now measurements and one of them is an argument, and it is worth being exact about which is which, because proved is a word this site spends carefully.

The move rule is proved, modulo a step checked on 31,731 heaps. That is an induction with one measured input, and the input is a statement about single heaps rather than about the rule — so it is the kind of gap a reader can hold in their head, and it is much smaller than the gap the rung below had.

The gap condition is reduced, from a statement about greedy expansions to a statement about consecutive losers. Nothing about it is proved; what has changed is that the thing to prove is now local, is about two members of one sequence, and does not mention the algorithm at all.

And two candidate proofs are eliminated, which is the part that will not have to be done again. The reply bound and the generalised recurrence are the two arguments anybody meeting this problem would reach for, both are natural, both are correct at c=2c = 2, and both are now known to be dead. That is worth as much as the reduction: a ladder that records which routes fail is a ladder that does not re-walk them.

What has not moved is the family’s own arithmetic. The family the Fibonacci numbers belong to established the growth rates and the lags, and this page uses them only to explain why the reply bound fails. The gap condition and the growth rate are now known to be independent questions — the first has a five-line derivation from an increment bound and the second has a characteristic equation, and neither reaches the other.

What the solver computed, and how

For each factor cc from 1 to 8, the losing heap sizes are generated by the ordinary recursion — a heap is a loser when every legal move from it leads to a winner — up to twenty thousand counters, which gives between 15 and 68 of them.

The greedy expansion of a heap over those losers is the usual one: take the largest loser at most the heap, subtract, repeat. Every heap up to four thousand is expanded at every factor, which is where the induction step’s 31,731 cases come from — heaps with a single term are the base case and are excluded from the step.

The three candidate inequalities are then checked directly over the loser sequence, index by index, with the first failure recorded rather than only a count. The induction step is checked heap by heap: take the smallest term, expand what remains, and compare its smallest term against cc times the one just taken.

Four things are asserted rather than reported. The induction step must be exact at every factor, since it is the proof this page keeps. The increment bound must hold at every factor, since the repair rests on it. And both proposed routes must fail somewhere — a page written about a route failing needs it to fail, and a sweep in which either held everywhere would make three of these figures argue the opposite of their captions.

Where the model stops

Eight factors and twenty thousand counters. The increment bound is checked on 285 index pairs in total, which is not many, and it is the statement the whole repair now rests on. A ninth factor or a longer sequence could break it; nothing here proves it, and the page says so rather than calling the gap condition proved.

The move rule’s induction is a genuine proof and its step is a measurement. The induction is valid — base case, step, done — but the step itself is verified on 31,731 heaps rather than derived. So the move rule is in exactly the position the gap condition is in one level down: an argument whose one non-trivial input is checked and not proved. That is better than where the rung below left it and it is not a theorem.

Normal play throughout. The whole apparatus depends on the last player to move winning; the losers are the second-player wins under that convention and nothing here survives the misère version. The greedy expansion is over those losers, so a misère version of this family would have a different digit set and a different condition, and whether it has one at all is not a question this anchor has asked.

And the figures cannot show the thing that would make the increment bound obvious, which is the loser sequence drawn with its own gaps marked against the loser cc places back. Six tables of counts describe inequalities between numbers; the object is a sequence and the claim is a picture about it — two adjacent losers, the distance between them, and a third loser further down the sequence at least that far apart. That drawing is one figure and it belongs on the rung this page hands its lemma to.

Where the ladder goes next

The fibonacci-nim anchor has four rungs: that the position is a heap and a cap rather than a heap, that the factor two is one member of a family, that the family’s numerals carry a condition the recurrences do not predict, and now the two derivations.

The result the two derivations are about is the one what restores the theorem needed: a heap with a cap is a component that can carry its own rule, which two clauses and a third question turns into a condition rather than a repair.

The rung above is the increment bound itself, and it is the best-posed thing this anchor has ever handed forward. Consecutive losers differ by at most the loser cc places back is a statement about a sequence defined by a game recursion, it has 285 confirmations and no counterexample, and it now carries the gap condition on its own. Proving it means saying something about how the losers are generated — a loser is a heap from which every move loses, so the distance to the next one is the distance to the next heap with that property, and the bound says that distance never exceeds an earlier loser. That is an argument about the game rather than about numerals, which is where this anchor started and has not been back to since.

Two neighbours are worth the trip. The heap is not the position is where the state was identified as a heap and a cap, and it is the page whose framing makes the induction step statable at all — the step is a statement about what cap the opponent inherits. And the period is small and the proof does not say so is the other place on this site where a quantity everyone measures turns out not to be the quantity that governs, which is exactly what happened to the reply bound here.

Part 4 of 4

One argument about Fibonacci nim. The parts either side of it:

The objects named here

The third axis, after the field and the series: the games, values and theorems themselves, and every essay that touches each one.

EnumerationFibonacci nimGrundy valueImpartialInductionNormal playNumeral systemPeriodicitySecond-player winZeckendorf representation