The proof needs both reductions

No fifth value found the ordinal sum’s exception class stable under depth: eighteen thousand forms built by adding day-three gift horses to day-three values, four followers, and not one value whose forms give two different ordinal sums. It named the theorem behind that and the argument it expected:

A gift horse added to a form with a non-nought option is dominated in the ordinal sum is a statement with a proof-shaped argument behind it and eighteen thousand confirmations … The shape it would take is visible: show that the base’s existing options are at least as good as any gift horse in the sum as well as in the base.

They are, on 97.8 per cent of them. The other 232 are not dominated by anything the base had, and the theorem holds on them for the other reason canonical form supplies.

What a gift horse is, and why it should vanish #

A gift horse is an option added to a form that does not change its value: a Left option at most the whole game, or a Right option at least it. The name is Conway’s and the joke is the one about looking one in the mouth — the option is a free gift and no player would take it.

Adding one leaves the value alone by construction. What what the colon respects established is that the ordinal sum does not read values, it reads forms — so an operation that leaves the value alone has no guarantee of leaving the ordinal sum alone, and the whole anchor exists because for most pairs of equal forms it does not.

Gift horses are the exception. Two forms differing by a gift horse give the same ordinal sum, every time, and that is the theorem. The question this rung was handed is why.

It is worth seeing how narrow an exception that is. The operation reads the base’s form, and almost every way of changing a form while keeping its value changes the ordinal sum — what the colon respects measured that over a whole day of the construction and found four values whose forms disagree. Gift horses are a way of changing a form that the operation cannot see, and the surprise is that there is one at all, not that it needs an argument.

And the argument cannot go through the value, which is what makes it interesting. The two forms are equal is true and is exactly the fact the ordinal sum ignores. So a proof has to work on the forms — on the option lists themselves, and on what happens to them when the follower is attached — which is why the proposal reached for a statement about options rather than about values, and why the case it missed is also a statement about options.

The case that was proposed #

The natural argument is that the gift horse stays a gift horse. Placed under a follower it becomes an option of the sum, and if some option the base already had is at least as good, the new one is dominated and the canonical form deletes it — leaving exactly the form the base alone would have given.

It works 10,280 times out of 10,512. And the shares differ by follower, which is the first sign that the argument is not the whole story: under the follower $1$ it covers everything, and under $-1$ it misses 190. A single argument that were the real reason would not care which follower it was run under, since the follower appears nowhere in its statement.

The 232 #

On all 232 the ordinal sum is unchanged anyway. So the theorem is not in doubt and the argument is: a true statement whose proposed proof reaches all but 232 of its instances.

Those 232 are not a residue of near-misses. They are forms where the added option, placed under the follower, is genuinely not at most any option the base had — the domination simply is not there, and looking for a subtler version of it would be looking for something absent.

Nor are they cases where the added option happens to coincide with one already present, which would be a dull way for the theorem to hold. Not one of the 232 has an ordinal sum equal to any existing option’s, so the added option is a genuinely new element of the option list, and it has to be removed by a reduction rather than absorbed by a coincidence.

Every one of them is reversible: the added option has a Right option of its own that is at most the whole ordinal sum, which is the condition under which canonical form bypasses an option rather than deleting it. Nothing is left over.

So the proof is two cases and the proposal named one. Domination handles the common case and reversibility handles the rest, and between them they are exhaustive.

That is the standing shape of this subject’s errors about canonical form. Canonical form is two reductions — delete the dominated, bypass the reversible — and the first is the one everybody remembers, because it is the one with a one-line justification and the one that always makes a form smaller. The second is where the difficulty lives, and an argument that forgets it is an argument that will be right most of the time.

Why the second reduction is the harder one is worth a paragraph, because it explains why an argument would skip it rather than merely that this one did.

Domination is a comparison between two options: $A$ is dominated when some sibling $B$ satisfies $B \geq A$, and deleting it is safe because a player choosing between them would never take $A$. That is local — two options, one comparison — and it always shrinks a form.

Reversibility is not local. An option $A$ of $G$ is reversible when some Right option of $A$ is at most $G$ itself, which is a comparison against the whole game rather than against a sibling; and bypassing it replaces $A$ by that answer’s own Left options, which can leave the form wider than it was. How wide a form can get is where that widening is measured, and it is why the reduction is stated as a fixed point rather than as a procedure that obviously terminates.

So an argument reaching for a reason a gift horse should vanish will reach for domination first: it is the reduction that removes things, and removing the added option is what the theorem says happens. Reversibility removes it too, by a route that goes through the whole sum and comes back.

Which follower the second case belongs to #

The second case is almost entirely one follower. Under $1$ it is never needed; under $-1$ it is needed 190 times of 2,628; under $\ast$, 41 times; under $\uparrow$, once.

Since the bases and the gift horses are identical across the four rows, the case a proof needs is decided by the follower — by the thing the ordinal sum places underneath. That is a useful thing to know about the shape of the missing argument, and it is not what the proposal expected: the proposal’s sentence is about the base’s options and the gift horse, and neither of those is what varies here.

The direction is legible. The gift horses added here are all Left options, added to a base’s Left list. Under a follower favouring Left there is always something at least as good already present, so domination suffices. Under a follower favouring Right the base’s Left options have been made less attractive relative to each other, the comparison that domination needs stops holding, and the reversal — Right’s answer to the new option being no worse than the whole sum — is what carries the argument instead.

