Numerical Linear Algebra
where the algebra stops being the arithmetic
The arithmetic underneath

Proving the answer is in the box

Every other method here computes a number and estimates how wrong it is. This one returns a verdict: there is exactly one solution in this box, or there is none, or — the honest third outcome — nothing can be said. Two of the three are proofs about infinitely many points from finitely many operations.
17 min read 8 figures Exact ground truthAssertions that rejectPrecision as the knob

Worth reading first: A bound that is proved.

Every method on this site so far computes an answer and then says something about how wrong it is. The strongest of them, the verified bound, says it rigorously: given an x̂ that something else computed, ‖x − x̂‖ is certainly below this number, or — when ‖I − RA‖ ≥ 1 — the method declines and returns nothing at all.

That is a statement about an approximation. This essay is about a different kind of statement, and it is the only one of its kind here:

there is exactly one solution in this box.

Not “the computed one is accurate to”. Not “the residual is small”. A quantified claim about a region of the plane, containing uncountably many points, established by a finite computation in floating-point arithmetic.

The Krawczyk operator on a box of half-width 0.4Two rectangles in the plane. The outer one is the box handed in; the inner one is K(X), the image the operator returns; and the marked point is the root (√2, √2), known in closed form. The image is narrower than the box — 0.2263 against 0.8 — and the verdict is: exactly one root.11.522.511.52xyexactly one roota verdict, not a bound‖I − C F′(X)‖0.28width of X0.8width of K(X)0.23strictly inside is a proofand overlapping is nothing at all
Fig. 1 The Krawczyk operator on a box of half-width 0.4 about a point near (√2, √2). The outer rectangle is the box handed in; the inner dashed one is K(X), the image the operator returns; the marked point is the root, known in closed form. Strictly inside is a proof of existence and uniqueness. Drag the half-width: both ends of the slider fail, for different reasons.

The operator

For a system f(x) = 0 on a box X with midpoint x̂ and C an approximate inverse of the Jacobian at x̂:

K(X)  =  x̂ − C·f(x̂)  +  (I − C·F′(X))·(X − x̂)

where F′(X) encloses the Jacobian over the whole box rather than evaluating it at a point. Two theorems:

  • K(X) ⊆ int X ⟹ f has exactly one zero in X, and Newton from any point of X converges to it;
  • K(X) ∩ X = ∅ ⟹ f has no zero in X at all.

Every operation in K is evaluated with outward rounding, so the conclusion is a statement about the real function rather than about its floating-point shadow. interval.js supplies that arithmetic and the genuine directed rounding underneath it — which JavaScript does not have, and which this site simulates at any precision from eleven bits up, because binary64’s directed modes are no-ops in a language with no access to the rounding-mode register.

C is computed in ordinary floating point. Its quality decides how often the test succeeds and never whether a success is true, which is the same division of labour the verified bound states for its R. That is worth being clear about because it is the property that makes the method usable: the expensive, delicate, approximate part of the computation cannot make the answer wrong, only unavailable.

Three verdicts, and the third is not a failure

The test problem is x² + y² = 4, x = y, whose roots are (√2, √2) and (−√2, −√2) exactly — so every claim below is checked against a number rather than against a better approximation, which is the exact ground truth habit this site applies wherever it can be had.

box verdict what it means
half-width 0.05–0.4 about the root unique exactly one root in there, proved
half-width 0.05 about (3, 3) none no root anywhere in there, proved
half-width 1.5 about the root inconclusive nothing is claimed

The third row is the outcome to be careful about, and it is where the mistakes get made. Inconclusive does not mean no root: the box in that row contains the root, and the operator declines to say so because the Jacobian varies too much across a box that wide for the image to land strictly inside. One of this essay’s published refusals is exactly that misreading — fed a wide box containing the root, and required to reject the claim that an inconclusive verdict is an exclusion.

The contraction that decides it is ‖I − C F′(X)‖, and it is reported on every figure: 0.035 at a half-width of 0.05, 0.28 at 0.4, and 1.0 at the boxes that fail. The operator contracts when that quantity is below one, which is the same condition, in the same shape, as the verified bound’s ‖I − RA‖ < 1 — and it is worth noticing that the whole of verified computing runs on one inequality.

