# 45. Interval certificates and simultaneous curve topology Dive 19, 2026-09-08. **Question:** what can computation prove about an implicit curve, and what extra work preserves an arrangement of several curves? Read [44](44_curve_sampling_topology.md) for the distinction between distance and topology. `[T]` marks source results in adapted notation; `[D]` marks derivations here, not novelty. The source cards distinguish selected-section reading from full proof verification. ## 1. A finite grid can miss a whole component On B=[0,1]² define `[D]` \[ F(x,y)=(x-\tfrac12)^2+(y-\tfrac12)^2-\tfrac1{16}. \] At every corner F=7/16>0, but F(1/2,1/2)=−1/16. Its zero set is a complete circle of radius 1/4 inside B. Looking only for sign differences between box corners finds none. A finite collection of function evaluations is not a whole-box exclusion proof. An **inclusion interval**, denoted I_F(B), contains {F(p):p∈B}. Thus \[ C_0(B):\quad 0\notin\mathcal{I}_F(B)\quad\Longrightarrow\quad F^{-1}(0)\cap B=\varnothing. \] The converse does not hold: an interval containing zero leaves the test inconclusive. Interval expressions may be wider than the true range. For x∈[−1,1], the expression x−x+1 evaluates naively to [−1,3], although the function is identically 1. Dependency is lost when repeated occurrences are treated as independently ranging. Algebraic form and subdivision affect tightness without changing truth. For the circle example, square-aware rational interval evaluation gives exactly [−1/16,7/16]. It correctly refuses to exclude the box. It does not yet certify the number of components. Floating point interval arithmetic needs outward rounding or another proved enclosure mechanism; ordinary rounded endpoints plus an arbitrary tolerance do not supply inclusion. ## 2. Plantinga–Vegter uses a pairwise gradient condition `[T]` Plantinga and Vegter consider smooth implicit curves with 0 a regular value: ∇F is nonzero at every zero of F. In the planar construction, start with a square containing the bounded curve and convergent inclusion bounds for F and its derivatives. Subdivision stops locally if C_0 holds or if \[ C_1(B):\quad \mathcal{I}_{\nabla F}(B)\cdot\mathcal{I}_{\nabla F}(B)>0. \] The lower endpoint must be strictly positive. Crucially, the expression encloses **∇F(p)·∇F(q) for every p,q∈B**, not just ||∇F(p)||² for one p. Gradient directions then make angles smaller than π/2. With the interval-box predicate at least one coordinate derivative is bounded away from zero, giving a consistent graph direction in the box. The archived paper's algorithm and formula were visually checked on physical p.4 (printed p.247). [SRC: plantinga-2004-isotopy] **Why squaring is different `[D]`.** Take F(x,y)=y−x² on x∈[−1,1]. Its gradient intervals are G_x=[−2,2], G_y=[1,1]. A same-point squared norm is at least 1 everywhere. But independent interval multiplication gives \[ G_xG_x+G_yG_y=[-4,4]+[1,1]=[-3,5]. \] Indeed, the endpoint gradients (2,1) and (−2,1) have dot product −3. Replacing G_xG_x with the specialized square [0,4] would incorrectly certify this **pairwise** predicate. The curve is regular and is a graph; the stronger test simply fails on this large box. A failed sufficient condition is not evidence of singularity. For shrinking boxes, continuity and convergent bounds eventually certify exclusion away from the curve, or positive pairwise gradient products near a regular zero. This is the mechanism behind termination under the source assumptions. A box containing a singular zero, where F=0 and ∇F=0, cannot pass either test. A depth cap must return an unresolved region instead of silently treating a stopped computation as certified. ## 3. Local predicates are only part of the global theorem `[T]` The planar algorithm also balances the quadtree, handles its edge subdivisions, uses sign conventions for zero-valued vertices, and connects output vertices according to specific rules. The source's Theorem 4.1 (physical p.5, printed p.248) establishes isotopy for the resulting polygonal approximation, under the algorithm and hypotheses as a whole. Neighboring cell sizes differ by at most a factor of two; a quadtree cell can have more than four edge pieces. The proof handles multiple crossings along an edge through curve excursions and deformations. [SRC: plantinga-2004-isotopy] This is a **global** guarantee. It does not say that the output inside every individual leaf is isotopic to the true curve restricted to that same leaf. Excursions may move across cell boundaries. Burr and Byrd explicitly revisit this distinction (physical p.3). [SRC: burr-2024-simultaneous] Consequently: - A C_0 leaf is certified empty of the zero set. - A C_1 leaf satisfies a sufficient regularity condition; it need not contain a zero. - A complete global meshing theorem requires the rest of the specified algorithm. - Topological correctness alone does not establish a requested positional tolerance or mesh quality. The original paper discusses accuracy refinement and singularity limitations in physical pp.9–10. This dive read the planar proof discussion, not the full three-dimensional correctness proof. No surface-meshing claim or production implementation is certified here. [Study 10](../experiments/10_geometry_certificates.py) implements exact rational interval classification for the hidden circle. It intentionally stops before balancing and mesh construction. Its checked predicates are certificates for its polynomial boxes; its colored quadtree is not an implementation of the complete Plantinga–Vegter mesher. ## 4. Individually correct curves can have an incorrect arrangement **Counterexample `[D]`.** On −1≤x≤1, compare the labeled pair \[ A_1:\ y=0,\qquad A_2:\ y=x^2-a^2 \] with \[ B_1:\ y=0,\qquad B_2:\ y=x^2+a^2,\quad 0