One expression proved, and one withdrawn

Where the value stops mattering closed this anchor’s census. Three expressions, one per class, exact on all 1,440 pairs: the stops add when the value is cold; the stop moves by two lines when the value has straight walls; and the bent class has $\min(2t_G - f,\ 2t_H - 2f)$.

It closed by asking for the thing a census cannot supply:

Every one of the three expressions is a measured identity over a census, and two of them are short enough to be provable … A ladder whose whole census is closed and none of it proved is in exactly the position the cutcake ladder was in before its proof arrived.

One of the two is provable and the other is not true.

That separation is the useful part. The rung below reported a bound and a rule together, as two halves of one closed census; widening the pool by eight addends of the same family shows they are objects of quite different kinds.

The cold case, which comes out in four lines #

The provable one is provable, and the argument is short enough to give in full.

Let $G$ be a number and $H$ be hot. Neither player wants to move in $G$ while $H$ is hot: a move inside a number gives away a fraction of a move and gains nothing, while there is a move in $H$ worth a whole fight. That is number avoidance, and it is the theorem what a number does to a fight is built on.

So the line of play that reaches a stop plays out $H$ and never touches $G$. When it ends, $G$ is still there, unchanged, and its value is $G$ — a number is its own left stop and its own right stop. So $\mathrm{LS}(G + H) = G + \mathrm{LS}(H)$, and the same for the right stop, and the error is nought.

The error being nought is now a consequence rather than a measurement. The census agrees on all 660 of its cold pairs, which is the check and not the argument.

The proof needs the value to be a number, not merely to have temperature at or below nought, and that is exactly how the cold class is defined here. A game with temperature nought that is not a number — $\ast$, for instance — has a move worth making, and number avoidance says nothing about it.

And it is worth seeing why this one was the easy one. The other two expressions are statements about a fight — about how much two hot positions interfere when added — and interference is what has no general theory. The cold case is a statement about a fight and a non-fight, and the whole content of it is that the non-fight does not participate. There is nothing to interfere. That is why four lines suffice and why the other two are hard, and it is a fair warning about how much the first success predicts about the rest.

It also sharpens what the anchor’s other results are claims about. What a number does to a fight established number avoidance on this site and measured its reach; this rung is that theorem being used rather than measured, and the difference is the difference between a census and a derivation. A census says the stops added on 660 pairs. A derivation says they add on every pair there could ever be, and the 660 become a check on the argument rather than the evidence for the claim.

A constant that is a gap #

The straight case carries a threshold: the stop moves by twice the smaller temperature when $t_H \geq \frac{3}{2} t_G$, and by the addend’s temperature alone below that.

Before that can be derived it has to be stated, and the census does not state it.

The ratios $t_H / t_G$ occurring in the straight class jump from $4/3$ to $3/2$ with nothing between. So the threshold is not a measured boundary — it is the top of a gap, and 1.4, 1.45 and 1.5 are all equally consistent with every pair in the census.

That is a defect in a stated law rather than in a measurement, and it is fatal to a derivation before the derivation starts. A proof has to prove something, and the boundary is somewhere in this interval is not a statement an argument can arrive at.

Filling the gap, and what it does #

The obvious repair is to put ratios into the gap and find out where the boundary really is. Bent addends with temperatures between 1 and $3/2$ do it — there are plenty, and they are the same kind of object the census already holds.

Eight addends put ratios of $9/8$, $19/16$, $5/4$, $21/16$, $11/8$ and $23/16$ into the straight class. Every one of them attains the bound, so every one belongs on the upper branch — which would put the threshold at or below $9/8$.

And the ratio $4/3$ still falls short, as it did in the census. So a ratio of $9/8$ takes the upper branch while a ratio of $4/3$ takes the lower one, and no threshold on the ratio can produce that. The variable is wrong, not the constant.

