The certified particle-mesh Ewald evaluator terminates with finite outputs or an explicit status

Each non-transform request [F1] either returns its supplied certified data or consumes at most the positive finite $B_{\mathrm{e}\mathrm{n}\mathrm{c}\mathrm{l}}$ instruction budget and exits. Each counted instruction on finite rational data or fixed-format operands terminates, with the model's range-failure outcome when appropriate. Thus no request can perform unbounded precision refinement, wait for an undecided equality, or search until a valid radius appears. Initial validation uses finitely many particle pairs and scalar/integer conditions. It either exits with a declared status, or supplies the finite data needed by the first step.

A phase call has at most $p_{\max }-p_0+1$ precision attempts by [F2]. At each attempt the Machin sums have $J_{\mathrm{p}\mathrm{h}\mathrm{a}\mathrm{s}\mathrm{e}}+1$ terms and rational tails. Its elementary DAGs are finite. Topological sorting removes a node at each successful iteration or reports a cycle, so it finishes. For every finite positive-endpoint logarithm interval, only finitely many dyadic bins lie between its endpoints; arctangent uses at most seven fixed pieces. For sine/cosine the algorithm computes finite $K=\lceil 2M_X\mathrm{/}{p}_{-}\rceil +1$ when $p_{-}>0$ and examines only $-K,\dots ,K$, otherwise returning a status. Every series has its fixed truncation degree; the exponential squaring count is the finite integer $\max (0,e_{\max }+2)$. Square-root endpoint bisection starts with integer gap $2^{p+1}$ and at each iteration replaces it by at most its ceiling half, so at most $p+1$ iterations suffice. Directed conversion of a rational endpoint searches a finite representable set using integer comparisons. All other rational endpoint arithmetic terminates, and unresolved domains or nonfinite conversions return statuses. Therefore each elementary call and each capped phase call terminates, including when its requested phase tolerance is unmet.

Induction on the integer $d_{\max }$ proves termination of each radix-two call: length one returns directly, depth zero at larger length returns inconclusive, and otherwise its two children have depth $d_{\max }-1$. Each finite butterfly list uses only scalar operations and the terminating phase calls of step 1.2. An inverse call adds only two finite conjugations around its forward call. Hence a radix-two call has a finite binary recursion tree, of at most $2^{d_{\max }+1}-1$ nodes. A cyclic convolution has just three such calls and a finite list of products/scalings, so it terminates too.

In Step 1 of the evaluator, obtaining the finite bound $B_K$ either succeeds in bounded work or exits by step 1.1. Its outward endpoint has an exactly computable integer ceiling $N_K$. The box has $(2N_K+1{)}^3$ integer triples; each distance/cutoff decision uses a bounded request and either includes, excludes, or returns cutoff-inconclusive. Retained-mode restrictions are finite integer comparisons. Thus both the retained set and omitted-mode ledger are constructed in finite work. Their symmetry, strict mesh restrictions and injection modulo the mesh are preserved because successful comparisons certify the exact radial membership: two strictly interior signed representatives differing by a mesh multiple must coincide coordinatewise.

In Step 2, if an assignment-coordinate interval has width greater than one, the stated exit occurs. Otherwise its integer support endpoints are finite, and the interval from $a^{-}-P$ to $a^{+}$ has length at most $P+1$. Any interval of length at most $P+1$ contains at most $P+2$ integers, so the triple list has at most $(P+2{)}^3$ entries. The finite formula for $W_P$ in [F5] uses integer powers, factorials, binomial coefficients, and $P+1$ summands, all finite for the given integer $P$. Each arithmetic/enclosure request terminates by step 1.1. Reduction modulo each positive $M_r$ and accumulation keep duplicate wraps rather than starting another loop. The same proof applies to the optional query support and to the finite polynomial derivatives. If a $P=2$ selected right-hand box cannot be certified within its budget, the explicit arithmetic-inconclusive branch returns; an exact knot certificate selects the same one-sided derivative in both correction factors.

