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

The finite arithmetic certificate

Stages 3 and 6: the explicit finite maximum certificate › The finite arithmetic certificate · lines 981–1038

Oai276-A@1#eq:certificate-data, Oai276-A@1#eq:derivative-bounds, Oai276-A@1#eq:ln2, Oai276-A@1#eq:arguments, Oai276-A@1#eq:value-certificate

Fix

N = 32, a = \frac{469}{1000}, b = \frac{47}{100}, p_{0} = \frac{939}{2000} .

For $p \in [a, b]$ , both $x (p)$ and $d (p)$ are positive. Define the rational derivative bounds

D_{N}^{-} (p) D_{N}^{+} (p) = x (p) L_{N} (x (p)^{2}) - d (p) (L_{N} (q (p)) + T_{N} (q (p))), = x (p) (L_{N} (x (p)^{2}) + T_{N} (x (p)^{2})) - d (p) L_{N} (q (p)) .

Then $D_{N}^{-} (p) \leq D (p) \leq D_{N}^{+} (p)$ .

A rational enclosure of $ln 2$ is

ℓ_{-} = \frac{2}{3} L_{12} (\frac{1}{9}), ℓ_{+} = ℓ_{-} + \frac{2}{3} T_{12} (\frac{1}{9}), ℓ_{-} \leq ln 2 \leq ℓ_{+} .

Indeed, $ln 2 = 2 atanh (1/3)$ .

At $p_{0}$ , the exact arguments are

x_{0} = \frac{561}{2000}, x_{0}^{2} = \frac{314721}{4000000}, q_{0} = \frac{2307279}{4000000} .

Define

A_{-} A_{+} L_{cert} = J_{32} (q_{0}) - J_{32} (x_{0}^{2}) - R_{32} (x_{0}^{2}), = J_{32} (q_{0}) + R_{32} (q_{0}) - J_{32} (x_{0}^{2}), = \frac{A _{-}}{ℓ _{+}}, U_{cert} = \frac{A _{+} + 1/2000000}{ℓ _{-}} .

Displayed formulas in this passage

Oai276-A@1#eq:certificate-data · line 984
$N = 32, a = \frac{469}{1000}, b = \frac{47}{100}, p_{0} = \frac{939}{2000} .$
Oai276-A@1#eq:derivative-bounds · line 993
$D_{N}^{-} (p) D_{N}^{+} (p) = x (p) L_{N} (x (p)^{2}) - d (p) (L_{N} (q (p)) + T_{N} (q (p))), = x (p) (L_{N} (x (p)^{2}) + T_{N} (x (p)^{2})) - d (p) L_{N} (q (p)) .$
Oai276-A@1#eq:ln2 · line 1008
$ℓ_{-} = \frac{2}{3} L_{12} (\frac{1}{9}), ℓ_{+} = ℓ_{-} + \frac{2}{3} T_{12} (\frac{1}{9}), ℓ_{-} \leq ln 2 \leq ℓ_{+} .$
Oai276-A@1#eq:arguments · line 1020
$x_{0} = \frac{561}{2000}, x_{0}^{2} = \frac{314721}{4000000}, q_{0} = \frac{2307279}{4000000} .$
Oai276-A@1#eq:value-certificate · line 1027
$A_{-} A_{+} L_{cert} = J_{32} (q_{0}) - J_{32} (x_{0}^{2}) - R_{32} (x_{0}^{2}), = J_{32} (q_{0}) + R_{32} (q_{0}) - J_{32} (x_{0}^{2}), = \frac{A _{-}}{ℓ _{+}}, U_{cert} = \frac{A _{+} + 1/2000000}{ℓ _{-}} .$