Trigonometric identities, Machin's formula and reduced Taylor tails

On each bounded square, the factorial series and their tails converge uniformly by [L8]. Their Cauchy products are absolutely convergent and can be grouped by total degree by [L9]. For sine, the coefficient of $x^r{y}^s$ in $\sin (x+y)$ vanishes when $r+s$ is even and otherwise equals $(-1{)}^{(r+s-1)\mathrm{/}2}\mathrm{/}(r!s!)$, by the binomial theorem; the same coefficient appears in $\sin x\cos y+\cos x\sin y$. For cosine, the coefficient in $\cos (x+y)$ vanishes when $r+s$ is odd and otherwise equals $(-1{)}^{(r+s)\mathrm{/}2}\mathrm{/}(r!s!)$, matching $\cos x\cos y-\sin x\sin y$. Thus both addition identities hold.

On every bounded interval, [L8] gives absolute convergence of the factorial coefficient series and their derivative series. Applying [L5] to the two power series gives ${\sin }^{\mathrm{\prime }}=\cos$ and ${\cos }^{\mathrm{\prime }}=-\sin$. By the product rule in [L4], the derivative of ${\sin }^{2}x+{\cos }^{2}x$ is zero; [L3] and its value $1$ at zero give ${\sin }^{2}x+{\cos }^{2}x=1$.

Write $A(t)=\arctan t$, $S(t)=\sin A(t)$ and $C(t)=\cos A(t)$. From [L1], the difference quotient for $A$ is the average of the continuous integrand $1\mathrm{/}(1+u^2)$ over the interval from $t$ to $t+h$, so $A^{\mathrm{\prime }}(t)=1\mathrm{/}(1+t^2)$. By the preceding sine and cosine identity and the chain and product rules [L4], $g(t)=S(t)-tC(t)$ satisfies $g^{\mathrm{\prime }}(t)=tg(t)\mathrm{/}(1+t^2)$ and $g(0)=0$. The quotient rule [L4] gives $(g(t{)}^2\mathrm{/}(1+t^2){)}^{\mathrm{\prime }}=0$. By [L3], this quotient is constant on every interval between $0$ and $t$, hence zero; therefore $g(t)=0$. Now $C(t{)}^2=1\mathrm{/}(1+t^2)$ by the preceding sine and cosine identity, and $C^{\mathrm{\prime }}(t)=-tC(t)\mathrm{/}(1+t^2)$. Put $q(t)=\sqrt{1+t^2}$. Since $q(t)\ge 0$ and $q(t{)}^2\ge 1$, it follows that $q(t)\ge 1$: otherwise $(1-q(t))(1+q(t))>0$ would imply $q(t{)}^2<1$. The same holds at $t+h$. For $h$ near zero, rationalization gives $\mathrm{\mid }q(t+h)-q(t)\mathrm{\mid }=\frac{\mathrm{\mid }h\mathrm{\mid }\mathrm{\mid }2t+h\mathrm{\mid }}{q(t+h)+q(t)}\le \frac{\mathrm{\mid }h\mathrm{\mid }(2\mathrm{\mid }t\mathrm{\mid }+\mathrm{\mid }h\mathrm{\mid })}{2}⟶0.$ Thus $q$ is continuous, and the rationalized difference quotient $(q(t+h)-q(t))\mathrm{/}h=(2t+h)\mathrm{/}(q(t+h)+q(t))$ tends to $t\mathrm{/}q(t)$; hence $q^{\mathrm{\prime }}(t)=t\mathrm{/}q(t)$. The product rule [L4] gives $(q(t)C(t){)}^{\mathrm{\prime }}=0$, so [L3] implies $q(t)C(t)$ is constant on every segment between $0$ and $t$. Its value at zero is $1$, hence $C(t)=1\mathrm{/}q(t)>0$. For $t>0$ and $0\le u\le t$, the integrand satisfies $1\mathrm{/}(1+u^2)\ge 1\mathrm{/}(1+t^2)$. Constant comparison for the integral [L1] gives $A(t)\ge t\mathrm{/}(1+t^2)>0$. Also $A^{\mathrm{\prime }}(t)=1\mathrm{/}(1+t^2)$, so $H(t)=A(t)+A(1\mathrm{/}t)$ has derivative $H^{\mathrm{\prime }}(t)=\frac{1}{1+t^2}-\frac{1}{t^2}\frac{1}{1+1\mathrm{/}{t}^2}=0.$ By [L3], $H$ is constant on the positive segment between $1$ and $t$; $H(1)=2A(1)$. Therefore $A(t)=2A(1)-A(1\mathrm{/}t)$ for every $t>0$, and the positivity just proved shows $0<A(t)<2A(1)$. Similarly, the derivative of $A(-t)+A(t)$ is zero and its value at zero is zero, so [L3] gives $A(-t)=-A(t)$ for every real $t$. Since $\pi \mathrm{/}2=2A(1)$, these bounds yield $A(t)\in (-\pi \mathrm{/}2,\pi \mathrm{/}2)$ for all real $t$ and $\tan A(t)=t$. At $t=1$, $S(1)=C(1)>0$ and step 1.2 gives both equal $1\mathrm{/}\sqrt{2}$; the addition identities yield $\sin (\pi \mathrm{/}2)=1$ and $\cos (\pi \mathrm{/}2)=0$.

