Finite certified evaluation of Gamma and a continued log-Gamma branch

Inputs are a finite dyadic complex rectangle $Z$, a target label $\mathrm{\Gamma }$ or $\mathrm{\ell }$, positive exact rational absolute tolerance ${\epsilon }_a$, optional positive exact rational relative tolerance ${\epsilon }_r$, a fixed dyadic format precision $p_0\ge 2$ and exponent range $(e_{\min },e_{\max })$, fixed integer elementary truncation index $K\ge 1$, finite positive integer work cap $W$, and integer precision cap $P\ge p_0$. The target $\mathrm{\ell }$ is the continued branch in Log-Gamma branch on the slit plane. Reject an invalid target, empty or non-finite rectangle, invalid cap, tolerance, $e_{\min }>e_{\max }$, or $Z\subset ̸\mathbb{C}\setminus (-\mathrm{\infty },0]$ by returning domain. The exact rectangle test is: either the imaginary interval omits zero, or the real interval has strictly positive lower endpoint. Reject a selected shift $m>W$ with inconclusive. For stages $q=1,\dots ,P$, use precision $p=\max (p_0,q)$, harmonic cutoff $M=\min (q,W)$, product cutoff $N=\min (q,W)$, and the fixed elementary truncation index $K$ for every range call. Output statuses are those of Certified special-function enclosure result.

Use Outward-rounded interval, rectangle and ball operations for interval arithmetic. Count every exact rational or interval operation, series term, elementary-DAG node operation, rounding, and loop update against the shared counter $W$. If the procedure is called by another evaluator, charge these same primitive operations directly to that caller's shared counter, so the caller can debit the actual child work; the local cap $W$ remains in force. Before any operation would exceed either remaining cap, return inconclusive. Run nested elementary-range calls under that counter and interrupt a subcall before its next operation would exceed the remaining budget. A non-finite range result makes the current candidate unavailable. Any other non-finite arithmetic result also makes its candidate unavailable; no partial result is retained. Final output overflow returns range.

Choose $m=\max \text{\hspace{0.17em}⁣}(0,\lfloor -\inf \mathrm{\Re }Z\rfloor +1),$ which is the least integer $m\ge 0$ for which $\inf \mathrm{\Re }Z+m>0$. Compute this exactly from the rational endpoint; if $m>W$, return inconclusive before forming the shift. Put $W_Z=Z+m$. Before every elementary-range call, round each rational interval input outward to the stage dyadic format; a conversion overflow makes that candidate unavailable. A rounded Log input must still avoid the cut; otherwise its candidate is unavailable, rather than declaring the valid original input outside the domain. Embed a real interval $X$ explicitly as $X+i[0,0]$ whenever it participates in a complex expression; real and complex DAG nodes retain their declared types. All elementary-range calls below use Certified range evaluation for elementary real and complex functions with the selected format and fixed truncation $K$; its soundness for finite real and complex results is given by Certified real elementary-function evaluations enclose their ranges and Certified complex exponential and principal logarithm enclose their ranges.

For stage $q=1,\dots ,P$, form a dyadic $P_q$ containing $\pi$: for $r\in \{1\mathrm{/}5,1\mathrm{/}239\}$, compute exactly $A_q(r)={\sum }_{k=0}^{q-1}(-1{)}^k{r}^{2k+1}\mathrm{/}(2k+1)$ and $E_q(r)=r^{2q+1}\mathrm{/}((2q+1)(1-r^2))$, combine $\arctan r\in [A_q(r)-E_q(r),A_q(r)+E_q(r)]$ by the Machin identity, and round outward to the selected format at precision $p$. The arctangent series and its geometric-tail argument are in Range-reduced exponential, logarithm and arctangent series have certified tails, and the Machin identity is in Trigonometric identities, Machin's formula and reduced Taylor tails. If the conversion is non-finite or $\inf P_q\le 0$, the Stirling candidate is unavailable for this stage; still attempt the product candidate. Let $a_W=\inf \mathrm{\Re }{W}_Z>0$ and $R_W=\max (\mathrm{\mid }\inf \mathrm{\Re }{W}_Z\mathrm{\mid },\mathrm{\mid }\sup \mathrm{\Re }{W}_Z\mathrm{\mid })+\max (\mathrm{\mid }\inf \mathrm{\Im }{W}_Z\mathrm{\mid },\mathrm{\mid }\sup \mathrm{\Im }{W}_Z\mathrm{\mid })$; $R_W$ is an exact rational upper bound for $\mathrm{\mid }w\mathrm{\mid }$ on $W_Z$.

For this stage, call the elementary-range algorithm on the principal-log node for each $Z+j$, $j=0,\dots ,m-1$. Translation by these real integers preserves avoidance of the cut for an input rectangle wholly in the slit plane; if the exact branch-domain check fails, return domain. Add the finite log rectangles to form the shift sum $L_Z$. If any shift-log call is non-finite, discard this whole stage, since both candidates require that sum. When $m=0$, set $L_Z=0$.

Construct the product candidate when $N>2R_W$. Call the elementary-range algorithm for the real node $\log M$ to get an enclosure $G_M=[g_{-},g_{+}]$ of $\log M$, and form the outward-rounded Euler-constant interval $[H_M-g_{+}-1\mathrm{/}M,H_M-g_{-}]$, where $H_M={\sum }_{k=1}^{M}1\mathrm{/}k$ exactly. Call the complex principal-log node on $W_Z$ and on each $1+W_Z\mathrm{/}k$ for $1\le k\le N$. All these rectangles lie in the principal-log domain since $\mathrm{\Re }{W}_Z>0$. Form $Q_N=-\mathrm{Log}(W_Z)-{\gamma }_E{W}_Z+{\sum }_{k=1}^N(\frac{W_Z}{k}-\mathrm{Log}(1+W_Z\mathrm{/}k))$ by interval arithmetic, and enlarge each coordinate by an outward upper bound for $T_N=\frac{R_W^2}{2N(1-R_W\mathrm{/}(N+1))}\mathrm{.}$ The tail lemma Explicit tail bound for the log-Gamma product series proves that this is an enclosure of ${\mathrm{\ell }}_{+}(W_Z)$, uniformly on the whole rectangle. Subtract $L_Z$ to get the shifted product candidate for $\mathrm{\ell }(Z)$. If $N\le 2R_W$ or a required call is non-finite, this candidate is unavailable at this stage.

Construct the Stirling candidate only when $P_q$ is finite and has positive lower endpoint. Call the complex principal-log node on $W_Z$, and the real logarithm node on $2P_q$. Form $S_Z=(W_Z-\frac{1}{2})\mathrm{Log}(W_Z)-W_Z+\frac{1}{2}\log (2\pi )-L_Z$ by interval arithmetic and enlarge each coordinate by an outward upper bound for $1\mathrm{/}(4a_W)$. The sectorial remainder lemma Explicit sectorial remainder bound for the right-half-plane log-Gamma branch proves this is an enclosure of $\mathrm{\ell }(Z)$. If a required call is non-finite, this candidate is unavailable at this stage.

If both log candidates are available, intersect them when the intersection is nonempty; if empty, discard the stage. If only one is available, select it. For target $\mathrm{\ell }$, use this rectangle as the output candidate. For target $\mathrm{\Gamma }$, call the complex exponential node on the selected rectangle and use its finite output rectangle. Return success at the first stage whose candidate 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.