Golden ratio, Fibonacci numbers and ... another sequence

Over the last weekend, another question was asked and later disappeared on/from Math StakExchange. The sequence, from that question, is too nice to "let it go", thus, copy/pasting my answer here.

Let's define the following sequence $$a(n)=\left\lfloor n\cdot\phi + \frac{1}{2}\right\rfloor$$ where $\phi$ is the golden ratio. Is there a closed form for the following sequence $$a^{\circ k}(n)=\underbrace{a(((...a(n)...)))}_{k \text{ times}}$$?

Calculating a few values of the sequence reveals that this is the A007067, with the property that $$a(a(n))=a(n)+n \tag{1}$$ a result proved in 2006. Let's show it ...

---

Proposition 1. $\left\lfloor \frac{a(n)}{\phi} + \frac{1}{2}\right\rfloor=n$

Given $x-1 < \lfloor x\rfloor \leq x$, we have $$n\phi - \frac{1}{2} < a(n)\leq n\phi + \frac{1}{2} \iff \\ n-\frac{1}{2\phi} < \frac{a(n)}{\phi}\leq n+\frac{1}{2\phi} \iff \\ n+\frac{1}{2}-\frac{1}{2\phi} < \frac{a(n)}{\phi}+\frac{1}{2}\leq n+\frac{1}{2}+\frac{1}{2\phi}$$

Given $1+\frac{1}{\phi}=\phi$ and $\frac{1}{2}-\frac{1}{2\phi} > 0$, then $$n < n+\frac{1}{2}-\frac{1}{2\phi} < \frac{a(n)}{\phi}+\frac{1}{2}\leq n+\frac{\phi}{2} < n+1$$

or $$n < \frac{a(n)}{\phi}+\frac{1}{2} < n+1 \Rightarrow \left\lfloor \frac{a(n)}{\phi} + \frac{1}{2}\right\rfloor=n$$

---

Proposition 2. $a(a(n))=a(n)+n$.

Obviously $a(n)\in\mathbb{N}$, then $$a(a(n))= \left\lfloor a(n)\cdot\phi + \frac{1}{2}\right\rfloor= \left\lfloor a(n)\cdot\left(1+\frac{1}{\phi}\right) + \frac{1}{2}\right\rfloor=\\ a(n)+\left\lfloor \frac{a(n)}{\phi} + \frac{1}{2}\right\rfloor = ...$$

applying Proposition 1 $$...= a(n)+n$$

---

Now back to the original question, a few observations, using $(1)$ $$a^{\circ 2}(n)=a(a(n))=F_2\cdot a(n) + F_1\cdot n$$ $$a^{\circ 3}(n)=a(a(\color{red}{a(n)}))=a(\color{red}{a(n)})+\color{red}{a(n)}=\\ 2\cdot a(n)+n=F_3\cdot a(n) + F_2\cdot n$$ $$a^{\circ 4}(n)=a(a(a(\color{blue}{a(n)})))=2\cdot a(\color{blue}{a(n)})+\color{blue}{a(n)}=\\ 3\cdot a(n)+2n=F_4\cdot a(n) + F_3\cdot n$$

It's easy to see, by induction, this is $$a^{\circ k}(n)=F_k\cdot a(n) + F_{k-1}\cdot n \tag{2}$$

because $$a^{\circ (k+1)}(n)=a^{\circ k}(a(n))=F_k\cdot a(a(n)) + F_{k-1}\cdot a(n)=\\ (F_k+F_{k-1})\cdot a(n) + F_{k}\cdot n=F_{k+1}\cdot a(n) + F_{k}\cdot n$$