The eight addends were chosen before anything about their sums was known, and that matters for how the 38 misses should be read. The selection criterion was a temperature strictly between 1 and $3/2$ with a genuine follow-up — a property of the addend alone, computed without reference to any value, any sum or any stop. Had they been found by searching for counterexamples the result would be worth much less: a large enough search finds a counterexample to almost anything, and what it establishes is that the searcher looked.

Choosing on temperature and then measuring is the same discipline the rung below applied to its own prediction about seven heaps on a different anchor, and it is what makes every one of them takes the upper branch a finding rather than a selection.

One more thing the widening does not do. It does not make the census wrong. All 372 of those pairs still behave exactly as reported, the fourteen that fall short still fall short, and the two-line rule still describes them perfectly. What has changed is what that description was evidence for — and a rule right on 372 of 372 and wrong on 38 of 620 is a rule about a pool rather than about a class.

What survives, and what does not #

The bound is untouched. $\mathrm{err} \leq 2\min(t_G, t_H)$ holds on all 620 pairs of the widened sweep exactly as it held on the 372, and it is attained on 595 of them. A bound with one number too many is where it was confirmed and where a third temperature was found not to sharpen it, and nothing here disturbs any of that.

The rule goes. It misses 38 of 620, and the residue it was written to describe is now five temperature combinations rather than one clean condition — with the stop moves by the addend’s temperature right on two of the five and wrong on three.

So the rung below’s sentence splits cleanly. The bound is a theorem waiting to be proved and the two-line rule is a fit, and the two were reported together because one sweep produced both.

The difference between them is visible in advance, once it is pointed at. A bound is a statement of the form this never exceeds that, and widening a pool can only ever refute it — every new pair is a fresh chance to break it and none of them did, so each addend added is evidence gained. A closed form is a statement of the form this equals that, and a pool that produces one is a pool that could have produced several; the new pairs are not evidence for it, they are the first occasion on which it is tested at all. Twelve addends produced the rule and twenty tested it, and the test is where a fit and a theorem come apart.

That is a lesson about this site’s method rather than about Domineering or about stops, and it applies to every anchor here that has closed a census with an expression. A measured identity exact on the population that produced it has not yet been tested once.

Why the census could not have known #

The last figure is the diagnosis, and it explains both halves of the failure at once.

The twelve addends were chosen for their behaviour rather than to span a space, and they do not vary their two temperatures independently: six of the twelve have a follow-up temperature of $1/2$, three have $1$, two have $2$, one has $3$. Several different rules therefore fit them equally well, and the one written down was one of those.

That is the same defect as the gap in the ratios, seen from the other side. A pool assembled to exhibit a phenomenon is not a pool that can adjudicate between explanations of it, and this anchor’s census was assembled to exhibit the shortfall.

There is a fleet-wide version of this and it is worth naming, because this site has now met it twice. 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 so the irrelevant variable was visibly absent. Here the opposite has happened: a statement is written without a variable it may well depend on, and the pool cannot tell. In both cases the fault is in the shape of the statement rather than in any number.

What the solver computed, and how #

Every value born by day three, taken in the first 120 of them, against a pool of bent addends — games of the form $\{a \mid \{b \mid c\}\}$, which have a hot wall and a follow-up hot enough to bend it. Each value is classified by its own wall: cold if it is a number, straight if its thermograph’s walls run straight to the temperature, bent if one of them turns.

For each pair the two games are added, the sum’s canonical form computed, and the left and right stops read off the thermograph. The error is how far the sum’s stops fall short of the sum of the parts’ stops, taken as the larger of the two sides. Every temperature is read from a thermograph rather than estimated, and every comparison is exact in the dyadic rationals rather than against a tolerance.

The widening adds eight addends of the same family, chosen by searching small dyadic $\{a \mid \{b \mid c\}\}$ for temperatures strictly between 1 and $3/2$ with a genuine follow-up. They were selected on temperature alone, before anything was measured about how their sums behave — which is what makes the 38 misses a test rather than a search for counterexamples.

