Proving the answer is in the box

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 operator has three verdicts and the box’s size chooses between them, with a definite answer at each end and no conclusion in between.

Across half-widths of 0.02, 0.05, 0.1, 0.2, 0.4, 0.8, 1.4 and 2 the verdicts are no root, no conclusion, exactly one root, exactly one root, exactly one root, exactly one root, no conclusion, no conclusion. A window of four stops in the middle where the operator proves what it is for, a proof of absence below it, and silence above.

The contraction number is exactly proportional to the box. It reads 0.0141, 0.0354, 0.0707, 0.1414, 0.2828, 0.5657, 0.9899 and 1.4142 over the eight — 0.7071 times the half-width at every one, because F′ is being evaluated over an interval whose width is the box’s and C is fixed.

And the ratio of the image’s width to the box’s is the same number: 0.01414, 0.03536, 0.0707, 0.1414, 0.2828, 0.5657, 0.99 and 1.414. So one quantity decides both halves of the test, and the two ends fail for different reasons — at half-width 2 the contraction number is 1.414 and the operator is not a contraction at all, while at 1.4 it is 0.9899 and the failure is containment: an image 2.772 wide inside a box 2.8 wide has nowhere to sit unless it is also centred, and it is not.

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.

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 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 same knob the format itself is, turned the other way.

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:

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.

Exactly half the separation, across four decades. That number is not a tuning constant and nothing in the implementation knows about it. The obvious reading is that the box stops when it reaches the second root — but a box of half-width r centred on one root reaches the other when r ≥ δ, not δ/2, and the factor of two has to come from somewhere. It comes from the same place the √2 above did.

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 — which turns out to be the same thing in both measurements.

One boundary, not two #

The essay has now measured the wide boundary twice and explained it twice, and the two explanations are the same explanation.

On the circle problem the boundary is √2, and the reason given is that the Jacobian [[2x, 2y], [1, −1]] is singular on x + y = 0, whose ∞-distance from the root is √2. On the close-pair problem the boundary is δ/2, and the reason given is the second root — which is δ away, not δ/2.

Look at where that problem’s Jacobian is singular. It is [[2x − 2 − δ, 0], [0, 1]], and it degenerates at x = 1 + δ/2, which is exactly halfway between the two roots. That is not a coincidence of this contrivance: between two simple roots of a smooth function the derivative has to vanish somewhere, and for a quadratic it vanishes at the midpoint. The critical point arrives before the second root does, and it is the critical point that stops the contraction. The second root is never reached by any verifiable box and has nothing to do with the boundary.

So one sentence covers both: the widest verifiable half-width is the ∞-norm distance from the box’s centre to the set where the Jacobian is singular. Which is testable by moving that set, so it was tested. A circle of radius R puts its root at (R/√2, R/√2) and leaves the singular line at x + y = 0, so the prediction is R/√2:

Sixteen digits, across a factor of sixteen in the geometry, and the close-pair problem gives 1.000000 against δ/2 at every one of its four separations. Nine cases, two problem families, one number.

That is a better statement of what the operator is than either half was. It is not testing whether the box contains another root, and it is not testing anything about the function’s values: it is asking whether I − C·F′(X) is a contraction, which fails precisely when the enclosed Jacobian can be singular, which happens precisely when the box reaches the singular set. Everything the wide boundary does is a statement about the derivative and none of it is a statement about the roots.

It also makes the uniqueness result stronger rather than weaker. The reason a verified box can never contain two roots is not that the operator checks for a second one. It is that any box containing two roots contains the critical point between them, and no box containing a critical point contracts. The uniqueness is a corollary of the contraction rather than a separate property, which is why it comes free and why a residual cannot supply it: a residual is evaluated at a point and the boundary is a fact about a derivative over a region.

assertTheWideBoundaryIsTheDistanceToTheSingularJacobian holds the whole of it, on both families, and would fail if either boundary stopped tracking its singular set — which is the kind of thing a change to the interval arithmetic could break silently, since the verdicts would all still be true.

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.

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.

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.

Three outcomes and a search #

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.

A closed form that is a poor solver and a good enclosure #

A formula whose products are named in advance is a bad computation and a fine object to bound with. Cramer’s rule is the clearest case: unusable in floating point and perfectly serviceable in interval arithmetic.