Finite certified Airy power-series evaluation

Inputs are an exact dyadic complex number $z$, a target label $\mathrm{Ai}$ or $\mathrm{Bi}$, positive rational absolute tolerance ${\epsilon }_a$, optional positive rational relative tolerance ${\epsilon }_r$, a fixed exponent range $(e_{\min },e_{\max })$, and finite positive integer caps $S_{\max },K_{\max },p_{\max },W$, with $p_{\max }\ge 2$. Reject an invalid target, nonpositive tolerance, invalid cap, or $e_{\min }>e_{\max }$ with domain. The caps bound stages, terms per residue class, final dyadic precision, and this procedure's exact interval operations and subroutine calls. For stage $q$, use $K=q$, precision $p=\max (2,\min (q,p_{\max }))$, and elementary-range truncation $q$; run stages $q=1,\dots ,\min (S_{\max },K_{\max },p_{\max })$.

All arithmetic uses Outward-rounded interval, rectangle and ball operations. Charge every exact arithmetic operation, range-evaluator node operation, term, rounding, and loop update to the shared counter $W$. Return inconclusive before any local operation would exceed $W$; interrupt a nested subroutine before its next operation would exceed the remaining budget. When nested, charge every Gamma-child operation directly to the same parent counter. If a final endpoint overflows, return range. A non-finite subroutine result makes the current stage unavailable; later stages may still be tried. Other statuses are those of Certified special-function enclosure result.

At stage $q$, outward-round the rational points $1\mathrm{/}3$ and $2\mathrm{/}3$ to dyadic intervals $G_r$ at precision $p$. For each $r\in \{1\mathrm{/}3,2\mathrm{/}3\}$, charge the child-call operation to the parent counter. If no parent work unit remains, return inconclusive; otherwise pass the positive remaining budget as the child's work cap and call Finite certified evaluation of Gamma and a continued log-Gamma branch with target $\mathrm{\Gamma }$ on the complex rectangle $G_r+i[0,0]$, absolute tolerance $2^{-q}$, no relative tolerance, the same exponent range, fixed elementary truncation $q$, base format precision $p$, and precision cap $p$. Debit every operation performed by the Gamma child to the shared counter. A success output rectangle encloses $\mathrm{\Gamma }(r)$, since $r\in G_r$; if either call is not successful or its rectangle contains zero, skip this stage. A failed rational-to-dyadic conversion also makes the stage unavailable.

For $s\in \{1\mathrm{/}6,1\mathrm{/}3,2\mathrm{/}3\}$, outward-round the exact rational $s$ to a dyadic interval $S_{s,p}$, then call Certified range evaluation for elementary real and complex functions on the real expression DAG $\exp (S_{s,p}\log 3)$, with the same exponent range, precision $p$, and truncation $q$. These calls enclose $3^s$ by Certified real elementary-function evaluations enclose their ranges. If a required call is not finite, skip this stage. Embed each real power interval $X$ as the complex rectangle $X+i[0,0]$, then combine it with the Gamma rectangles by outward complex arithmetic to enclose the two initial coefficients $(a_0,a_1)=(\frac{1}{3^{2\mathrm{/}3}\mathrm{\Gamma }(2\mathrm{/}3)},-\frac{1}{3^{1\mathrm{/}3}\mathrm{\Gamma }(1\mathrm{/}3)})$ for Ai, or $(b_0,b_1)=(\frac{1}{3^{1\mathrm{/}6}\mathrm{\Gamma }(2\mathrm{/}3)},\frac{3^{1\mathrm{/}6}}{\mathrm{\Gamma }(1\mathrm{/}3)})$ for Bi. If any divisor rectangle contains zero or an arithmetic operation is non-finite, skip this stage.

Put $R=\mathrm{\mid }\mathrm{\Re }z\mathrm{\mid }+\mathrm{\mid }\mathrm{\Im }z\mathrm{\mid }$, an exact rational upper bound for $\mathrm{\mid }z\mathrm{\mid }$. For each residue $r=0,1$, initialize $t_{r,0}=c_r{z}^r$ using the selected pair of initial coefficient intervals, and compute $t_{r,j+1}=t_{r,j}{z}^3\mathrm{/}((k+3)(k+2))$, where $k=r+3j$. Sum $t_{r,0},\dots ,t_{r,q-1}$ and compute the first omitted term $t_{r,q}$. Put $k_r=r+3q$ and ${\rho }_r=\frac{R^3}{(k_r+3)(k_r+2)}\mathrm{.}$ If either ${\rho }_r\ge 1$, skip the stage. Otherwise enlarge the sum of both partial rectangles in each coordinate by $\frac{M(t_{0,q})}{1-{\rho }_0}+\frac{M(t_{1,q})}{1-{\rho }_1},$ where $M(X+iY)=\max (\mathrm{\mid }\inf X\mathrm{\mid },\mathrm{\mid }\sup X\mathrm{\mid })+\max (\mathrm{\mid }\inf Y\mathrm{\mid },\mathrm{\mid }\sup Y\mathrm{\mid })$. The $c_2=0$ residue class vanishes identically. The ratio and tail lemma Airy coefficient recurrence and geometric tail bounds therefore makes the enlarged rectangle a containing enclosure of the selected Airy value.

Round the final rectangle outward to precision $p$. Return success at the first stage whose radius is at most ${\epsilon }_a$. Set relative_certified to true exactly when relative tolerance was requested, zero is excluded, and the contract's relative-radius test passes; a failed relative test does not prevent absolute success. If no stage succeeds before its caps, return inconclusive. The stage loop and all subroutine calls have finite caps, so the procedure has no unbounded retry.