The formula in question:
$$\sin\left(\frac{x}{2^n}\right) = \sqrt{a_1-\sqrt{a_2+\sqrt{a_3+\sqrt{a_4+\dots+\sqrt{a_{n-1}+\sqrt{\frac{a_{n-1}}{2}\left(1-\sin^2(x)\right)}}}}}}$$ where $$a_k = \frac{1}{2^{2^k-1}} \quad \forall k \in \{1,2,\dots,n-1\}, \ n \in \Bbb{N}, \ x \in \left[0,\frac{\pi}{2}\right[$$ and only the first sign (after $a_1$) is $-$, the rest is $+$.
If this holds, this is a great way to calculate the $\sin$ of small angles, specifically ones that are a power of $\frac{1}{2}$ radians.
My attempt:
I have derived at this by continously using the formula $$\sin\left(\frac{x}{2}\right) = \sqrt{\frac{1-\sqrt{1-\sin^2(x)}}{2}} = \sqrt{\frac{1}{2}-\sqrt{\frac{1}{4}-\frac{\sin^2(x)}{4}}}$$ Which holds true, since $$ \begin{align} \sin(2x) &= 2\sin(x)\cos(x) \\ \sin(x) &= 2\sin\left(\frac{x}{2}\right)\cos\left(\frac{x}{2}\right) \\ \sin(x) &= 2\sin\left(\frac{x}{2}\right)\sqrt{1-\sin^2\left(\frac{x}{2}\right)} \\ \sin^2(x) &= 4\sin^2\left(\frac{x}{2}\right)\left(1-\sin^2\left(\frac{x}{2}\right)\right) \ \left(\text{if } x \in \left[0,\frac{\pi}{2}\right[\right) \\ \sin^2(x) &= 4\sin^2\left(\frac{x}{2}\right)-4\sin^4\left(\frac{x}{2}\right) \\ 0 &= 4\sin^4\left(\frac{x}{2}\right)-4\sin^2\left(\frac{x}{2}\right)+\sin^2(x) \\ \sin^2\left(\frac{x}{2}\right)_{1,2} &= \frac{4 \pm \sqrt{16-16\sin^2(x)}}{8} = \frac{1 \pm \sqrt{1-\sin^2(x)}}{2} \end{align} $$
And this holds true with $-$, since: $$ \begin{align} \sin^2\left(\frac{x}{2}\right) &\stackrel{?}{=} \frac{1-\sqrt{1-\sin^2(x)}}{2} \\ 2\sin^2\left(\frac{x}{2}\right) &\stackrel{?}{=} 1-\cos(x) \\ 2\sin^2\left(\frac{x}{2}\right) &\stackrel{?}{=} 1-\cos^2\left(\frac{x}{2}\right)+\sin^2\left(\frac{x}{2}\right) \\ \sin^2\left(\frac{x}{2}\right) &\stackrel{?}{=} 1-\cos^2\left(\frac{x}{2}\right) \end{align} $$
Yes, since $$ \sin^2\left(\frac{x}{2}\right) + \cos^2\left(\frac{x}{2}\right) = 1 $$ So we found that if $x \in \left[0,\frac{\pi}{2}\right[$, then $$\sin\left(\frac{x}{2}\right) = \sqrt{\frac{1-\sqrt{1-\sin^2(x)}}{2}}$$ Now I plugged the formula into itself a couple times, and guessed what it would look like if I had plugged it in $n$ times. However, I have only assumed the above values of $a_k$ are true by looking at the results, so I'd like a rigorous proof of the formula.
I tried induction by $n$, but I couldn't figure out the $n \rightarrow n+1$ step.
Question:
Provide a proof of the first formula or correct it if it's wrong.
It's a bit tedious, but nonetheless doable:
Since we have
\begin{align}\sin\left(\frac{x}{{2^{n+1}}}\right)&= \sqrt{\frac{1}{2}-\sqrt{\frac{1}{4}-\frac{\sin^2\left(\frac{x}{{2^{n}}}\right)}{4}}} \end{align}
We can use the induction hypothesis to calculate \begin{align*}\frac{1}{4}\cdot\sin^2\left(\frac{x}{{2^{n}}}\right)&=\frac{1}{4}\cdot \left(a_1-\sqrt{a_2+\sqrt{a_3+\sqrt{a_4+\dots+\sqrt{a_{n-1}+\sqrt{\frac{a_{n-1}}{2}\left(1-\sin^2(x)\right)}}}}}\right)\\ &=\frac{a_1}{2^2}-\sqrt{\frac{a_2}{(2^{2})^2}+\sqrt{\frac{a_3}{((2^{2})^2)^2}+\sqrt{\frac{a_4}{2^{2^4}}+\dots+\sqrt{\frac{a_{n-1}}{2^{2^{n-1}}}+\sqrt{\frac{a_{n}}{2^{2^n}\cdot 2}\left(1-\sin^2(x)\right)}}}}}\\ &=a_2-\sqrt{a_3+\sqrt{a_4+\sqrt{a_5+\dots+\sqrt{a_{n}+\sqrt{\frac{a_{n+1}}{2}\left(1-\sin^2(x)\right)}}}}} \end{align*} where we used that $$\frac{a_n}{2^{2^n}}=\frac{1}{2^{2^n-1}\cdot 2^{2^n}}=\frac{1}{2^{2\cdot 2^{n}-1}}=\frac{1}{2^{2^{n+1}-1}}=a_{n+1}$$ And since $$\color{red}{a_1=\frac{1}{2^{2^1-1}}=\frac{1}{2}}$$ and $a_2=\frac{1}{2^{2^2-1}}=\frac{1}{8}$ so that $$\color{blue}{\frac{1}{4}-a_2=\frac{1}{4}-\frac{1}{8}=\frac{1}{8}=a_2}$$ you get
\begin{align}\sin\left(\frac{x}{{2^{n+1}}}\right)&= \sqrt{\frac{1}{2}-\sqrt{\frac{1}{4}-\frac{\sin^2\left(\frac{x}{{2^{n}}}\right)}{4}}}\\ &= \sqrt{\color{red}{\frac{1}{2}}-\sqrt{\color{blue}{\frac{1}{4}-a_2}+\sqrt{a_3+\sqrt{a_4+\sqrt{a_5+\dots+\sqrt{a_{n}+\sqrt{\frac{a_{n+1}}{2}\left(1-\sin^2(x)\right)}}}}}}}\\ &= \sqrt{\color{red}{a_1}-\sqrt{\color{blue}{a_2}+\sqrt{a_3+\sqrt{a_4+\sqrt{a_5+\dots+\sqrt{a_{n}+\sqrt{\frac{a_{n+1}}{2}\left(1-\sin^2(x)\right)}}}}}}} \end{align}