Two boundaries, and only one of them is the arithmetic

A box can be too wide to verify. It can also be too narrow — which the first version of this measurement did not expect and which is the more interesting of the two.

The widths a proof is available at, against the precisionTwo boundaries against the number of significand bits, on a logarithmic vertical axis, with the band between them shaded. The narrow boundary runs from 0.00162 at 12 bits to 3.33·10⁻¹⁶ at 53, a small multiple of u at each. The wide boundary is 1.414214 at every precision — which is √2, the half-width at which the box first touches the line where the Jacobian is singular.9172533414910⁻¹⁶10⁻¹³10⁻¹⁰10⁻⁷10⁻⁴10⁻¹significand bitsbox half-widthwidest provablenarrowest provableutwo boundaries, two causesnarrowest, in units of u3widest, at 53 bits1.4√21.4one end is the arithmeticthe other is the function
Fig. 2 The band of half-widths that can be settled, at six precisions. The narrow boundary is a small multiple of the unit roundoff and falls with the precision through thirteen orders of magnitude. The wide one is 1.41 at every precision — the same number to three digits at 12 bits and at 53.
significand bits u narrowest provable in units of u widest provable
12 2.4·10⁻⁴ 1.6·10⁻³ 6.6 1.410
16 1.5·10⁻⁵ 1.2·10⁻⁴ 7.9 1.414
24 6.0·10⁻⁸ 3.8·10⁻⁷ 6.4 1.4142
32 2.3·10⁻¹⁰ 9.2·10⁻¹⁰ 4.0 1.41421
53 1.1·10⁻¹⁶ 3.3·10⁻¹⁶ 3.0 1.4142135623730947

The narrow end is the arithmetic. A box has to be wide enough to contain the correction the operator adds, and that correction carries the rounding in f(x̂); below a few multiples of u there is no room and the image spills out the bottom. So how tightly a root can be pinned down is a statement about the precision, and it improves by thirteen orders of magnitude across the range drawn.

The wide end is the function, and it does not move with the precision at all — 0.3% across four decades of u, against thirteen orders of magnitude at the other end.

And the value it does not move from is worth pausing on. At 53 bits the widest verifiable half-width is 1.4142135623730947, which is √2 to every digit. This problem’s Jacobian is [[2x, 2y], [1, −1]], singular exactly where x + y = 0, and the ∞-norm distance from (√2, √2) to that line is √2. The operator verifies precisely up to the point where the box could contain a singular Jacobian, and not a fraction further.

That is asserted rather than admired — a coincidence to fifteen digits is a mechanism — and it is the sharpest available statement of what the method is doing: it is not estimating anything, it is asking whether a contraction exists on the box, and a contraction exists exactly as far as the derivative stays away from zero.

Uniqueness, which is what nothing else offers

Newton’s method converges to a root and says nothing about how many there are. That is not a criticism; it is what the method is.

Take two roots δ apart, run Newton from either side, and read what it reports:

start converges to residual
(0.9, 0.2) 1.000000 0
(1.05, −0.3) 1.001000 1.1·10⁻¹⁹

Two different roots, residuals at or below the level of rounding, and nothing in either run indicating that the other exists. A reader who ran only the first would have an answer with a perfect residual and a wrong picture of the problem.

The widest box a uniqueness proof is available forVerified half-width against the distance between two roots, both axes logarithmic. The measured widths are 0.05, 0.005, 5·10⁻⁴, 5·10⁻⁵ at separations of 0.1, 0.01, 0.001, 10⁻⁴ — a ratio of 0.5000 at every one of them. The operator verifies exactly up to the point where the box would reach the second root, and a box containing both is refused.10⁻⁴10⁻³10⁻²10⁻¹10⁻⁴10⁻³10⁻²10⁻¹distance between the two rootswidest verified half-widththe separationverified widthuniqueness is a claim about a regionwidth ÷ separation at δ = 0.10.5width ÷ separation at δ = 0.010.5width ÷ separation at δ = 0.0010.5verified up to the second rootand refused past it
Fig. 3 The widest box the operator will verify, against the distance between the two roots. The measured widths are 5.0·10⁻², 5.0·10⁻³, 5.0·10⁻⁴ and 5.0·10⁻⁵ at separations of 10⁻¹ to 10⁻⁴ — a ratio of 0.5000 at every one of them, to four decimals. It verifies exactly up to the point where the box would reach the second root.

