Certified Gaussian gridding terminates with a defined status

The elementary evaluator in [F2] visits a finite typed DAG in topological order. Its series have the fixed finite index $J$; its exponential scaling uses a finite integer number of squarings; logarithm bins are a finite integer range determined by positive finite endpoints; and trigonometric reduction examines a finite cell list determined by finite endpoints and a positive certified pi lower bound, returning a named failure if that bound or a branch is unresolved. Square-root endpoint bisection starts with finite integer indices and strictly decreases their positive gap until it is at most one (Exact dyadic bisection for square-root endpoints). Thus these child calls terminate. The phase routine examines only the integer precisions from $p_{\varphi ,0}$ to $p_{\varphi ,\max }$ and calls those finite evaluators (Certified dyadic enclosures for unit-circle phases). Each FFT recursion either returns at length one, returns when its depth cap is zero, or makes two calls with the cap reduced by one and a finite twiddle loop. Induction on the finite depth cap therefore proves termination of every forward call; inverse mode adds only finite conjugations. A failed child call propagates its named status. Consequently no child in [F2]–[F3] is an unbounded evaluation oracle.

Every loop in a candidate is finite: the dimension, source and mode lists, grid-cell lists, image ranges $[-L_r,L_r]$, expression DAGs, range truncation index $J$, phase precision interval $[p_{\varphi ,0},p_{\varphi ,\max }]$, and recursion cap $d_{\mathrm{F}\mathrm{F}\mathrm{T}}$ are finite by [F1]–[F3]. Each coordinate support list $W_{j,r}$ is generated by the finite integer interval in [F7]. Every FFT length is a finite power of two by [F3]. The finite norm sums used in the radius construction are defined by [F5]. Thus a candidate either returns a result or reaches one of its explicitly named failure branches after finitely many operations.

Every division in step 1 is preceded by the denominator, $s_r<1$, and $d_{\min }^{}>0$ checks; every type-1 or type-2 mode division is preceded by its own positive-lower-endpoint test in steps 3–4. Hence all performed divisions have divisor intervals excluding zero. The FFT is called only on inputs in its model's representable set; its statuses are checked and no FFT output is used unless every returned twiddle certificate is at most ${ϵ}_{\mathrm{t}\mathrm{w}}$. The type-1 FFT-error radius uses the same checked call bounds [F6]; its normalization divisor is checked to have a strictly positive enclosure before division, and its finite upward radius sum is checked for overflow. A failed interval, range, FFT, denominator, mode-positivity, radius or twiddle check rejects the candidate. Sound containment of every returned finite interval follows from [F2] and [F4].

The ordered candidate list is finite, and processing terminates for each candidate by step 1.2. The procedure returns the first successful candidate whose outward absolute-error bound meets ${\epsilon }_{\mathrm{r}\mathrm{e}\mathrm{q}}$; if none does so, it returns inconclusive with the first recorded non-success reason, including requested-tolerance-not-met when all computed bounds exceed tolerance. Therefore every certified return has passed its finite checks, and the inconclusive branch returns no approximation certified to the requested tolerance.