Where the box is cut

Proving the answer is in the box established the only computation on this site that proves anything. The Krawczyk operator, handed a box, returns one of three verdicts: unique — there is exactly one root in here; none — there is no root in here at all; or inconclusive — nothing can be said. The first two are statements about infinitely many points reached by finitely many operations, and the third is the honest outcome that makes the other two worth having.

What that essay did not do is find anything. The box has to be supplied.

The search #

Start with one box covering the region of interest and ask the operator.

On none, discard the box and never look at it again. That is the pruning, and it is what makes the search finite rather than a grid: a region proved empty stays proved however fine the search becomes elsewhere.

On unique, record it and stop subdividing. Everything inside is settled — one root, and it is in there.

On inconclusive, cut the box in half along its widest side and ask about both halves.

At the end the region is covered by boxes each carrying a proof, plus whatever could not be decided before the stopping width was reached — and those are returned rather than discarded, because a search that reported only what it proved would report a subset of the roots as though it were all of them.

What it settles #

The circle-and-diagonal problem — x² + y² = 4 and x = y, whose roots are (√2, √2) and (−√2, −√2) exactly — over the square [−3, 3]², to a stopping width of 10⁻⁴:

The whole square is covered, every part of it carries a proof, and it took 87 evaluations of a 2×2 operator.

Four things are checked against the exact roots rather than against the method’s own output: each root is inside exactly one verified box; no verified box contains both; no box proved empty contains either; and the search terminates rather than exhausting its evaluation budget. The third is the one worth having — a search that pruned a box containing a root would report a subset of the answer with exactly the same confidence as the whole of it.

And then the subdivision rule loses a root #

Change the problem to two roots a distance δ apart — the construction the interval field uses to measure separation, with the only difficulty in the gap — inside the box [0, 2].

The roots are at x = 1 and x = 1 + δ. A midpoint bisection of [0, 2] cuts at exactly 1.

Nothing is verified, at any separation, at any depth. The search spends 163 evaluations at δ = 0.1 to say so, and its answer — six undecided boxes and no roots — is not wrong, it is empty.

The reason is one line. The first cut lands on the root; every later cut inherits that boundary; so the root is on the edge of every box the search ever asks about. Krawczyk’s verdict requires the image K(X) to lie strictly inside X, and a root on the boundary cannot produce that.

The operator is not at fault, and that is asserted beside it: a box of half-width 0.02 centred on the same root is verified immediately.

Cutting at 0.485 #

The repair is to cut somewhere other than the middle, and this is the reason it is standard.

Both roots verified at every separation, nothing left undecided, and fewer evaluations — 45 against 163, a factor of 3.6, because a search that verifies stops subdividing and a search that never verifies does not.

And on a problem whose roots are nowhere near a bisection boundary it changes nothing at all: the circle problem’s counts under the two rules are identical — 87 evaluations, 2 verified, 42 empty. A repair that is free where it is not needed is worth the assertion, and it has one.

What kind of defect this is #

Worth naming, because the site has met the shape before and not in this form.

It is not a numerical failure. Nothing overflows, nothing cancels, no condition number is large, and every operation is exact in the sense interval arithmetic means. Running at higher precision changes nothing; running longer changes nothing; the tolerance is irrelevant.

It is not a defect of the operator either. The operator answers correctly about every box it is given.

It is a defect of the questions being asked — a search whose subdivision rule generates a set of boxes none of which can answer, on a problem whose only special feature is that one of its roots is at a dyadic rational. And the failure is silent: the search terminates normally, reports what it proved, and what it proved is nothing.

The nearest relative on this site is the block method that returns two copies of a triple eigenvalue — accurate eigenvalues, tight residuals, a genuine invariant subspace, and one copy missing with nothing in the computation to say so. Both are cases where the method succeeds at a smaller problem than the one it was given.

What the operator is being asked #

Worth spelling out, because the search’s cost is a count of these and nothing else.

One evaluation is: invert the Jacobian at the box’s midpoint in ordinary floating point, to get an approximate inverse C; evaluate the Jacobian over the whole box in interval arithmetic, which is where the outward rounding lives; form I − C·F′(X) as an interval matrix; and check whether the image x̂ − C f(x̂) + M(X − x̂) lies strictly inside X or misses it entirely.

Two things about that are worth noticing.

The floating-point inverse cannot make the answer wrong. C is a preconditioner: a bad one makes the test fail more often and cannot make a success untrue, because the containment is checked in interval arithmetic whatever C was. That is the same division of labour the verified-bound essay states for its own R, and it is why a proof can rest on a computation nobody proved anything about.

And the interval evaluation is where the width goes. The Jacobian over a box of width w is an interval of width proportional to w, so halving a box halves the overestimation — which is why subdivision works at all, and why a region where the overestimation is not shrinking is a region a subdivision search cannot settle.

On this problem there is no such region: the search terminates with nothing undecided. On a problem with a singular Jacobian inside the region of interest there would be, and the honest form of the search’s output is the list of undecided boxes rather than a verdict about the whole square.

What it does not prove #

Three limits, each of which a reader would otherwise supply for themselves and get wrong.

It does not prove there are no other roots outside the box. Everything here is a statement about [−3, 3]², and the problem has no roots outside it, which is known from the algebra rather than from the search.

It does not prove the roots are simple in any sense the search checked. Uniqueness inside a box is what the operator returns; a double root would fail the test rather than be reported as double, and the search would return an undecided box where the root is.

And it says nothing about conditioning. A verified box of width 0.375 around a root is compatible with a well-conditioned root and an appalling one; what separates them is how the box’s width scales with the precision, which is the measurement the interval field’s own two boundaries are about.

Each of those is a question the method could be extended to answer, and none of them is answered by the output as it stands — which is the difference between a proof and a report.

