convergence of the iterated cosine

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|
$$\cos x = \cos \alpha \cos \epsilon – \sin \alpha \sin \epsilon = \alpha (1+O(\epsilon^2)) – \beta(\epsilon + O(\epsilon^3))
$$ |\cos x – \alpha| = \beta |\epsilon|+O(\epsilon^2)= (\beta +O(\epsilon))|\epsilon|
$$ giving
$$ |\cos x – \alpha| = (\beta +O(\epsilon))|x-\alpha|

Solutions Collecting From Web of "convergence of the iterated cosine"

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$