Exactly half the separation, across four decades. That number is not a tuning constant and nothing in the implementation knows about it: it falls out of the theorem, because a box of half-width r about one root reaches the other exactly when r ≥ δ, and the operator’s contraction fails as the second root enters — and the midpoint sits halfway, so the reachable half-width is δ/2.

So the method answers a question the residual cannot: is this the only one? And it answers it with a number that tracks the thing that makes the question hard.

What this is worth, and what it costs

The honest accounting, because a verdict is not free.

It is dear. Every operation is two floating-point operations with directed rounding, the Jacobian has to be enclosed over the box rather than evaluated at a point, and the whole thing is run in a simulated arithmetic here because the language has no directed modes. A verified solve is an order of magnitude more work than an unverified one, and that is before the search over box widths that finding a verifiable box requires.

It declines often. Three verdicts and one of them says nothing at all. On a wide box, on a box near a singularity, on a box narrower than a few multiples of u, the answer is no conclusion — and there is no partial credit available.

And what it buys is a different kind of sentence. Everywhere else on this site, an error bound is a statement about a computation: this algorithm, on this machine, produced something within this distance. Here the conclusion is about the problem: f has one zero in this region, whatever anybody computes. That distinction is the reason the field exists, and it is why the method’s failure mode is a refusal rather than a wrong answer — a property this site has now measured twice and values both times.

Where a bound can be proved, against κuEvery combination of 4 working precisions and 5 Hilbert sizes, placed by the product of the condition number and the unit roundoff. Filled marks are the cases where a bound was proved; open ones are the cases the method refused. The two sets separate at κu ≈ 1 — the largest verified is 0.24 and the smallest declined is 0.89 — which is the threshold iterative refinement's convergence sits at.10⁻⁵10⁻²10¹10⁴10⁷10¹⁰132129κ · usignificand bitsκu = 1a bound was provedthe method refusedit never returns a wrong boundlargest κu with a proof0.24smallest κu without one0.89cases refused, of the grid15a refusal is not a wide bound — it is no bound at alland it is the only failure mode here
Fig. 4 The other method of this kind, from the field’s own essay: a verified bound on the error of an approximate solution, with its boundary at κu ≈ 1 — everything verified below 0.237 and everything refused above 0.891. Both methods either prove or decline, and both have a boundary that can be measured rather than guessed at.

The one thing a proof cannot fix

It is worth saying plainly, because “verified” is a word that invites over-reading.

The theorem is about the function it was handed. If f is a model of something — a discretisation of a differential equation, a fit to measured data, an idealisation of a mechanism — then a proof that f has exactly one zero in a box says nothing whatever about whether the thing being modelled has one. The convection field has an essay’s worth of this: a scheme that solves its own system exactly while answering a different question from the one posed.

What verification removes is the arithmetic’s contribution to the doubt. That is a real contribution — this site has spent seventy essays measuring it — and it is one term of several.

