convergence of the iterated cosine [duplicate]

it can be demonstrated by elementary means that the curves $y=\cos x$ and $y=x$ meet exactly once, at a value $x=\alpha$ satisfying: $$\cos \alpha = \alpha$$ it is also evident (empirically) that simple reiterated pressing of the cosine button on a calculator produces a sequence that seems to converge at a steady, modest pace, from any initial real value to $0.73908\dots$.

however for some time I have fiddled about ineffectually attempting to prove this convergence. this is interesting from a psychological point of view - because I believed the problem was just beyond my reach, I failed to spot a fairly simple proof-idea, which requires no more than high-school calculus and trigonometry.

or at least that is my present thought! the following proof-idea seems OK, though i haven't dotted every i and crossed every t, and since I know myself to be error-prone, I would appreciate it if someone more experienced could check the argument, and remedy any deficiencies - or at worst detect some fundamental flaw I haven't noticed.

I am uncertain how to finish off, and also about how to properly manage the role of $\delta$ - in fact the convergence, though not rapid, seems very robust with regard to initial values.

thank you

firstly, since we know the number $\alpha$ exists, this simplifies the demonstration. it suffices to show that: $$\exists \delta,\lambda \in (0,1) . \forall x \in \mathbb{R}.|x-\alpha| \lt \delta \rightarrow |\cos x - \alpha| \lt \lambda |x-\alpha|$$

set $\beta=\sin \alpha = \sqrt{1-\alpha^2}$ and let $x=\alpha +\epsilon$. then: $$ |x-\alpha| = |\epsilon| $$ and $$\cos x = \cos \alpha \cos \epsilon - \sin \alpha \sin \epsilon = \alpha (1+O(\epsilon^2)) - \beta(\epsilon + O(\epsilon^3)) $$so: $$ |\cos x - \alpha| = \beta |\epsilon|+O(\epsilon^2)= (\beta +O(\epsilon))|\epsilon| $$ giving $$ |\cos x - \alpha| = (\beta +O(\epsilon))|x-\alpha| $$

Here is a formal proof:

Let $f(x) = \cos x$ then the iteration is $$x_{n+1} = f \left( x_n\right)$$

In the interval $[0,1]$, $\cos$ is decreasing and $ 0 \lt \cos 1$. Hence the function maps $[0,1]$ into itself. So by Brower's fixed point theorem, $x_n$ converges to a fixed point.

Also in the interval $|f'| < 1$, so the mapping is a contraction eventually converges as $\rho^n$ where $\rho=\sin 1 \approx 0.84$

The slow convergence is due to the fact that $\rho \approx 1$