Soundness of finite Gamma and log-Gamma enclosures

For an admissible $Z$, the prescribed integer shift has $a_W=\inf \mathrm{\Re }(Z+m)>0$. Translation by a nonnegative real integer preserves cut avoidance: either the imaginary interval omits zero, or the real lower endpoint was already positive. Thus each exact shift-log input lies in its domain. Its outward-rounded input still contains it; the procedure uses it only when its domain is certified. By [A1] the finite shift-log sum therefore encloses the corresponding exact sum for every $z\in Z$. An unavailable shift sum discards the stage and makes no finite claim.

Write $G_M=[g_{-},g_{+}]$ for a finite enclosure of $\log M$. By [F5], the outward interval $[H_M-g_{+}-1\mathrm{/}M,H_M-g_{-}]$ contains the same real ${\gamma }_E$ used by the branch. Finite outward evaluation of the product partial sum contains its exact value for every $w\in W_Z=Z+m$ by [A1]. The exact rational majorant $R_W$ bounds $\mathrm{\mid }w\mathrm{\mid }$ uniformly. When $N>2R_W$, [F4] bounds each omitted tail by $T_N=R_W^2\mathrm{/}(2N(1-R_W\mathrm{/}(N+1)))$, since the numerator increases and the positive denominator decreases when $\mathrm{\mid }w\mathrm{\mid }$ is replaced by $R_W$. The disk of radius $T_N$ lies in the coordinate rectangle used to enlarge the partial sum. Subtracting the containing shift-log sum from step 1.1 and using [F3] therefore encloses the full range $\mathrm{\ell }(Z)$.

The finite Machin construction encloses $\pi$ by [F7]. Its positive interval and the real logarithm call enclose $\log (2\pi )$ by [A1]. Therefore the finite Stirling main-term rectangle contains the exact main term on $W_Z$. For every such $w$, $\mathrm{\mid }w\mathrm{\mid }\ge \mathrm{\Re }w\ge a_W>0$, so [F6] gives $\mathrm{\mid }R(w)\mathrm{\mid }\le 1\mathrm{/}(4a_W)$. The prescribed outward coordinate enlargement contains this remainder disk. After subtracting the shift-log sum, [F3] again identifies every enclosed target as the same continued branch $\mathrm{\ell }(z)$.

Either finite log candidate thus contains $\mathrm{\ell }(Z)$; their coordinatewise intersection, when used, also contains that entire image. For a log-Gamma target the selected rectangle is therefore sound. For a Gamma target, [A1] encloses its complex exponential, and [F3] identifies the pointwise exponential with $\mathrm{\Gamma }(z)$ for every $z\in Z$. This proves full input-range containment for both targets.

The algorithm tests the actual final outward rectangle's radius before reporting success, and sets a relative flag only when the rectangle excludes zero and passes the relative-radius test. By [F2] these arithmetic tests give exactly the stated absolute and reported relative guarantees. Failed or non-finite candidates are never used for a finite success claim; no finite-cap success guarantee is asserted.

The stage count is at most $P$, each shift and sum has a finite integer cutoff, and each elementary call has a finite DAG, format and truncation index. Moreover [F1] checks the shared counter before each local or nested primitive operation and loop update, interrupting before either its own or its caller's remaining work budget is exceeded. Consequently every capped invocation returns a status after finitely many charged operations, whether or not any candidate succeeds.