For $u,v\ge 0$ with $uv<1$, define $H(v)=A(u)+A(v)-A((u+v)\mathrm{/}(1-uv))$. Differentiating with the inverse-tangent derivative formula and the chain rule [L4], the derivative of the last term is $\frac{(1+u^2)\mathrm{/}(1-uv{)}^2}{1+((u+v)\mathrm{/}(1-uv){)}^2}=\frac{1}{1+v^2},$ which is also $A^{\mathrm{\prime }}(v)$. Thus $H^{\mathrm{\prime }}(v)=0$ and $H(0)=0$; [L3] gives $A(u)+A(v)=A((u+v)\mathrm{/}(1-uv))$. Set $\alpha =A(1\mathrm{/}5)$ and $\beta =A(1\mathrm{/}239)$. This identity gives $2\alpha =A(5\mathrm{/}12)$, then $4\alpha =A(120\mathrm{/}119)$, and also $\beta +A(1)=A(120\mathrm{/}119)$. Hence $4\alpha =\beta +A(1)$ and $16\alpha -4\beta =4A(1)=\pi$.

Put $q=2x\mathrm{/}\pi$. By [L6], choose an integer $n>\mathrm{\mid }q\mathrm{\mid }+1$. Among the finite ordered list $-n,-n+1,\dots ,n$, take its greatest member $k_0\le q$; then $k_0\le q<k_0+1$. At least one of $k_0,k_0+1$ is within $1\mathrm{/}2$ of $q$; call it $k$. Since $0<1\mathrm{/}(1+u^2)\le 1$ on $[0,1]$, integral comparison [L1] and step 2.1 give $0<A(1)\le 1$, hence $\pi \mathrm{/}4=A(1)\le 1$. Therefore the residual $r=x-k\pi \mathrm{/}2$ satisfies $\mathrm{\mid }r\mathrm{\mid }\le \pi \mathrm{/}4\le 1$. Repeated application of the addition identities in step 1.1 and the values proved in step 2.1 gives the quarter-period sign and swap formulas.

Since $1\mathrm{/}5$ and $1\mathrm{/}239$ lie in $[0,1\mathrm{/}2]$, [L2] gives rational intervals for $\alpha$ and $\beta$ with the displayed tail widths. Multiplying those intervals by $16$ and $4$ and using the exact identity in step 3.1 gives a certified rational interval for $\pi$; increasing the truncation count decreases both tail bounds.

Fix any $\mathrm{\mid }r\mathrm{\mid }\le 1$ and $N\ge 0$. The sine terms after degree $2N+1$ have first omitted magnitude $\mathrm{\mid }r{\mathrm{\mid }}^{2N+3}\mathrm{/}(2N+3)!$ and each later ratio is at most $\mathrm{\mid }r{\mathrm{\mid }}^2\mathrm{/}((2N+4)(2N+5))<1$. Summing this geometric majorant gives $T_s$. The cosine terms after degree $2N$ have first omitted magnitude $\mathrm{\mid }r{\mathrm{\mid }}^{2N+2}\mathrm{/}(2N+2)!$ and ratio at most $\mathrm{\mid }r{\mathrm{\mid }}^2\mathrm{/}((2N+3)(2N+4))<1$, giving $T_c$.