A bound that is proved

CLAIM_REGISTRY.md records this as one of the areas the depth phase declined: interval arithmetic as a method rather than as a two-run bracket on a sum. In the same phase it built the machinery the method needs and wrote in float.js that the directed rounding modes are “useless singly and the whole of interval arithmetic”. This essay is that sentence cashed.

Every error statement this site has made so far is a measurement. A residual computed, a forward error compared against a known answer, a bound evaluated and reported loose by a factor of five. Every one of them is a statement about the run that produced it.

Interval arithmetic makes a different kind of claim: that the answer lies in this set, for this input, with no probability and no asymptotics attached. The difference between those two kinds of statement is the whole content here.

Directed rounding, and why it is at 24 bits #

An interval operation is rigorous only if the lower end is rounded toward −∞ and the upper end toward +∞, so no rounding can move the true value outside.

JavaScript has no rounding-mode control, and at binary64 roundBits correctly returns its argument unchanged in every directed mode — the value is already representable, so there is nothing to round.

So the arithmetic here runs at a simulated precision, 24 bits by default, where arith(24, { mode: "up" }) and arith(24, { mode: "down" }) genuinely round outward. That makes every interval below rigorous for a 24-bit machine, and it makes the enclosure checkable against a double-precision computation that is exact by comparison.

This is not a simulation of interval arithmetic. It is interval arithmetic, on a machine whose precision is a parameter — which is this site’s precision as the knob thread doing something it has not done before: making a method available that the host language cannot express.

Containment, checked sixteen thousand times #

The property everything rests on, and the only one whose failure would be silent. An enclosure that is too narrow still looks like an enclosure.

So it is checked by brute force: four operations over four thousand random operand pairs, with the exact answer computed in double, which is twenty-nine bits better than the arithmetic under test. Sixteen thousand containments, all of them holding.

Multiplication is where a hand-written version usually goes wrong, because it must take the extreme over all four corner products. [−2, 1] × [−3, 4] is [−8, 6], and neither end comes from the pair of endpoints that look like they should produce it. The refusal at the end of lib/interval.js feeds the two-endpoint version and requires it to fail — the only bug in this file that would produce an enclosure too narrow rather than too wide, and therefore the only one that could go unnoticed.

Which operations stay tight, and it is not the pair the textbook names #

A bound that is true and enormous proves nothing anybody wanted, so the width matters as much as the containment. Measured relative widths, at 24 bits where u = 6.0·10⁻⁸:

Multiplication and division come back a few ulps wide, always: their relative error is bounded by u regardless of the operands, because a product’s exponent is the sum of the exponents and nothing can cancel.

Addition and subtraction are both unbounded, and getting to that took two attempts. The first version asserted tightness over all four and found 1.4·10⁻⁴. The second blamed subtraction, on the strength of this site’s own cancellation essay, and failed on addition with the identical number.

Which is right, and is the sharper statement. Cancellation is a property of adding two numbers whose signs differ, not of the operator that was typed. a + b with b ≈ −a cancels exactly as a − b with b ≈ a does, and the operands here are random normals, so both happen. The rule of thumb subtraction is dangerous names the common case and misses the mechanism.

And the wide interval is not a defect. It is the property that makes the method worth having: a floating-point subtraction returns a confident wrong answer there and an interval one returns a wide correct one. The relative width of the additive pair is therefore asserted to be large, in the direction it goes.

The way that does not work #

Carry intervals through an algorithm and it fails, spectacularly, for a reason that has nothing to do with rounding.

An interval box is an axis-aligned rectangle. Rotate one and the true image is a tilted rectangle; the smallest axis-aligned box containing it is larger. Do it again and the enlargement compounds. This is the wrapping effect, and it is why nobody does interval Gaussian elimination.

Measured over twenty rotations of 45°: the true width stays at 2.000 throughout, because a rotation is an isometry and the set does not change size at all. The enclosure reaches 2,048 — a factor of 1,024, which is 2¹⁰ = (√2)²⁰ exactly.

The growth per step measures 1.4142137 against √2 = 1.4142136. That is not a fitted constant. It is the ratio of the side of the axis-aligned box around a square to the side of the square, at 45°, and it is where the whole effect comes from.

No rounding error is responsible for any of it. The loss is the shape of the representation — information about the tilt is discarded at every step — and a higher precision does not touch it.

The way that works #

Compute the answer in ordinary floating point, then prove a bound on it.

With R an approximate inverse, if ‖I − RA‖ < 1 then A is provably nonsingular and

‖x − x̂‖  ≤  ‖R(b − Ax̂)‖ / (1 − ‖I − RA‖)

with every quantity on the right evaluated in interval arithmetic with outward rounding, so the inequality survives the arithmetic that evaluated it. This is Rump’s method in its simplest form, and it is the shape every practical verified solver has: the floating-point computation does the work and the interval computation does the proof.

The floating-point half does not need to be careful. Its errors are what the bound is measuring, and a better solver makes the bound tighter, never truer.

What it does need is to be on the same machine, and the first version of this file was not. It solved in double and verified at 24 bits, producing bounds that were perfectly valid and six billion times larger than the error they bounded — because ρ was a 24-bit quantity and the error being bounded was a 53-bit one. A verified solver verifies the answer the machine produced; verifying a better answer than the machine can compute is a bound on nothing.

Checked against an answer that is known #

The test problem is the Hilbert matrix, whose exact solution exact.js computes in BigInt rationals with no rounding anywhere. So the bound is not checked against a better float — it is checked against the answer, which is the strongest available form of this claim.

