The driver does the search at run time with the compiled isolator. The witness it emits is what the kernel re-checks, and that witness is a fixed conjunction of strict comparisons between exact dyadics, not a replay of the search. The Newton-Kantorovich atom witness is three such comparisons on the square itself:
Newton-Kantorovich contraction witness on the closed square s itself
(sup norm), with r = 2^{−s.prec} the half-width and y, z₁, z₂ the exact
dyadic bounds:
0 < normSq c₁ ∧ y + z₁·r + z₂·r²/2 < r ∧ z₁ + z₂·r < 1.
Implies (Mathlib companion): p has exactly one root in the closed square,
it is simple, and it lies in the open square.
The Pellet form is the analogous root-count inequality on the circumscribed disc, at three radii. Either way the kernel cost is a bounded number of exact dyadic evaluations at the atom's centre, independent of how many subdivision rounds the search performed to find it. Absolute values, which are irrational in general, never enter the kernel: each is replaced by an exact dyadic bound on the correct side, so soundness is preserved at the cost of a factor-2 margin in how well-separated a root must be before its witness fires.