There exist libraries that claim to use interval arithmetic for conservative function graphing, specifically recursive algorithms where interval arithmetic is used to prove absence of roots on a given interval. By continuously subdividing space and rejecting regions without roots, they are able to simply stop when a cell becomes equal or less than the size of a pixel and render it as filled.
Simpler algorithms use marching squares for contouring and according to the intermediate value theorem (rather unreliably) look for intervals with roots by comparing signs of taken samples. The main drawback of this approach is that a curve may intersect an edge of the square multiple times, sometimes causing signs of samples taken at the edge vertices to have equal signs, breaking the algorithm as a result.
So my question is how interval arithmetic may with 100% certainty guarantee absence of roots on a given interval?
We assume the function is continuous. The interval Newton method will compute a "family of tangents" whose slopes are all possible slopes of the function over the initial interval (this set is possibly even overestimated). The graph of the function is contained in the (double) cone that is the reunion of all "tangents": https://media.springernature.com/lw685/springer-static/image/chp%3A10.1007%2F978-3-319-31769-4_3/MediaObjects/978-3-319-31769-4_3_Fig2_HTML.gif This is guaranteed by the mean value theorem + interval inclusion, and it's even robust to roundoff errors.
If this cone does not intersect the x-axis within the initial interval, the function cannot have a root within the initial interval.