At 24 significand bits:

The bound holds at both sizes where it exists, and it is tight — 23 times the error at n = 4 and 10 at n = 5. Not a factor of a million. A bound that is true and a million times too large would prove nothing anybody wanted, and the assertion requires the slack to be under 10⁴.

Its failure mode is a refusal #

The condition ‖I − RA‖ < 1 either holds or it does not. When it does not, the method returns nothing — not a wrong bound, not a wide one, not a warning.

On a site whose recurring finding is that wrong answers arrive looking exactly like right ones, that is worth more than it sounds. A small residual is not a small error is about an answer that looks fine and is not. Classical Gram–Schmidt returns a Q with an off-diagonal of 1.0 while every column is still a unit vector to 10⁻¹². Lanczos returns the same eigenvalue five times, each to eight digits.

This is the one method on the site that cannot mislead, and the price is that it frequently declines. assertItDeclinesRatherThanLies checks both halves: every bound it returns is true, at every precision, and it does decline somewhere in the range.

And the boundary is a number this site already has #

Where it declines is not arbitrary. Across five precisions and six sizes, every verified case has κu below 0.237 and every declined case has κu above 0.891.

The boundary is κu ≈ 1, and that is not a coincidence. ‖I − RA‖ is of the size of κ times the unit roundoff, because R is an inverse computed to that precision — so the condition ‖I − RA‖ < 1 is the condition κu < 1 with a modest constant in front.

Which is the same threshold where the hardware went measures for iterative refinement: three formats straddling it at κ = 10³, with bfloat16 at κu = 3.91 failing to recover and fp32 at κu = 10⁻⁴ matching a double solve.

So one number decides two apparently unrelated questions — whether refinement converges, and whether a bound can be proved at all. Both are asking whether an approximate inverse is close enough to an inverse for a Neumann series to converge, which is the same question in two disguises. The assertion states it as a separation rather than as a value, and excludes the transition region, which is the bracket discipline the mixed-precision field established for exactly this shape of threshold.

What proving costs #

Three things, and none of them small.

The arithmetic. Every interval operation is two to eight floating-point operations, and forming ‖I − RA‖ is an n³ matrix product done in intervals. Verification costs several times the solve it verifies.

An approximate inverse. R is n² numbers and computing it is another n³, where the solve itself needed only a factorisation. Verified computing is not a cheap addition to a solve; it is a second computation of comparable size.

And a precision the machine will round outward at, which is the one JavaScript cannot supply and which is why everything here runs at a simulated 24 bits. The refusal list includes a figure drawn at 53 bits, required to fail, because at binary64 the directed modes do nothing and every interval would be degenerate — a rigorous method with no rigour in it, which is the failure that would look most like success.

What the boundary looks like as a table #

The separation is clean enough to be worth setting out, because “κu ≈ 1” is a summary of twenty-five individual outcomes.

At each of five precisions, the largest Hilbert size at which a bound could be proved:

The boundary moves right with the precision and it moves by about the amount κu = 1 predicts: eight more bits buys about two more Hilbert sizes, because the Hilbert condition number grows by roughly a factor of thirty per size and 2⁸ is 256.

That the boundary is monotone in the precision is asserted rather than observed. A precision that verified less than a coarser one would be a bug in the interval arithmetic rather than a property of the problem, and it is exactly the sort of thing a sign error in the directed rounding would produce.

Two things this method does not claim #

Not that the answer is accurate. The bound at n = 5, 24 bits is 2.14·10⁻¹ on a solution whose entries are 1 to 5. That is a rigorous statement that the answer is wrong by less than about 4%, and it is a rigorous statement about a fairly bad answer. Verification says how wrong, with certainty; it does not make anything right.

And not that a refusal means the problem is unsolvable. At n = 6, 24 bits the method declines, and a double-precision solve of that system returns eleven correct digits. The refusal says this arithmetic cannot prove a bound on the answer it produced — not that no answer exists and not that this one is bad.

Both are worth stating because the natural reading of a rigorous method is stronger than what it delivers, and the gap between the two is where the practical disappointment lives. What is on offer is certainty about an interval, and both the certainty and the interval have to be looked at.

The one it cannot mislead about #

Set against that, the property is genuinely unusual on this site.

Every other method in this collection has a failure mode that looks like success. An elimination without pivoting reproduces its matrix to 3.8·10⁻¹⁷ and returns an answer wrong in the fifth digit. A sketch returns a confident low-rank approximation of a matrix with no low-rank structure. Strang’s preconditioner is indefinite at moderate size and produces a converging iteration that is slower than doing nothing.

In every one of those, the wrong answer arrives with the same shape and the same plausibility as the right one, which is why this collection prints residuals on everything.

A verification either proves a bound or returns nothing. There is no version of it that returns a bound the answer violates, because the bound is computed with outward rounding from quantities that are themselves enclosures. That is a different relationship between a method and its user, and it is worth one essay in twelve fields.

What is left #

Interval Newton and Krawczyk, which prove the existence and uniqueness of a solution rather than bounding an approximate one — a genuinely stronger claim, and the one that makes verified computing a subject rather than a technique.

The wrapping effect’s real remedies, which are representations other than boxes: zonotopes, affine arithmetic, Taylor models. Each keeps some of the correlation between components that a box discards, and each has its own version of the same failure further along.

And the two-run bracket this site already had. The rounding-mode essay computes a sum twice, once rounding up and once down, and reports the gap as a bracket on the answer. That is interval arithmetic with one operation in it and no propagation — and the whole difference between it and this essay is what happens to the width when the operations compound.