Nine steps of pessimism

Two routes to a rigorous error statement exist in this collection and only one of them is used. A bound that is proved computes the answer in ordinary floating point and then proves a bound on it, and it states plainly that the other route — carrying intervals through the algorithm — is what nobody does. That is the standing rule of the whole subject, and it is stated without a number in it.

Both routes are rigorous. Both overstate. The question the rule leaves unasked is by how much, because a prohibition is worth having only if the thing prohibited is worse than the thing recommended, and worse by enough to matter over the length of computation anybody runs.

The two over-estimates have different shapes, and that is the whole content here. Enclosing once, at the end, costs a fixed multiplier: the bound comes back some number of times larger than the error it bounds, and that number does not depend on how long the computation was. Re-enclosing at every step costs a multiplier per step, which compounds. A fixed factor and a compounding one cross somewhere, and where they cross is a length.

Both multipliers are measurable in this collection’s own arithmetic, and neither has been measured against the other.

The compounding price is exactly √2 and it is not about the arithmetic #

A rotation is the cleanest possible test case, because it changes nothing. It is an isometry, so the true set has the same width after twenty applications as before the first, and every increase in the enclosure is over-estimate and nothing else.

At 24 significand bits, over the seven rotation counts the figure above can be driven to, the enclosure divided by the set reads 4.00 at four rotations, 16.0 at eight, 64.0 at twelve, 256 at sixteen, 1,024 at twenty, 16,384 at twenty-eight and 262,145 at thirty-six. The mean growth per step is 1.41421 at every one of those counts, against √2 = 1.41421.

That is not a fitted constant and it is not a rounding effect. Measured across six rotation angles at twenty steps, the growth per step is 1.17588 at π/16, 1.30656 at π/8, 1.36603 at π/6, 1.41421 at π/4, and then back down through 1.36603 and 1.30656 as the angle passes 45° — matching |cos θ| + |sin θ| to five figures at every angle. That expression is the width of the axis-aligned box around a unit square rotated by θ, divided by the width of the square. The over-estimate is the shape of the representation and nothing else, which is why a rotation was chosen: there is no residual, no conditioning, and no accumulation of rounding to attribute any of it to.

There is also no transient. At twenty-four bits every one of the twenty individual step ratios reads 1.41421 to six figures: the first rotation costs the same factor as the twentieth, and the minimum and maximum over the twenty are the same number. That is worth separating from the several bounds in this collection that are true only in a limit. This one is not an asymptotic rate that a long enough run settles onto — it is the exact factor at every step from the first, which is what makes a crossing at nine steps a meaningful thing to compute at all. A rate that only holds after fifty steps could not be set against anything at nine.

The consequence is that the compounding price is known in closed form before anything runs. After m re-enclosures the carried interval is (√2)ᵐ times too wide, at worst, and the worst is the 45° case drawn here.

The fixed price is about twenty, over nineteen cases where it exists at all #

The other route computes the answer first and proves a bound on it afterwards, and the quantity to price is the slack: the proved bound divided by the error the computation actually made.

That division is only available because the error is known rather than estimated. The test problem is the Hilbert system whose solution is the integers 1 to n by construction, so the answer the bound is held against is the answer and not a better float. The slack is therefore a division and not an estimate of one, which is what lets it be set against a geometric factor without a tolerance in the middle.

Across five working precisions from 16 to 40 significand bits and eight Hilbert sizes from 3 to 12 — forty cases — the method proves a bound in nineteen and refuses in twenty-one. The nineteen slacks, sorted, run 7.85, 8.17, 9.95, 12.5, 15.6, 15.8, 17.4, 19.0, 19.8, 22.0, 23.1, 25.9, 26.0, 26.4, 32.1, 56.0, 126, 365 and 2,822. Fourteen of the nineteen lie between 7.85 and 26.4, a spread of a factor of 3.4 over twenty-four bits of precision and six matrix sizes, and the median is 22.0.

Nineteen of forty is itself part of the price, and it is the half of it that has no factor attached. A refused case does not return a wide bound; it returns nothing, so its slack is not large but undefined, and no average over the grid can include it. Every number in this comparison is therefore conditional on a bound existing, and the condition failed in twenty-one of the forty cases drawn. The carried interval has no such condition: it returns a width at every size and every precision, and the width is correct.

The natural explanation for a factor of twenty is the wrong one, and the measurement says so. The bound is ρ/(1 − κ′), with κ′ = ‖I − RA‖ and ρ the outward-rounded residual norm, and the obvious reading is that the slack is the amplifier 1/(1 − κ′) growing as κ′ climbs toward the refusal. It is not. Across the nineteen verified cases that amplifier is below 1.08 in sixteen of them and its largest value anywhere is 2.56. The factor of twenty is ρ divided by the true error — the residual route overstating on its own, before any amplification.

