Numerical Illustration versus Mathematical Certificate

Conceptual map

V-04.01Exact arithmetic
V-04.02Verified intervals
V-04.03Rank and subspace checks
V-04.04Limits of finite approximation
V-04.05Optimization certificates

1. Computations have different logical roles

A numerical output can illustrate behavior, refute a universal claim, or certify a bounded statement. The role depends on arithmetic and error control.

A floating-point example illustrates a mechanism when its result is stable to precision and implementation choices. An exact rational or symbolic witness can refute a universal statement after all premises are verified. A positive certificate establishes a claim over a set only when interval enclosures, analytical error bounds, exhaustive finite search, or primal-dual inequalities cover that set.

Definition 1 · Verified enclosure

An interval $$I$$ is a verified enclosure for real quantity $$q$$ when the arithmetic procedure proves $q\in I$ , including rounding error and input uncertainty under the stated model. Printing many digits is not an enclosure.

2. Exact rank and numerical rank answer different questions

For rational $\varepsilon$ , consider

\[A_{\varepsilon }=\begin{bmatrix}1 & 1 \\ 1 & 1+\varepsilon \end{bmatrix}, \quad \operatorname{det}(A_{\varepsilon })=\varepsilon .\](1)

At $\varepsilon=10^{-12}$ , exact arithmetic certifies rank two. A numerical routine using a singular-value threshold above roughly $5\times 10^{-13}$ can report numerical rank one because the smaller singular value is of that order. Both statements can be correct under their declared definitions. The audit records scaling, norm, precision, threshold, and singular values.

An interval determinant contained entirely in (0, $\infty$ ) certifies nonsingularity. An interval containing zero leaves the sign unresolved; it does not certify singularity. Increasing precision or deriving a sharper enclosure may resolve the case.

3. Primal and dual witnesses bound optimization error

Consider the linear program min $x_{1}+x_{2}$ subject to $x_{1}+2x_{2}\ge1$ and $x\ge0$ . Its dual is max $\lambda$ subject to $0\le \lambda \le1$ and $2\lambda \le1$ . The primal point (0,1/2) and dual point $\lambda=1/2$ are feasible and have equal value 1/2.

Proposition 1 · Feasible primal-dual gap certificate

For any minimization linear program and its dual maximization problem, a primal-feasible point with value $$p$$ and dual-feasible point with value $$d$$ satisfy $d\le v^{*}\le p$ . Hence $$p-d$$ bounds the primal objective error; equality certifies optimality.

Proof. Weak duality gives every dual-feasible value as a lower bound for every primal-feasible value. Taking the infimum over primal-feasible points and the supremum over dual-feasible points yields the two inequalities. If one feasible pair has equal values, both equal the optimum. ∎

Solver status without feasibility residuals provides weaker evidence. For approximate witnesses, residual bounds and objective-coefficient norms must translate numerical feasibility into rigorous bounds.

4. Finite grids do not certify unsearched continua

Failure case · No violation found on a dense grid

A narrow violation can lie between grid points. A grid certifies the continuum only when a modulus of continuity or interval method bounds behavior inside every cell.

Root-finding needs a bracket and continuity for an existence certificate; Newton convergence from one start is a local diagnostic. Rank changes discontinuously at zero singular values. Eigenvectors become unstable as a spectral gap closes, even when eigenvalue sets remain stable. Optimization duality can fail under malformed signs or unsupported solver transformations. Exact rational arithmetic can become expensive, and decimal input must be mapped to exact rationals or input intervals deliberately. Overflow, underflow, cancellation, and nondeterministic parallel reductions are part of the error model.

5. Implementation, exercises, and sources

Classify each computation as illustration, counterexample, or certificate. Use exact arithmetic for small rational witnesses, intervals for bounded real calculations, and primal-dual residuals for convex programs. Print precision, tolerance, norm, condition estimate, feasibility residuals, and solver termination. Recompute sensitive quantities with an independent method.

Download the volume verification script →

Exercises

Compute the determinant and exact rank of (1) for $\varepsilon=0$ and $\varepsilon=10^{-12}$ .
Verify the primal and dual witnesses and derive their objectives.
Give a Lipschitz condition under which a grid bounds the maximum error between nodes.

Partial solutions

1. Rank is one at zero and two for every nonzero rational $\varepsilon$ . 2. The primal constraint binds and the dual upper constraint $2\lambda \le1$ binds; both objectives equal one half. 3. If $\lvert f(x)-f(y)\rvert \le L\lvert x-y\rvert$ and mesh width is $$h$$ , every point lies within $$h/2$$ of a node in one dimension, giving an $$Lh/2$$ envelope.

Nicholas J. Higham, Accuracy and Stability of Numerical Algorithms.Floating-point error and conditioning.
Ramon E. Moore, R. Baker Kearfott, and Michael J. Cloud, Introduction to Interval Analysis.Verified enclosures.
Stephen Boyd and Lieven Vandenberghe, Convex Optimization, Chapter 5.Duality and residual certificates.

6. Audit checkpoint

Logical role, exact versus floating input, precision, rounding mode, interval inclusion, determinant enclosure, singular values, numerical-rank threshold, norm, scaling, spectral gap, grid modulus, root bracket, primal and dual feasibility, complementarity, objective gap, solver transformations, overflow, cancellation, and independent recomputation.

7. Scope boundary

The chapter covers small exact witnesses, interval logic, and linear-program certificates. Formal verification of large nonlinear solvers and certified global optimization require specialized software.