Manuscript Oai276-A@1 · Oai276-A.tex · lemma · 215068af

Lemma: Finite rational comparisons

Stages 3 and 6: the explicit finite maximum certificate › The finite arithmetic certificate · lines 1039–1095 · proof included or linked

Oai276-A@1#lem:arithmetic, Oai276-A@1#eq:sign-checks, Oai276-A@1#eq:midpoint-check, Oai276-A@1#eq:value-checks

Back to manuscript

The rational numbers in (eq:certificate-data)–(eq:value-certificate) satisfy

D_{32}^{-} (a) 0 < D_{32}^{-} (p_{0}) A_{-} > \frac{1}{1000}, \leq D_{32}^{+} (p_{0}) < \frac{1}{1000}, > 0, D_{32}^{+} (b) \frac{412377}{1 0 ^{6}} < - \frac{1}{10000}, < L_{cert} < U_{cert} < \frac{412378}{1 0 ^{6}} .

Proof. These are finite rational comparisons, not transcendental evaluations. Substitute (eq:sums) and (eq:tails) into the displayed definitions.

For complete arithmetic reproducibility, the comparisons are equivalently the following positive-rational checks:

D_{32}^{-} (a) - \frac{1}{1000} > 0, - \frac{1}{10000} - D_{32}^{+} (b) > 0,

D_{32}^{-} (p_{0}) > 0, \frac{1}{1000} - D_{32}^{+} (p_{0}) > 0,

1 0^{6} A_{-} - 412377 ℓ_{+} > 0,

412378 ℓ_{-} - 1 0^{6} (A_{+} + \frac{1}{2000000}) > 0.

All denominators in these substitutions are positive: the series arguments are rational numbers in $[0, 1)$ , and $ℓ_{-} > 0$ . Expansion and collection over their positive common denominators gives the asserted signs. The inequality $D_{32}^{-} \leq D_{32}^{+}$ follows directly from the nonnegative tail terms, and $L_{cert} < U_{cert}$ follows from the definitions.

Appendix app:checker gives a short exact-rational implementation of precisely these finite substitutions. It uses no floating-point arithmetic, logarithms, numerical root finder, or external optimizer.

Displayed formulas in this passage

Oai276-A@1#eq:sign-checks · line 1044
$D_{32}^{-} (a) 0 < D_{32}^{-} (p_{0}) A_{-} > \frac{1}{1000}, \leq D_{32}^{+} (p_{0}) < \frac{1}{1000}, > 0, D_{32}^{+} (b) \frac{412377}{1 0 ^{6}} < - \frac{1}{10000}, < L_{cert} < U_{cert} < \frac{412378}{1 0 ^{6}} .$
Oai276-A@1#eq:midpoint-check · line 1044
$D_{32}^{-} (a) 0 < D_{32}^{-} (p_{0}) A_{-} > \frac{1}{1000}, \leq D_{32}^{+} (p_{0}) < \frac{1}{1000}, > 0, D_{32}^{+} (b) \frac{412377}{1 0 ^{6}} < - \frac{1}{10000}, < L_{cert} < U_{cert} < \frac{412378}{1 0 ^{6}} .$
Oai276-A@1#eq:value-checks · line 1044
$D_{32}^{-} (a) 0 < D_{32}^{-} (p_{0}) A_{-} > \frac{1}{1000}, \leq D_{32}^{+} (p_{0}) < \frac{1}{1000}, > 0, D_{32}^{+} (b) \frac{412377}{1 0 ^{6}} < - \frac{1}{10000}, < L_{cert} < U_{cert} < \frac{412378}{1 0 ^{6}} .$
unlabeled · line 1067
$D_{32}^{-} (a) - \frac{1}{1000} > 0, - \frac{1}{10000} - D_{32}^{+} (b) > 0,$
unlabeled · line 1071
$D_{32}^{-} (p_{0}) > 0, \frac{1}{1000} - D_{32}^{+} (p_{0}) > 0,$
unlabeled · line 1075
$1 0^{6} A_{-} - 412377 ℓ_{+} > 0,$
unlabeled · line 1078
$412378 ℓ_{-} - 1 0^{6} (A_{+} + \frac{1}{2000000}) > 0.$

Lemma: Finite rational comparisons

Displayed formulas in this passage

Nearby in this section