The slack has no trend in the matrix size either, which is the other axis it might have had one in. At 40 bits the six verified sizes read 7.85, 25.9, 126, 15.6, 32.1 and 26.4 as the size runs from three to eight, and at 32 bits the five read 8.17, 19.0, 19.8, 15.8 and 2,822. Both sequences move up and down inside the band and neither climbs with the size, even though the condition number rises by about a factor of thirty per size across them. The slack is a property of the method rather than of the problem it is applied to, which is the assumption the crossing needs and which nothing had checked.

The largest slack in the set makes the point at size: 2,822 at 32 bits and the seventh Hilbert size, where the amplifier is only 1.33 and ρ alone is 2,128 times the error. And 126 at 40 bits and the fifth size has an amplifier of 1.000 to four figures, because κ′ there is 6.0·10⁻⁷ — that slack is entirely a solve that happened to come out more accurate than its neighbours, which is the same phenomenon a small residual is not a small error reads from the other side.

The crossing is at nine #

The two prices are now numbers of the same kind — a factor by which a rigorous statement exceeds the truth — so they can be set against each other directly. For each rotation count m, the question is how many of the nineteen proved bounds are wider than (√2)ᵐ, which is how many of them a carried interval would have beaten:

At four re-enclosures the carried interval is narrower than the proved bound in every one of the nineteen cases, because the smallest slack anywhere in the set is 7.85 and 4 is below it. At eight it is narrower in thirteen. At nine it is narrower in nine and wider in ten, which is where the majority turns over. At twelve it is narrower in three, and those three are the anomalous cells named above — 126, 365 and 2,822 — rather than anything typical.

The same number arrives from the other direction. Setting (√2)ᵐ equal to the median slack of 22.0 gives m = 8.91; equal to the 23.1 the twenty-four-bit figure reports at the fourth Hilbert size, m = 9.06. Taking the median slack at each precision separately and solving for m gives 10.40 at 16 bits, 9.40 at 20, 7.30 at 24, 8.49 at 32 and 9.41 at 40 — five independent estimates spanning 7.3 to 10.4, with four of the five above 8.4.

So the rule this collection has been carrying is a statement about length, and the length is about nine. Below it, carrying intervals through the computation is the tighter of the two rigorous routes. Above it, the enclose-once route wins and goes on winning by a factor that doubles every two steps.

What precision buys is reach, and it does not buy tightness #

Sixteen more bits of significand between the two figures above move the refusal from the sixth Hilbert size to the tenth, and leave the slack where it was. Over the five precisions the largest size at which a bound can be proved runs 4, 5, 5, 7, 8 — monotone, and roughly what the boundary at κu ≈ 1 would predict. Over the same five precisions the median slack runs 36.7, 26.0, 12.5, 19.0 and 26.1, which is not monotone in anything and has no trend in it at all.

That separation is the reason the crossing is a stable number rather than a number that has to be quoted with a precision beside it. The compounding price has no precision in it, as the next two figures establish, and the fixed price barely moves across twenty-four bits. The crossing is the ratio of two quantities that both ignore the arithmetic, so it ignores the arithmetic too.

It also means the two prices are paid for different things. More precision does not make a proved bound tighter; it makes a proved bound exist at problems where it previously did not, which is a statement about what a float can hold rather than about the method. The bound’s width is a property of the residual and the outward rounding, and both of those scale with the answer.

The excess over √2 is the outward rounding’s own accumulation, and it is computable #

At eleven bits the growth is 1.41561 a step rather than 1.41421, and the enclosure after twenty rotations is 1,044 times the set rather than 1,024. Both differences are real and both are small: one part in a thousand on the growth, against a compounding factor of 41 per cent a step.

The excess has a form. Dividing the measured ratio by (√2)ᵐ at eleven bits gives 1.0039, 1.0078, 1.0117, 1.0156, 1.0195, 1.0273 and 1.0352 at four, eight, twelve, sixteen, twenty, twenty-eight and thirty-six rotations. Those are exactly 2·m·2⁻¹¹ to every digit shown. Each rotation rounds the box outward by a relative 2⁻ᵇⁱᵗˢ at each end, and those roundings accumulate alongside the √2 rather than inside it, so the excess is linear in m where the effect being measured is exponential in it.

The per-step ratios at eleven bits are not constant either, where at twenty-four bits they were. Across the twenty rotations they oscillate between 1.41504 and 1.41615 around the 1.41561 mean, with no drift in either direction. Where the outward rounding lands depends on the endpoints of the box being rounded, and those endpoints move at every step, so the excess arrives unevenly and averages out — which is why the mean over twenty steps is a stable quantity even though no individual step carries it.

The multiplier on m·2⁻ᵇⁱᵗˢ is not always two. At sixteen bits the same ratio comes out as exactly m·2⁻¹⁶ — 6.1·10⁻⁵ at four rotations rising to 5.5·10⁻⁴ at thirty-six — because whether the rounded value of cos(π/4) falls above or below the true one is decided by the bit pattern at that precision, and it differs between eleven bits and sixteen. At twenty-four bits the multiplier is two again and the excess is 2.4·10⁻⁶ at twenty rotations. At fifty-three bits it is negative and of size 10⁻¹⁵.