The cost of getting close #

krawczyk.js measured the verified width as exactly half the distance to the second root, across four decades of separation. In a search that becomes a depth.

Eight or nine levels a decade, and forty extra evaluations a decade against a base of forty-five — additive in the number of decades rather than multiplicative, which is what makes a proof about two roots a thousandth apart affordable at all. Halving a box’s width costs one level, and one level of a two-dimensional search costs two boxes at the frontier rather than twice everything.

That is the practical case for pruning stated as a number: without it the same depth would cost 2²⁷ boxes rather than 125.

Why the pruning is what makes it finite #

The three verdicts are not symmetric in what they buy, and the asymmetry is the whole reason a search of proofs is affordable.

Unique ends a branch and settles a small region. Inconclusive ends nothing and doubles the work. And none ends a branch and settles a region that is usually large — the boxes proved empty on the circle problem cover almost the whole square, and each of them was decided by a single evaluation on a box that was still big.

That is the arithmetic of pruning: a search that could only verify would have to subdivide the entire square to its stopping width, which at 10⁻⁴ over [−3, 3]² is 3.6·10⁹ boxes. The search does it in 87, and the ratio is what the empty verdict is worth.

It is also why an interval method is worth more than a grid of Newton starts. A grid samples; it can report where it found roots and can never report that there are none anywhere else. The three-verdict structure turns the second question — the one that actually matters when a system’s root count is unknown — into the cheap case.

What a verified box is not #

The proof is about containment, and containment is weaker than location.

A verified box says there is exactly one root in here. It does not say where in here, and at a stopping width of 10⁻⁴ the verified boxes on the circle problem have width 0.375 while their centres are 0.144 from the roots. Both numbers are correct and the second is not a bound the method offers — what it offers is the first.

So a verified box is a starting point for a Newton iteration rather than a substitute for one. The combination is what a verified solver actually does: the search establishes that there is one root in a region and no roots outside it, and a floating-point iteration inside the region finds it to the last bit — with the containment proof doing the part no residual can, which is the uniqueness claim the interval field is about.

The three verdicts, as a budget #

One more way to read the first table, and it is the one that says what the method costs.

Of the 87 evaluations, 44 produced a verdict — 2 unique and 42 empty — and 43 produced nothing and were subdivided. So half the work of a proof search is spent on boxes that decide nothing, and that is not waste: an inconclusive verdict on a large box is what a subdivision is, and the subdivided boxes are the internal nodes of a tree whose leaves are the proofs.

The ratio is the thing to watch when the method is applied somewhere new. A search where nine evaluations in ten decide nothing is one whose boxes are being cut in a direction that does not help, or whose interval arithmetic is overestimating faster than the bisection shrinks it — and both are visible in that one number without knowing the answer.

Here it is 43 to 44, and it is roughly that at every square the slider reaches, which says the tree is balanced: the pruning keeps up with the subdivision.

The rule in one line #

Cut boxes at 0.485 of their width rather than at 0.5.

It is a strange-looking piece of advice and the measurements make it a short argument. A midpoint rule generates boundaries at dyadic rationals — 1, 1/2, 3/2, 1/4, and so on — and any root at one of those points is on the boundary of every box the search will ever ask about. Dyadic rationals are exactly the numbers that turn up in constructed problems, in symmetric systems, in equations with unit coefficients, and in every test case anybody writes by hand.

So the failure mode is not rare in the space of problems people actually run: it is concentrated exactly where the problems people write down live. Perturbing the split point removes it at no cost — measured at no cost, on a problem where it was not needed — and the search gets faster where it was.

What the drag does, and what it was drafted as #

The slider is the square: the search is run over [−2, 2]², [−2.5, 2.5]², and so on to [−4, 4]², and both roots are verified and nothing is left undecided at every setting. What moves is the cost, and it does not move the way a reader expects.

[−3, 3]² costs more than half as much again as [−4, 4]², which contains it. That is not a wobble in a trend; the largest number in the sweep sits in the middle of it, at nearly twice its neighbours, and it is the square every other figure in this essay is drawn over.

The explanation is the essay’s own subject. Cut the boxes at 0.45 instead of 0.485 and the 87 becomes 23, while the two largest squares become the expensive ones at 55 and 59. The anomaly follows the cut rule rather than the region, so what is being measured is how many boxes end up straddling the line the Jacobian is singular on — the one place the Krawczyk operator can neither verify nor refute, where the only move left is to subdivide. Where that line falls relative to a box’s cuts is a property of the box’s corners. It has nothing to do with its area.

So the cost of a proof search is not a function of how much plane it is asked about, and the assertion that carries this is written in both directions, because “cost grows with area” and “cost is unrelated to area” are both wrong: the sweep is non-monotone under one cut rule and reordered by another. Two refusals sit behind it — one fed the claim that a larger square costs at least as much as a square inside it, and one fed the claim the slider used to make.

Because this figure was drafted with a different slider, over the stopping width, and a note saying that both roots are verified at every setting while the verified boxes shrink towards them and the evaluation count grows slowly. The first half was true and the rest was not: all five settings drew the same picture, down to the byte.

The reason is in the table this essay already printed. Nothing on this problem is ever undecided — 2 verified, 42 empty, 0 undecided — so no box is ever still open when the stopping width is reached, and the parameter never binds. A stopping width is a bound on how finely a search may subdivide while it still has something to subdivide, and on a problem the operator settles completely it is inert. It would bind on the close-pair problem, where the midpoint rule leaves six boxes undecided for ever, and that is the figure two sections up.

Nothing caught it but the build, which renders every frame and refuses a figure whose frames are all the same picture. That check now runs in this site’s own gate as well, forty seconds against seven minutes, because a drag block is a claim — this parameter changes the picture — and a claim on this site is given a test it could fail.