广义Hofstadter函数G, H及其它函数的逐点序
Pointwise order of generalized Hofstadter functions G, H and beyond
AI总结：
本文通过引入无限形态词推广Fibonacci词，证明了广义Hofstadter函数族(F_k)满足逐点序F_k(n) ≤ F_{k+1}(n)，并利用Rocq证明助手进行了形式化验证。
摘要：
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证明助手中提供了所有这些结果的认证形式化。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