The distinction matters for what the closed form is asserted against. A claim that the ratio is (√2)ᵐ to within a flat two per cent is true at twenty-four bits and above and false at eleven, where the excess reaches 3.5 per cent by thirty-six rotations — not because the geometry changed but because a term nothing in the claim mentioned had grown into view. Carrying the computable term instead lets the same assertion run at every precision the arithmetic reaches, and all twenty-eight combinations of seven rotation counts and the four precisions drawn here render under it. The direction the error leans is the reason the term exists at all: outward rounding is the one thing in this arithmetic that is deliberately not to nearest, and the price of that is a small one-sided drift that never cancels.

Where nine is the wrong number #

The crossing is a real measurement and it is narrower than it sounds. Four things bound what it covers, and each of them moves the number in a direction worth knowing.

Nine counts re-enclosures, not operations. A rotation is one re-enclosure per step by construction, which is what makes it a clean instrument and also what makes it unrepresentative. The count that matters is the number of times a correlated quantity is forced back into an axis-aligned box, and that is not the operation count. A straight-line accumulation re-encloses once per term and pays nothing at all for it, because addition is monotone in both arguments and the enclosure is exactly the two directed runs — the two widths have been measured bit-identical at lengths up to four thousand. The price is charged when a value is used twice, and only then.

Forty-five degrees is the worst case. The growth per step is |cos θ| + |sin θ|, which is 1 at zero and √2 at 45°, so the crossing at other angles is later: solving for the same factor of 22.6 gives m = 19.3 at π/16, 11.7 at π/8, 10.0 at π/6 and 9.00 at π/4. Nine is therefore a floor on the crossing rather than an estimate of it, and a computation whose correlations are mostly axis-aligned tolerates two or three times as many re-enclosures before the other route wins.

The fixed price has a tail the crossing does not describe. Three of the nineteen slacks are 126, 365 and 2,822, and against those a carried interval stays narrower to fourteen, seventeen and twenty-three re-enclosures. Two of the three sit at the last size a precision verifies at, where the amplifier is doing something; the third does not. A median is the right summary for nineteen cases and it is not a guarantee about any one of them, which is the same reservation a bound that holds with probability is built around, arriving here without any randomness to justify it.

And the comparison assumes both routes return something. Below nine re-enclosures the carried interval is narrower, and it is narrower everywhere rather than only where a bound exists. Twenty-one of the forty cases have no proved bound at any width, and in those the carried interval is not narrower than the alternative — there is no alternative. That asymmetry is what the refutation at the head of this essay is about, and it is the one respect in which the recommended route is strictly worse than the prohibited one.

What follows for anything that has to be rigorous #

A verified solver is already built the right way, and now for a stated reason. Computing in floating point and enclosing once at the end is not merely the way that works; it is the way that wins by a factor of (√2)ᵐ⁻⁹ over the alternative, which is a reason with a length in it rather than a warning.

A short interval computation is not a mistake. Four or six re-enclosures of a correlated quantity cost a factor of four or eight, and every proved bound measured here is wider than that. A method that carries intervals through a handful of steps and stops is doing something defensible, and the prohibition as usually stated forbids it.

An operator that re-encloses per iteration should count its iterations. The operator that turns an enclosure into a proof of existence and the subdivision search built on it both re-enclose, and the count is the thing to watch rather than the width of any single box. A search that halves boxes for twenty rounds has spent (√2)²⁰ of pessimism if it carries a correlated quantity across them, and nothing about the box widths on the screen says so.

A bound that grows with the length of an accumulation is a different object. Three walks and one bound prices an error bound that overstates by a factor rising with the number of terms, and the resemblance is superficial: that growth is in a bound on a computed quantity, and this one is in the quantity itself. The carried interval really is that wide. Nothing is being overstated about it.

And a bound wide enough to be satisfied by everything is the failure this measures against. A bound every answer satisfies and the bound that is never attained are both about statements that are true and empty. A factor of twenty is neither: it is a bound anybody would accept and a bound that is doing work. A factor of a thousand, which is what twenty re-enclosures buys, is the first kind.

The exact route prices both of these. An answer with no error in it computes in rationals and has no over-estimate of any size, at a cost that grows with the size of the numerators. Rigour by enclosure is the cheap approximation to that, and what it charges is the factor of twenty. Rigour by carrying is the same purchase made repeatedly, and what it charges compounds.

And none of it is a backward-error statement. The exact answer to a nearby problem is a claim about which problem was solved, with no interval in it and no refusal available. The two prices here are both paid for a forward statement about this problem, which is the more expensive thing to want and the thing a verification is for.