The two intermediate followers fit that reading and are worth quoting because they are not extremes. Under $\ast$, which favours neither player, the second case is needed 41 times; under $\uparrow$, which favours Left by an infinitesimal, once. So the count falls with how much the follower helps Left — 190, 41, 1, 0 as the follower runs from $-1$ through $\ast$ and $\uparrow$ to $1$ — and that ordering is the ordering of the followers themselves. The share needing the second case is a monotone function of the follower’s own value, over four points, which is few and is the right shape.

The hypothesis that does nothing #

The theorem as the rung below stated it carries a hypothesis — a form with a non-nought option — and on this sweep it is satisfied by every base. So it excludes nothing, it cannot be separating the two cases, and the sweep has no information about what it is for.

That is worth recording rather than quietly dropping. A hypothesis that is vacuous on the population a theorem was measured over is a hypothesis nobody has tested, and it arrived from a plausible worry rather than from a counterexample. Whether it is needed at all is a question for a pool containing forms whose every option is nought, and day three has none.

What this says about the theorem’s status #

The anchor’s ledger is worth updating explicitly, since proved is a word this site spends carefully and none of it has been spent here.

The theorem is not proved. It is confirmed on 10,512 instances, as it was on eighteen thousand forms one rung down, and this page adds no argument that holds beyond the sweep.

What is now known is the shape of the argument. It has two cases, they are the two reductions of canonical form, and their proportions are 97.8 to 2.2. Anybody attempting the proof knows what to prove and knows that a single-case argument will be a proof of most of it — which is worth having, because a single-case argument is what would have been attempted and what would have looked like a success.

And one route is closed. The proposal’s sentence — the base’s existing options are at least as good as any gift horse in the sum as well as in the base — is false as a general statement. It is not that nobody has proved it; it has 232 counterexamples in this pool, and any argument for it is an argument for something that does not hold.

That last is the most useful of the three, and it is the kind of thing this ladder produces rather than theorems. The other sum that nests is where this anchor’s operations were laid out; what it has been accumulating since is a list of what the ordinal sum does and does not respect, and this rung adds a line to the second list about an argument rather than about a value.

What the solver computed, and how #

One hundred distinct values born by day three, sampled from the full day-three list, each given every gift horse from a pool of eighty day-three values. A Left gift horse is a value at most the base; adding it to the base’s Left option list must leave the value unchanged, which is checked rather than assumed, and forms failing that check are discarded.

Each surviving form is placed under four followers — $\ast$, $1$, $-1$ and $\uparrow$ — by the ordinal sum, and three things are computed for each.

Domination: the added option’s ordinal sum against every existing Left option’s ordinal sum, asking whether any of them is at least as good. That comparison is a search over a difference game, run in full rather than approximated.

Reversibility: for the escapes, whether the added option’s ordinal sum has a Right option at most the whole sum — which is the definition, applied directly.

And the theorem itself: whether the ordinal sum of the enlarged form equals the ordinal sum of the base, compared by identity of canonical forms rather than by value.

Three things are asserted rather than reported. Domination must cover most and not all, or there is no second case to report. No escape may be neither dominated nor reversible, since the page’s claim is that the two cases are exhaustive. And the ordinal sum must be unchanged on every escape, or the theorem fails there and the page is about something else.

Where the model stops #

Day three, a hundred bases and eighty gift horses. The two cases are exhaustive on 10,512 instances and that is a sweep rather than an argument — nothing here proves that a gift horse escaping domination is always reversible, only that all 232 in this pool are. A day-four sweep is the obvious next check and is expensive.

Left gift horses only. Every gift horse added here goes into a Left option list. The mirror sweep — Right gift horses — should behave as the mirror, and the follower asymmetry says it would not be symmetric in the followers: what $-1$ does to Left options, $1$ should do to Right ones. That has not been run, and the prediction is stated here in the right order.

And two cases exhaustive is not a proof of either. What this rung establishes is the shape of the argument — which reductions it needs and in what proportion — and it does not supply either case. The proposal’s case would still have to be proved in general, and so would the reversibility case, and the second is the harder of the two because reversibility is a condition on the whole sum rather than on a pair of options.

Normal play throughout, and both reductions are normal-play reductions: they preserve the value under the disjunctive sum, which is what makes canonical form well defined. The ordinal sum is not a disjunctive sum and does not preserve values, so this page is using a normal-play tool on an operation the tool was not built for — which is the whole reason the anchor exists and is worth naming once rather than assuming.

And the figures cannot show a reversal. Six tables of counts describe two reductions, and the object — a form, its added option, and the Right answer that makes that option reversible — is a small tree with an arrow in it. Canonical form draws one reduction on one position; what this page would want is the same drawing on one of the 232, with the follower underneath, and it is a figure this anchor does not have.

Where the ladder goes next #

The ordinal-sum anchor has five rungs: the operation and its Hackenbush reading, that it does not respect equality, how much of equality it respects anyway, that the exception class is stable under depth, and now what a proof of the gift-horse theorem needs.

The rung above is the reversibility case on its own. It is 232 instances, all under followers that favour Right, and the pattern in them is stated but not extracted: the added option’s Right answer is at most the whole sum, and which Right answer it is has not been recorded. Recording it is the same sweep with one field added, and if the answer is always the follower’s own contribution — the part of the sum below the base — then the reversibility case has a one-line description and the theorem has a two-case proof written out. That is the first time this anchor has had a target that specific.

Two neighbours are worth the trip. What the colon respects is where the exception class was found and where the gift horses were identified as the operation’s one safe substitution, and it is the page this one supplies the reason for. And when the nested sum only sees the value is the ordinal sum’s one dangerous property stated from the other side — that it reads the form of its base — which is exactly why a substitution that preserves the value needs an argument at all.