The context that tells them apart
Two positions put into the same company, one context at a time. Each column is a game X; each cell is the outcome class of that side added to X. Equality means every column agrees, for every X there is — so a single disagreeing column is a disproof, and agreement across a bounded list of contexts is evidence rather than proof. The proof is that the difference is zero.
4 essays call
context-witness. The drawing above is what it returns with no arguments at all; every
call below passes it something, because a placement that passes nothing draws whichever
member of the family the generator happens to default to rather than the one its essay argues
about.
The positions it draws
28 distinct positions, harvested by drawing the figure again at the options each essay asked for.
Where it is called
Every one of these figures is a drawing of the same construction, so a correction to it corrects them all.
Sums and comparison
Equal in every company
Two games are equal when no third game can tell them apart — a quantifier over every position there is, discharged by one finite test. A search over 184 contexts separates all 5,790 unequal pairs it is handed and still calls two different games the same, which is exactly why G − H = 0 is a theorem and an exhaustive search is not.
Where it stops
Equal in this company
Equality quantifies over every game there is, and the quantifier can be made smaller. Restricted to a company of nine numbers, the twenty-two values born by day two collapse to seventeen; restricted to four games — nought, one, minus one and star — they stay twenty-two, and no three of the four will do. The company that decides equality is tiny, and it has to contain a star.
Sums and comparison
The same parts, different wholes
Equality is worth having because equal parts make equal wholes: a game may be replaced by an equal one inside any sum and any larger position. The relation that 184 contexts define — no context tells the two apart — is exact on day three and merges a third of a sample of day four. Put 567 of its merged pairs through negation, addition and forming options, and it survives two of the three. Adding the same game to both separates them 1,527 times.
Sums and comparison
A universe grows by days, not by sums
A relation built from a sample of contexts can be repaired two ways: allow sums of more values, or allow values born a day later. On a sample of day four the first stalls — 147 pairs of different games stay merged from five summands to seven, through 25,696 contexts — while the 985 values of day three, a seventh as many, separate every pair. The reason is four lines long: the context that tells two games apart is always minus one of their options.
The whole library · The position index · The figures that play back