The same parts, different wholes

Equal in every company defines equality by a quantifier over every game there is — $G = H$ when no third game $X$ puts $G + X$ and $H + X$ in different outcome classes — and then discharges the quantifier with one finite test: $G = H$ exactly when $G - H$ is a second-player win. It also runs the quantifier directly over a universe of 184 contexts, the 22 values born by day two and every sum of two of them, and finds that universe separating every unequal pair it is given except one, tiny-two against tiny-four, which all 184 contexts agree about.

That leaves two relations side by side. Equality, which the difference test decides. And the sampled relation: two games are related when none of the 184 contexts separates them. The second is computable by brute force and contains the first; the question this essay asks is whether it can do the first one’s job.

The job is substitution. Every recursive computation in the subject replaces a part by something equal to it — a component of a sum by its value, an option by its canonical form, a region by a table entry — and trusts the result. That trust is a theorem about equality, and the question is whether the sampled relation has the same theorem.

The theorem that licenses every recursion #

The substitution theorem has three clauses, and each is the reason for a habit.

Equality is preserved by addition. If $G = H$ then $G + X = H + X$ for every $X$. The proof is one line: $(G + X) - (H + X)$ is $G - H$ plus a copy of $X$ and its negative, and both of those pieces are worth nothing. This is the clause that lets a board be split into regions and each region replaced by its value.

Equality is preserved by negation. If $G = H$ then $-G = -H$, because $-G - (-H)$ is the negative of $G - H$ and the negative of a second-player win is a second-player win. This is what lets a position be read from the other player’s side.

Equality is preserved by forming options. If $G = H$, then a game with $G$ among its Left options equals the same game with $H$ in its place. This is the clause every canonical-form computation leans on, since simplifying a game means simplifying its options first and trusting that the game has not changed.

Together they say equality is a congruence: an equivalence that every operation of the subject respects. A value is a class of games under a congruence, which is why values can be added, negated and nested exactly as games can. Every game has a negative supplies the mirror strategy that makes the first two clauses work.

What the sample sees, one day at a time #

Before asking whether the sampled relation is a congruence, it is worth knowing how coarse it is.

On day three the sampled relation is equality. The 985 values with up to two options a side drawn from day two fall into 985 classes: the universe separates every one from every other. That is consistent with what the earlier essay found for day two and suggests the universe is simply a generous sample.

One day later it is nothing of the kind. A seeded sample of day-four games — 6,000 forms with up to two options a side drawn from those 985, which canonicalise to 495 distinct values — falls into only 366 classes. Forty-nine classes hold more than one value, 178 values between them, and the largest holds twenty-two. Tiny-two and tiny-four were not a rare exception. They were the first visible case of a relation that, one day past the games it was built from, merges more than a third of what it sees.

Two operations it survives #

Take every pair of distinct values from those forty-nine classes — 567 pairs — and apply the three operations of the theorem to both halves of each pair, then ask the 184 contexts again.

Negation never separates a pair. That is not luck. The universe is closed under negation — the negative of a day-two value is a day-two value, and the negative of a sum of two is a sum of two — so if no context separates $G$ from $H$, no context separates $-G$ from $-H$ either: a context $X$ that separated the negatives would have $-X$ separating the originals. The clause holds for the sampled relation by the same kind of argument that proves it for equality, with the universe standing in for all games.

Forming options never separates a pair either. Each pair was used as an extra option of $\{A \mid B\}$ on either side, with $A$ and $B$ each empty or one of the four day-one values, 28,350 constructions in all, and the universe told none of the resulting pairs apart. That clause is explained by a property the closure that picks the nimbers names: a universe whose games have all their options inside it licenses the replacement of a subposition, and this universe is such a one — the options of a day-two value are day-one values, and the options of a sum of two day-two values are sums of a day-two and a day-one value, all inside the 184.

The operation it fails #

Adding the same game to both halves separates them 1,527 times out of 12,474 tries — every pair, beside each of the 22 day-two values. And 355 of the 567 pairs are separated by at least one of those additions. The sampled relation calls the parts the same and the wholes different, which is precisely what a congruence cannot do.

The shortest broken pair makes the failure concrete. The two games $\{\{∗ \mid ↓\} \mid 0\}$ and $↓ + ↓ + ↓∗$ — three downs and a star — are different: their difference is not nought. Every one of the 184 contexts nonetheless puts them in the same outcome class, so the sampled relation calls them equal. Now add $↑$ to both. Beside the context $⇑∗$, which is in the universe, the sum built from three downs is a second-player win and the other is a win for Left. The relation has been handed two equal parts, one copy of $↑$, and returned two unequal wholes.

Why adding a game can make the difference visible #

The mechanism is the same one that let the difference test replace the quantifier in the first place.

Among all contexts, one is sure to separate $G$ from anything unequal to it: $-G$, because $G - G$ is a second-player win and nothing unequal to $G$ gives one. For three downs and a star, that context is three ups and a star — a sum of three day-two values, and the universe holds sums of two. So the one context certain to work is missing, and none of the others happens to do the job.

Add $↑$ and the game becomes two downs and a star. Its negative is $⇑∗$, the sum of $↑$ and $↑∗$, and that is in the universe. The addition did not change what the two games are; it moved the needed context into reach. Every one of the 1,527 failures has this shape: some context $Y$ in the universe separates $G + X$ from $H + X$, which is the same as saying $X + Y$ separates $G$ from $H$ — and $X + Y$, a sum of up to three day-two values, lies outside the universe that defined the relation.

That is also the whole reason the sampled relation fails addition and survives the other two. The company that is closed states it as a condition: a relation defined by a company of contexts is preserved by adding a member of the company exactly when the company is closed under addition, and it found that none of the companies these computations use is closed. The 184 are the equality essay’s own company, and here the condition is watched failing on real pairs rather than stated.