In Step 6 the bounded request for $B_R$ either exits or gives a finite ceiling $N_R$. For each needed pair the box has $(2N_R+1{)}^3$ candidates. There are at most $n$ query/source pairs and $n^2$ particle pairs for each of the energy and force sums. For a true retained image, $\mathrm{\mid }{t}_a-t_b\mathrm{\mid }\le \sqrt{3}$ gives $\mathrm{\mid }\mathrm{\ell }\mathrm{\mid }\le \mathrm{\parallel }{A}^{-1}{\mathrm{\parallel }}_{2}R+\sqrt{3}\le B_R$, so the box misses none. Each candidate uses a bounded include/exclude/cutoff-inconclusive test. The own zero-image term is omitted before singular kernel evaluation; every other kernel division requires a certified positive distance bound or exits. Its elementary values and finite derivative arithmetic use step 1.1. The real potential, energy, force and ordinary Ewald self constant thus finish, without differentiating the cutoff indicator.

For arbitrary transform length $N$, trial division can examine $2,\dots ,N-1$ and thus terminates. A composite non-power-of-two branch has factors $1<r,s<N$, makes $r$ length-$s$ calls and $s$ length-$r$ calls, and a finite twiddle list. Strong induction on $N$ proves these calls terminate, with length one the base case. A power of two uses step 2.1. At a prime, start at one and double until the padding length is at least $2N-1$. This search is finite since $2^j\ge j+1$ by integer induction, and its least resulting power $M$ satisfies $M<4N$. There are finitely many chirp phases, one cyclic convolution of length $M$, and finitely many final products; steps 1.2 and 2.1 finish them. Thus all transform calls terminate with their actual supplied caps; no sufficient-depth or phase-success assumption is needed.

Step 7's floor requests terminate or return cutoff-inconclusive. With determined floors, [F6] constructs the real controller using $J_R-M_R+1$ summands and the reciprocal controller using $J_K-M_K+1$ summands, plus four $I_s$ terms apiece. The $I_s$ recurrence reduces $s$ by two and stops at zero or one; no search for larger $J_R,J_K$ is performed. For each of finitely many retained modes, each one-dimensional source/derivative alias sum through $1\le \mathrm{\mid }j\mathrm{\mid }\le J_A$ has $2J_A$ terms, followed by the explicit p-series remainder. Their tensor products need no infinite summation; even a direct finite triple list would have at most $(2J_A+1{)}^3$ entries. For $P=2$, [F5] instead supplies the finite derivative-window bound. The omitted ledger is finite by step 2.2. All controller elementary values, arithmetic radii and final sums are bounded requests under step 1.1. This proves finite construction or an explicit arithmetic-inconclusive exit.

The full grid has finite size $N_g=M_1{M}_2{M}_3$. Each tensor transform has exactly $N_g\mathrm{/}{M}_r$ coordinate fibers in direction $r$; every one-dimensional call terminates by step 3.1. Step 3 uses one tensor transform; Step 5 uses at most one potential transform, one force transform, and one optional kernel transform. Thus there are at most four tensor transforms, with finitely many normalizations. Failed calls/scales return transform-inconclusive; bounded denominator certification in Step 4 returns denominator-inconclusive before an unsafe division. Retained-mode and grid array construction are finite. All gathers visit the finite supports from step 2.3, and self correction visits at most $(P+2{)}^6$ ordered tuple pairs per particle. These polynomial products, derivatives and finite sums therefore terminate while retaining the same energy, force, and diagonal correction formulas.

Finally there are finitely many requested output radii and tolerance comparisons. Each is bounded by [F1]; proven satisfaction gives certified, proven excess gives certified-over-tolerance, and an unresolved decision returns arithmetic-inconclusive. Steps 1.1–3.2 prove that every preceding branch or subcall finishes; their finite concatenation therefore terminates with the stated record. Divisor, branch and enclosure checks prevent undefined successful outputs. On a valid final-output branch the unchanged arithmetic-enclosure assumptions and finite formulas meet [F7], so its potential, energy, force and optional self-correction error guarantees apply. No work-count premise was used to infer termination.