A box rotated 20 times, and the smallest box containing itTwo widths against the number of rotations, on a logarithmic vertical axis. The set's width is a flat line, because a rotation is an isometry. The interval enclosure's climbs geometrically — by a factor of 1.4142 a step against a predicted √2 — and after 20 rotations it is 1024 times larger than the thing it encloses.036912151810¹10²10³rotationswidththe enclosurethe seta rotation is an isometrymeasured growth a step1.4√2, from the geometry1.4enclosure ÷ set after 201024no rounding error is responsible for any of thisa higher precision does not touch it
Fig. 5 Why interval arithmetic is not simply carried through an algorithm: an enclosure that grows by exactly √2 a rotation while the set it encloses does not move. The operator above avoids that by asking one question about one box rather than propagating an enclosure.
The proved bound against the error it bounds, at 24 significand bitsTwo curves against the Hilbert size on a logarithmic vertical axis: the error the computation actually made, which is known because the exact answer is the integers by construction, and the bound proved for it in interval arithmetic. The bound is above the error at every size, by 9.949 to 23.12 times. Past n = 5 the method refuses to return a bound at all.345678910111210⁻⁵10⁻³10⁻¹Hilbert size nerrorrefusedrefusedrefusedrefusedrefusedthe proved boundthe actual errorbound ÷ errorslack at n = 313slack at n = 423slack at n = 59.9the error is known, not estimatedthe exact answer is the integers 1 … n
Fig. 6 How tight the other verified method’s answer is when it succeeds: 23.1 times the true error at n = 4 and 9.9 at n = 5, against an exactly known integer solution. A verdict has no analogous number — it is true or it is not offered.
The width of a guaranteed bracket, and the error it guarantees, at 24 bitsTwo rising curves on logarithmic axes. The upper one, the bracket width, rises faster than the lower one, the actual error.10¹10²10³10⁴10⁻¹¹10⁻¹⁰10⁻⁹10⁻⁸10⁻⁷10⁻⁶10⁻⁵10⁻⁴10⁻³terms summedrelative widthbracket widthactual errora bound with no tolerance in itbracket contains the truth7width at 10,000 terms4.4·10⁻⁴error it bounds2.4·10⁻⁶every sum computed twice, up and downtrue at every size, useful at none of the large ones
Fig. 7 The arithmetic underneath all of this: the rounding modes that are useless singly and are the whole of interval arithmetic together. Everything in this essay is two computations, one rounding down and one rounding up.
Where a bound can be proved, against κuEvery combination of 4 working precisions and 5 Hilbert sizes, placed by the product of the condition number and the unit roundoff. Filled marks are the cases where a bound was proved; open ones are the cases the method refused. The two sets separate at κu ≈ 1 — the largest verified is 0.24 and the smallest declined is 0.89 — which is the threshold iterative refinement's convergence sits at.10⁻⁵10⁻²10¹10⁴10⁷10¹⁰132129κ · usignificand bitsκu = 1a bound was provedthe method refusedit never returns a wrong boundlargest κu with a proof0.24smallest κu without one0.89cases refused, of the grid15a refusal is not a wide bound — it is no bound at alland it is the only failure mode here
Fig. 8 The other boundary this field has measured, for comparison with the two above: κu ≈ 1, with everything verified below 0.237 and everything refused above 0.891. Both methods have a frontier that can be bisected for rather than guessed at.

What the operator is doing, term by term

The formula is three terms and each has a job, which is worth separating because the middle one is where the method’s only approximation lives.

x̂ − C·f(x̂) is a Newton step from the midpoint, computed in interval arithmetic. If f(x̂) were zero this term would be x̂ itself.

(I − C·F′(X))·(X − x̂) is the correction that makes the statement true over the whole box rather than at its midpoint. C is an approximate inverse of the Jacobian at one point; F′(X) encloses the Jacobian over every point of the box; and I − C·F′(X) measures how badly one stands in for the other.

And the verdict is a containment, not a comparison of numbers. The theorem needs K(X) strictly inside X — overlapping is not enough, and accepting overlap would turn a proof into a plausibility argument, which is the distinction this whole essay is about. That is one of the refusals the file runs: a box wide enough to reach both roots, with the claim that its verdict is unique, required to fail.

The quantity that decides everything is ‖I − C F′(X)‖, printed on every figure. Below one the operator contracts; at one it does not. The same inequality, in the same shape, decides whether the verified bound is available — there it is ‖I − RA‖ — and it is worth noticing that the whole of verified computing on this site runs on one number being below one.

Why the approximate inverse cannot make the answer wrong

C is computed in ordinary floating point, from the Jacobian at the midpoint, by this site’s own dense solve. Nothing about it is rigorous.

That is not a gap in the argument, and the reason is structural. C appears inside an expression that is evaluated with outward rounding, so whatever C is, the interval K(X) certainly contains the true image of the map it defines. A bad C makes I − C·F′(X) large, which makes K(X) wide, which makes the containment fail — and a failure is inconclusive, which claims nothing.