Which addend is added matters, and not in the order a reader might guess. The switches of day two — $\{1 \mid 0, ∗\}$, $\{1 \mid ∗\}$, $\{∗ \mid -1\}$ — each separate about a third of the pairs; so do $-1$ and $∗$. The infinitesimals $↑$ and $↓$ separate few, and $∗2$ separates eight. Fifteen of the twenty-two separate at least one pair. There is no addend that can be relied on to be harmless, which is what a practical version of the sampled relation would need.

The famous pair is the robust one #

The pair that started this, tiny-two against tiny-four, behaves differently from the pairs the addition test breaks, and the difference is instructive.

The tinies form a family, $\{0 \mid \{0 \mid -n\}\}$ for $n = 1, 2, 3, \ldots$, each positive and each smaller than the one before, all of them smaller than every positive number and than $↑$. Put the first six through the 184 contexts and tiny-one stands alone while tiny-two to tiny-six all fall into one class: the universe can tell that tiny-one is not tiny-two, and cannot tell any two of the rest apart. The reason is the one above, run on a family. The context guaranteed to separate tiny-$n$ is its negative, miny-$n$, which is born on day four; tiny-one’s difference from the others is large enough that something simpler catches it, and the differences further down are smaller than anything the universe contains.

And that pair, unlike the 355 the addition test broke, survives addition. Tiny-two and tiny-four were added to each of the 184 contexts in turn and the sums tested against all 184 again; none separated. They were used as the extra option of $\{A \mid B\}$ for every $A$ and $B$ empty or a single day-two value, 1,058 constructions, and none separated either. Adding a game to both tinies does not bring the needed context into reach. The context certain to separate tiny-two plus $X$ from tiny-four plus $X$ is the negative of the first sum, miny-two minus $X$, and no choice of $X$ from the universe brings it inside: that would need miny-two to be a sum of two of the 184, and a check of all 17,020 such sums finds it nowhere. For three downs and a star the needed context was one ordinary game too many; for the tinies it is a game of a different order, and no addition supplies it. The pair tiny and miny made famous is the one that looks most like a congruence from inside the sample. The pairs that give the relation away are the anonymous ones, whose difference is an ordinary game the universe nearly contains.

That is a warning about how a relation like this would be tested in practice. A reader checking the sampled relation on the one pair everybody knows would find it respects every operation tried. The failure lives in the pairs nobody has names for, and it took a sample of 495 values to find the first of them.

A signature is a key, and a key is not a value #

There is a practical version of the sampled relation, and it is worth naming because a solver might build one without meaning to. The column of 184 outcome classes is a signature: a fixed-length string computed from a game, equal for equal games, and cheap to compare. A solver that stored positions by their signature — to recognise a region it had met before, say — would be using the sampled relation as its notion of sameness.

A key shorter than the position measures what happens when a table is addressed by a key that identifies positions which differ: wrong verdicts at a rate set by arithmetic. The signature is a better key than a hash — it never confuses two games with different outcomes against anything in the universe — but it has the defect the table above measures. A solver may safely recognise a whole game by its signature. It may not recognise a part by its signature and add: two parts with the same signature can make sums with different signatures, and 355 of the 567 merged pairs do. A value, by contrast, is exactly a key that survives addition — which is why many forms, one value can collapse 256 written forms to 22 values and then add the values rather than the forms.

Equality, through the same test #

The column of noughts beside equality in the hero table is not taken on trust; it is checked on the same range.

Every form $\{A \mid B\}$ with $A$ and $B$ day-two values was grouped by its value, and each form paired with another of the same value — 314 pairs of equal games written differently. Each pair was added to every day-two value and negated, and the results compared by canonical form: 7,222 comparisons, no difference. The theorem says there can be none. The check exists because a test that has never been run against the relation it trusts is a test of nothing, and this one is run on the same games and the same operations as the sampled relation that failed.

The convention named #

Everything here is normal play, and the outcome of a sum is computed from the recursion rather than read from a value table. “Separates” means puts in different outcome classes; the sampled relation is defined by the 184 contexts of equal in every company, sorted simplest first, and every test that reports a separation names the context. The day-four sample is drawn with a fixed seed, so the counts are reproducible, but they are counts for this sample: a different seed gives different pairs, and the 567 are not every merged pair day four contains.

What the tables cannot show #

Forming options survived 28,350 constructions and is explained by closure under options; it is not proved here for every construction. The constructions used one extra option of day-one company. A game with two of the merged values among its options at once, or with a merged value deep inside an option, is untested.

The sample is a sample of day four. Day four has more values than anyone has listed, and the share of it the sampled relation merges could be larger or smaller than the third measured here. What cannot change is the direction of the failure: once one merged pair is separated by an addition, the relation is not a congruence, whatever the rest of the day looks like.

And nothing here says the sampled relation is useless. It is exact on day three, it respects negation and options, and it is cheap. It is a coarser arithmetic that cannot be trusted across a plus sign — which is a precise description of where a solver may use it and where it may not. Tiny and miny is where the first merged pair comes from, and it is a family whose members differ by less than anything in the universe can measure.

Still open: a universe that grows with what it is asked #

The failure has a repair in principle and a cost in practice. Every broken pair is separated by a context that is a sum of three day-two values, so a universe of sums of three would separate every pair the addition test broke — and would fail in turn on pairs separated only by sums of four. The measurement that would say whether that regress ends is the same census run with sums of three: how many of the 567 pairs it merges, and whether its own merged pairs are broken by adding a day-two value at a rate that falls. If the rate falls fast, a universe of modest size is a practical stand-in for equality up to some day; if it does not, comparison is a search is the only honest way to decide equality, and the difference test is not merely convenient but unavoidable.