Certificates for finite transcendental inequalities

A finite numerical certificate specifies rational input intervals, exact decimal constants as rationals, outward interval operations, and rigorous enclosures for each occurrence of $\sin$, $\arcsin$ and $\log$. A strict inequality is certified only when the resulting closed intervals are disjoint in the asserted direction. Sine is the smooth real sine function, inverse sine takes its principal values in $[-\pi \mathrm{/}2,\pi \mathrm{/}2]$, and $\log$ is the natural logarithm. The certificate records every denominator's nonvanishing and each inverse function's domain. For an infinite geometric tail, it uses an exact finite expression and a proved remainder bound; a printed decimal table alone is not a certificate. Rounded entries used as lower bounds do not replace exact recurrence values.

The admitted elementary certificates are rational sine sums and tails, principal-branch endpoint tests, range-reduced logarithm and Machin enclosures, and an infinite-tail bound. Their combination supplies a separate scalar replay at $\alpha =0.0816$, including every displayed lower bound and both cap comparisons; no graph-theoretic conclusion is part of this definition.

For storage, choose and record a dyadic floating-point format with precision $p\ge 2$ and finite exponent limits $e_{\min }\le e_{\max }$. Convert every rational interval $[a,b]$ to $[\mathrm{rd}(a),\mathrm{ru}(b)]$, and every exact rational constant $c$ to $[\mathrm{rd}(c),\mathrm{ru}(c)]$. Use exact integer comparisons for this conversion and directed rounding after each endpoint calculation. Every stored interval must be finite. Overflow or a failed domain check supplies no successful certificate; refinement may use a different recorded format. An inconclusive endpoint test establishes no tested inequality, although a separately justified fallback enclosure may still be used. The finite expression graph is a directed acyclic graph whose shared nodes reuse the same exact intermediate value. Arithmetic nodes use the real addition, subtraction, multiplication, division away from zero, and square operations.

The following interval extensions apply at transcendental nodes to the entire stored predecessor interval $X=[l,u]$, including irrational admissible values inside it. All auxiliary endpoints below are exact rationals before outward conversion to storage. Sine point enclosures use an integer $N\ge 0$ and the finite factorial sums and remainder $S_N(x)\pm R_N(x)$, only when $q_N(x)=x^2\mathrm{/}((2N+4)(2N+5))<1$. At a sine node, set $m=(l+u)\mathrm{/}2$ and $r=(u-l)\mathrm{/}2$. If $[s_{-},s_{+}]$ encloses $\sin m$ by that point rule, output the outward conversion of $[s_{-}-r,s_{+}+r]$. At a logarithm node require $l>0$. Obtain point enclosures $\log l\in [L_l,U_l]$ and $\log u\in [L_u,U_u]$ from the range-reduced rule with integer $N\ge 1$, and output the outward conversion of $[L_l,U_u]$.

At an inverse-sine node require $-1\le l\le u\le 1$. Record a Machin enclosure $0<P_{-}\le \pi \le P_{+}$. Start with the rational lower and upper bounds $A=-P_{+}\mathrm{/}2$ and $B=P_{+}\mathrm{/}2$. One may replace $A$ by a rational $a$ satisfying $\mathrm{\mid }a\mathrm{\mid }\le P_{-}\mathrm{/}2$ if a valid sine point enclosure has upper endpoint at most $l$; one may replace $B$ by a rational $b$ satisfying $\mathrm{\mid }b\mathrm{\mid }\le P_{-}\mathrm{/}2$ if a valid sine point enclosure has lower endpoint at least $u$. Output the outward conversion of $[A,B]$. The two optional tests are independent, apply to signed endpoints, and need not succeed. The initial bounds handle $l=-1$, $u=1$, and any inconclusive test. For nonnegative rational point inputs, the original principal-branch endpoint rule is also admitted under its stated hypotheses. No search termination or guaranteed separation at a fixed precision is asserted.

Finite real interval operations enclose their exact values

Principal inverse sine and inverse cosine

Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm

The derivatives of sine and cosine are cosine and minus sine

Rational sine enclosures from a finite factorial sum

Rational inverse-sine brackets on the principal branch

Rational logarithm and pi enclosures after range reduction

A uniform inverse-sine majorant and geometric angular tail

Exact rational replay of the regular amplification constants

Real intervals, complex rectangles and ball enclosures

Outward-rounded interval, rectangle and ball operations

Dyadic floating-point format and directed rounding

Directed dyadic rounding encloses with explicit underflow and overflow bounds

Parity and the Pythagorean identity for sine and cosine

A function differentiable at c is continuous at c

Mean value theorem on a closed real interval