So the division of labour is: the approximate computation decides how often the method can answer, and the interval arithmetic decides that an answer is true. That is the same division verifiedBound states for its R, and it is why both methods can use a fast, delicate, unverified computation in their innermost step without weakening what they prove.

The three verdicts are not a taxonomy for its own sake; they are exactly what a search over a region needs.

Subdivide a region into boxes. Every box proved empty is discarded and never looked at again. Every box proved to contain exactly one root is recorded, with a certificate. Every inconclusive box is subdivided and the process repeats — and the narrow boundary measured above is where that recursion has to stop, because below a few multiples of u no box can be verified however small the subdivision gets.

That procedure is what interval branch-and-bound is, and it is how a code finds all the roots in a region rather than certifying one at a time. Nothing here builds it. What this essay supplies is the step it is made of, with both of its boundaries measured — which is the part that decides whether the search terminates and what it costs when it does.

What is left

Interval Newton with extended division, the operator this one is usually introduced beside. When the Jacobian enclosure contains zero, the division is extended to produce a pair of intervals, and the method splits the box rather than declining — which turns verification into a search and is how a real code finds all the roots in a region rather than certifying one at a time.

Branch and bound over a region, which is that search: subdivide, discard the boxes proved empty, verify the ones that contract, and continue on the rest. The three verdicts here are exactly the three outcomes that search needs, which is why the operator is stated with all three rather than as a test.

And the preconditioner C, which here is the inverse of the Jacobian at the midpoint and is the only design choice in the method. For a badly scaled or nearly singular system it is the difference between a verdict and a shrug, and the literature on choosing it is as large as the literature on choosing a preconditioner for an iterative solve — which this phase has also measured, in a field that would not have thought itself related.

Where this goes next

10⁻⁹10⁻⁶10⁻³110³10⁶13212937κ · usignificand bitsκu = 1a bound was provedthe method refusedit never returns a wrong boundlargest κu with a proof0.45smallest κu without one0.89cases refused, of the grid13a refusal is not a wide bound — it is no bound at alland it is the only failure mode here A bound that is proved Every error statement on this site so far is a measurement of one run. Interval arithmetic makes a different kind of claim — the answer lies in this set, for this input, with no probability attached — and its failure mode is that it returns nothing at all. On a Hilbert system it proves a bound 23 times the error it bounds, and one size later it refuses. H13 x = b, b formed exactly so that x = (1, 2, …, 13)12345678910111213exact1.00002.00003.00133.97865.18864.993010.46720.048921.2657-2.575319.21478.906013.5113computed6.6 correct digits4.8 correct digits3.4 correct digits2.3 correct digits1.4 correct digit0.8 correct digitno correct digitsno correct digitsno correct digitsno correct digitsno correct digits0.6 correct digit1.4 correct digitbackward error2.2·10⁻¹⁷κ = 1.7·10¹⁸The algorithm solved a neighbouring problem perfectly. That problem's answer is this one.right-hand side built in BigInt rationalsthe truth is known An answer that is known Almost every demonstration of numerical error estimates the error by computing the same thing more carefully. The Hilbert matrix does not need that: its inverse is a closed form in integers, so the true answer is available exactly and the error is measured rather than approximated. 110²10⁴10⁶10⁸10¹⁰10¹²10¹⁴10⁻¹⁷10⁻¹⁴10⁻¹¹10⁻⁸10⁻⁵10⁻²10¹condition number κ(A)relative errorforward errorbackward errorpredicted: κ · u8×8, 20 seeds per κ; dashed is the worstthe problem worsens, not the method A small residual is not a small error Substituting the answer back and finding that it fits is the most natural check there is, and it verifies the wrong thing. A residual of 10⁻¹⁷ is entirely compatible with an answer whose second digit is wrong.

Shares its objects with

Essays that name at least two of the same things, and that neither author linked.

Named objects

A flat tag is an object no other essay names yet.

Directed roundingExistence and uniquenessInterval arithmeticJacobianKrawczyk operatorNewton iterationUnit roundoffVerified computing