A conjectured identity for the fractional iterates of $\sqrt{x}+2$

Deeply impressed by the Fractional iterates of $$x²-2$$, a problem by Ramanujan post one month ago, I decided to investigate a little by myself on the topic and discovered that using Carleman matrices would be of great help for that purpose.

After various numerical computations, and helped by several algorithms for recognizing patterns and guessing formulas, I finally came accross a differential equation detected in a Carleman matrix (by the guessHolo function in the FriCAS computer algebra system) which I could easily solve in order to write down the following identity:

$$F^{[n]}(x) = 2 + 2\cosh\left(2^{1-n}\,\textrm{arcsinh}\!\left(\frac {\sqrt{x-4}}{2}\right)\right)$$

with $$F(x) = \sqrt{x} + 2$$. Plotting this function for various values of $$n$$ between $$1$$ and $$2$$ together with the functions $$F$$ and $$F^{}$$ shows how smoothly the interpolation works.

Now, I don't know if this is something trivial or not and would be very happy to learn about it. Is such a result already known?

Let $$a_n=2(1+\cos\theta_n)$$. Then

$$a_{n+1}=2+\sqrt{2(1+\cos\theta_n)}=2+\sqrt{4\cos^2(\theta_n/2)}=2+2\sqrt{(1+\cos(\theta_n/2))}$$

using the familiar half angle formula for cosine. By comparison

$$\theta_{n+1}=\theta_n/2$$

and thence

$$\theta_n=2^{-n}\theta_0$$

which is easily "fractionated". We have to define a "principal value" of $$\theta_0$$, such as placing it in the interval $$[0,\pi]$$ for real values ($$0\le a_0 \le 4$$), in order to keep things single-valued.