1.1 For rational $a\le b$ within the recorded format's finite range, [F5] gives $\mathrm{rd}(a)\le a\le b\le \mathrm{ru}(b)$. Thus outward conversion contains the whole rational-endpoint input set, not only its endpoints. The same argument with $a=b=c$ encloses an exact rational constant, and applies after every auxiliary rational enclosure. Each successful conversion returns the finite dyadic intervals required by [F1]. Overflow and all invalid operation domains are excluded from a successful certificate. [given, F1, F5, algebra]

2.1 For any real $x,m$, apply [F7] to sine on the interval with endpoints $x,m$ when they differ. It is continuous on that closed interval by [F2] and [F7], differentiable in the interior by [F2], and its derivative has absolute value at most $1$ by [F6]. The mean value identity therefore gives $\mathrm{\mid }\sin x-\sin m\mathrm{\mid }\le \mathrm{\mid }x-m\mathrm{\mid }$; when $x=m$ the same inequality is equality. For $x\in [l,u]$ this gives $\mathrm{\mid }\sin x-\sin m\mathrm{\mid }\le r$, so $s_{-}-r\le \sin x\le s_{+}+r$. Here $m$ is rational, the point enclosure is valid by [F3] with its checked $q_N(m)<1$, and the output conversion preserves containment by step 1.1. This proves the sine extension on every finite stored interval without a monotonicity assumption on sine there. [given, F2, F3, F6, F7, step 1.1, algebra]

2.2 At a logarithm node, every $x\in [l,u]$ is positive because $l>0$. Its endpoints are rational, so [F3] supplies the two point enclosures with their range-reduction and $N\ge 1$ hypotheses. Monotonicity in [F2] gives $L_l\le \log l\le \log x\le \log u\le U_u$. Step 1.1 then proves that the stored output encloses $\log x$ for every such $x$, including irrational ones. [given, F2, F3, step 1.1]

2.3 On $[-1,1]$ the inverse in [F2] is increasing: an inequality between two inverse values in the opposite direction would, by strict increase of sine on the branch, reverse the inequality between their inputs. Thus $\arcsin l\le \arcsin x\le \arcsin u$ for all $x\in [l,u]$. The initial bounds enclose the whole branch because $P_{+}\ge \pi$. If the optional lower test succeeds, $\mathrm{\mid }a\mathrm{\mid }\le P_{-}\mathrm{/}2\le \pi \mathrm{/}2$ puts $a$ on the branch, and [F3] gives $\sin a\le l=\sin (\arcsin l)$; strict increase gives $a\le \arcsin l$. The upper test similarly gives $\sin b\ge u=\sin (\arcsin u)$ and $b\ge \arcsin u$. These arguments use rational point sine enclosures valid for either sign, rather than applying the nonnegative-input supplier outside its hypotheses. Hence $A\le \arcsin x\le B$ whether either test succeeds or not, including inputs $-1$ and $1$. The separately admitted nonnegative point rule is exactly [F3]'s inverse-bracket rule under its own hypotheses. Step 1.1 preserves all these enclosures on storage conversion. [given, F2, F3, step 1.1, algebra]

3.1 Traverse the finite acyclic graph in dependency order. Each exact input or constant belongs to its stored interval by step 1.1. If the exact predecessor values belong to their computed intervals, an arithmetic node encloses its exact output by [F1], and a transcendental node does so by steps 2.1, 2.2 or 2.3 with its checked domain. Induction reaches every root for each admissible assignment; shared nodes cause no change because the same exact value is used at every occurrence. If the entire left root interval lies strictly below the right root interval, their exact values obey that strict inequality. Overlap makes no strict-comparison claim. For an infinite geometric expression, add its separately proved omitted-tail interval before the endpoint comparison; [F3] supplies such an interval for its inverse-sine tail under its stated hypotheses. This imports no arbitrary infinite sum into a finite expression graph. [given, F1, F3, step 1.1, step 2.1, step 2.2, step 2.3, induction]

4.1 In particular [F4] proves that $0.570-\arcsin (3.168\mathrm{/}13.985)-\arcsin (3.168\mathrm{/}(13.985\cdot 2.1274))-3.326\mathrm{/}(63.295(1-1\mathrm{/}2.1274))>0.1356>0.131$. Its recurrence retains $c_3=(2.4093{)}^3$ before rounding, and its cap checks use the exact $5(0.0816{)}^2\mathrm{/}4=0.0083232$. This is a completed rational certificate for the scalar assertions. Each consumer must still establish the hypotheses of its graph-theoretic or asymptotic application. [F4, step 3.1] ∎