Hofstadter's G function is recursively defined via $G(0)=0$ and then $G(n)=n-G(G(n-1))$. Following Hofstadter, we vary the number $k$ of nested recursive calls in this equation and obtain a family of functions $(F\_k)$. Here we establish that this family is ordered pointwise: for all $k$ and $n$, we have $F\_k(n) \le F\_{k+1}(n)$. To achieve this, we make a detour via infinite morphic words generalizing the Fibonacci word. We prove various properties of these words, concerning the lengths of substituted prefixes of these words and the number of occurrences of specific letters in these prefixes. We also relate the limits of $\frac{1}{n}F\_k(n)$ to the frequencies of letters in the considered words. We provide a certified formalization of all these results in the Rocq proof assistant.

翻译：Hofstadter的G函数通过递归定义：$G(0)=0$，然后$G(n)=n-G(G(n-1))$。遵循Hofstadter的思路，我们改变该方程中嵌套递归调用的数量k，从而得到一个函数族$(F\_k)$。本文证明该函数族具有逐点序性质：对所有k和n，均有$F\_k(n) \le F\_{k+1}(n)$成立。为此，我们借助推广Fibonacci词的无限形态词进行迂回论证。我们证明了这些词的若干性质，涉及这些词中替换前缀的长度以及这些前缀中特定字母出现的频次。我们还建立了$\frac{1}{n}F\_k(n)$的极限与所考察词中字母频率之间的联系。我们在Rocq证明助理中对所有这些结果进行了形式化验证。