Three things are asserted rather than reported. The cold case must be exact on every cold pair, since that is the case the page proves. The two-line rule must be right on all 372 census pairs and wrong on some widened ones, because the page needs it to hold and then break. And the bound must survive the widening intact, since the whole finding is that the two claims come apart.

What a derivation would have to look like #

It is worth saying what the anchor is now missing, because the rule is withdrawn leaves a hole with a definite shape.

The bound is the thing to prove, and its statement is clean: a sum’s stops fall short of the sum of its parts’ stops by at most twice the smaller of the two temperatures. That is a claim about every pair of short games rather than about a pool, it has survived 620 pairs and two independently chosen addend families, and an argument for it would be an argument about walls — the sum’s left wall cannot fall below either part’s by more than the other part’s temperature allows, because a player who has lost that much has a move left worth taking.

What is not there is any account of when the bound is attained. 595 of the 620 pairs attain it exactly and 25 fall short, and the five combinations that fall short are the whole of what a closed form would have to explain. Two of them are at $t_H = 1$ and three are at $t_H$ just below 1, which is suggestive and is not a rule — temperatures do not add is the standing reminder that suggestive arithmetic on temperatures is how this anchor got into trouble in the first place.

So the honest position is: one expression proved, one bound strongly supported and unproved, one closed form withdrawn, and one — the bent case — untested. That is a worse position than the rung below’s census closed and it is a more accurate one, and the difference between those two sentences is what this rung is.

Where the model stops #

Day three, 120 values, twenty addends. The widened pool is still a pool, chosen by one criterion, and it is entitled to the same scepticism this page applies to the census. What it establishes is that the two-line rule is false — one counterexample would do that and there are 38 — and it does not establish what the correct rule is.

And no correct rule is offered. The error is a function of the two temperatures on every pair measured, so a two-variable rule exists on this data; it is not a threshold on their ratio, and finding what it is has not been attempted here. Naming a replacement fitted to the widened pool would repeat the exact mistake this page is about.

The bent case is untouched. The rung below’s third expression, $\min(2t_G - f,\ 2t_H - 2f)$, has not been tested against the widened pool at all — the eight new addends were chosen to sit in the straight class’s ratio gap, and what they do to the bent class is a different measurement. It is the obvious next thing and it is not done here.

Normal play, and stops are a normal-play notion: the left stop is where the value settles when Left moves first and both players stop as soon as nothing is worth fighting over, which is defined by the recursion this convention makes well-founded.

And the figures cannot show what the argument most wants, which is a picture of two walls failing to meet where the rule says. Every table here is a table of temperatures; the object underneath is a thermograph, and what a reader would learn from seeing the sum’s diagram beside the two parts’ is where the shortfall comes from geometrically. Reading a thermograph draws one, and the comparison this page needs is three of them at once, which is a figure this anchor does not have.

Where the ladder goes next #

The translation anchor has eight rungs: what a number does to a fight, what an infinitesimal does, what a fight does, the bound with one number too many, which end a sum lands at, how far inside the bound the bent ones land, the last class without a formula, and now the attempt to prove the three.

The rung above is the bent expression under the same treatment. It is the one the rung below called the hard one and left for last, and it is now the only one of the three whose status is unknown: the cold case is proved, the straight one is withdrawn, and $\min(2t_G - f,\ 2t_H - 2f)$ has never been asked to survive an addend it was not fitted to. The experiment is the one this page ran, with the addends chosen to vary $f$ independently of $t_H$ rather than to fill a ratio gap — which is the specific defect the last figure identifies, and which is now known to be there. A three-variable expression fitted to a pool where the three variables move together is exactly the situation this page has just found the two-variable one in, and the honest expectation is that it goes the same way.

Two neighbours are worth the trip. The same number in two currencies is where the bent class got its formula and where the follow-up temperature became a quantity, and it is the page whose expression is now the only one standing. And a bound with one number too many is where the bound was confirmed and a third temperature found not to sharpen it — and it is worth reading beside a page where the bound survives everything and the rule beneath it does not.