pith. sign in

arxiv: 2410.00529 · v2 · pith:PP6RA5OInew · submitted 2024-10-01 · 💻 cs.DM · cs.FL· math.CO· math.NT

Pointwise order of generalized Hofstadter functions G, H and beyond

Pierre Letouzey (IRIF (UMR\_8243) , PICUBE) , Shuo Li (H3I) , Wolfgang Steiner (IRIF (UMR\_8243)) This is my paper

Pith reviewed 2026-05-25 08:11 UTC · model grok-4.3

classification 💻 cs.DM cs.FLmath.COmath.NT
keywords Hofstadter functionsgeneralized recursive functionsmorphic wordspointwise orderingFibonacci word generalizationletter frequenciesasymptotic growth
0
0 comments X

The pith

Generalized Hofstadter functions satisfy F_k(n) ≤ F_{k+1}(n) for all k and n.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper defines a family of functions F_k that generalize Hofstadter's G function by increasing the number of nested recursive calls from two to k. It proves that these functions are ordered pointwise, meaning each additional nesting produces a function that is always at least as large as the previous one at every input n. The proof proceeds by constructing infinite morphic words that generalize the Fibonacci word and linking the growth rates of the functions to letter frequencies in those words. This ordering gives a clear hierarchy among these recursively defined sequences.

Core claim

By generalizing the defining equation of Hofstadter's G function to allow k nested recursive calls, the resulting functions F_k satisfy F_k(n) ≤ F_{k+1}(n) for all k and n. The proof relies on properties of lengths of substituted prefixes and occurrence counts of letters in infinite morphic words, which also determine the asymptotic densities lim F_k(n)/n.

What carries the argument

The family of functions (F_k) obtained by varying the number k of nested recursive calls in the defining equation, together with the associated infinite morphic words used to analyze their growth.

Load-bearing premise

The infinite morphic words obtained by the generalized substitution rules satisfy the stated length and occurrence-count properties that are used to relate the limits of F_k(n)/n to letter frequencies.

What would settle it

A specific pair k and n where F_k(n) > F_{k+1}(n), or a computation showing that the morphic words fail to satisfy the required prefix length or letter occurrence properties.

Figures

Figures reproduced from arXiv: 2410.00529 by PICUBE), Pierre Letouzey (IRIF (UMR\_8243), Shuo Li (H3I), Wolfgang Steiner (IRIF (UMR\_8243)).

Figure 1.1
Figure 1.1. Figure 1.1: Plotting F1, F2, . . . , F5 1.3. Substitutions and morphic words. For k ≥ 1, let τk be the substitution2 on the alphabet {1, 2, . . . , k} defined by τk : k 7→ k1, i 7→ i+1 for 1 ≤ i < k. Let xk = xk[0]xk[1] · · · ∈ {1, 2, . . . , k} ∞ be the fixed point of τk. x2 = 2122121221221212212122122121221221212212 · · · x3 = 3123313123123312331312331312312331312312 · · · x4 = 412344141241234123441234414123441412… view at source ↗
Figure 1.2
Figure 1.2. Figure 1.2: Infinite words x2, . . . , x5 (with highest letter in red) 2A substitution (or morphism) on an alphabet A is a map τ : A∗ → A∗ satisfying τ(uv) = τ(u)τ(v) for all u, v ∈ A∗ , where A∗ denotes the set of finite words with letters in A. The map τ is therefore defined by its value on the letters of A, and it is extended in a natural way to infinite words (or sequences) w = w[0]w[1] · · · ∈ A∞ by setting τ(x… view at source ↗
Figure 5.1
Figure 5.1. Figure 5.1: gives approximate values for the first αk and βk. Note in particular that β1 = 2 and β2 is the golden ratio ϕ = 1+√ 5 2 . Thanks to the rational root theorem, one can easily show that αk and βk are irrational for k ≥ 2. α1 = 0.5 α2 = 0.6180339887498948 . . . α3 = 0.6823278038280193 . . . α4 = 0.7244919590005157 . . . α5 = 0.7548776662466925 . . . α6 = 0.7780895986786012 . . . β1 = 2 β2 = 1.61803398874989… view at source ↗
Figure 7.1
Figure 7.1. Figure 7.1: The known (F j k , ≤) lattice, displayed here for 1 ≤ k, j ≤ 5. are uncomparable in this case; or j > 2k in which case we conjecture that F j k ≤ F j+1 k+1 . For studying these questions, we focus now on L j+1 k+1(1) − L j k (1). Lemma 7.6. For all k ≥ 1, we have L j+1 k+1(1) − L j k (1) = ( 1 if 0 ≤ j ≤ 2k, − (j−2k−1)(j−2k+2) 2 if 2k ≤ j ≤ 3k. In particular L 2k+2 k+1 (1) = L 2k+1 k (1). Moreover for al… view at source ↗
read the original abstract

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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper generalizes Hofstadter's G-function (G(0)=0, G(n)=n-G(G(n-1))) to a family F_k by varying the number k of nested recursive calls, establishes the pointwise ordering F_k(n) ≤ F_{k+1}(n) for all k,n via properties of infinite morphic words (lengths of substituted prefixes and letter occurrence counts), relates lim F_k(n)/n to letter frequencies, and supplies a complete Rocq formalization of all results.

Significance. The pointwise ordering for this family of recursive functions is of interest in discrete mathematics and combinatorics on words. The complete machine-checked Rocq formalization of the morphic-word length/occurrence properties, frequency limits, and resulting inequalities supplies external verification and is a notable strength of the work.

minor comments (2)
  1. [Abstract] The abstract states that results are machine-checked but does not specify the exact version of Rocq or the libraries used; adding this would aid reproducibility.
  2. Notation for the generalized substitution rules could be clarified with an explicit table listing the rules for small k (e.g., k=1,2,3) to help readers track the morphic-word construction.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive evaluation of our manuscript, for highlighting the interest of the pointwise ordering result in discrete mathematics and combinatorics on words, and for recommending acceptance. We are particularly pleased that the complete Rocq formalization was noted as a strength.

Circularity Check

0 steps flagged

No significant circularity; derivation self-contained via Rocq formalization

full rationale

The central claim (pointwise ordering F_k(n) ≤ F_{k+1}(n)) is established by proving length/occurrence properties of generalized morphic words, relating F_k(n)/n limits to letter frequencies, and certifying the entire argument in Rocq. This machine-checked verification against the proof assistant's axioms constitutes independent external support rather than any reduction to self-definition, fitted parameters renamed as predictions, or load-bearing self-citations. No steps in the provided derivation chain match the enumerated circularity patterns.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The proof rests on standard mathematical properties of recursive definitions over natural numbers and on combinatorial facts about morphic words generated by substitutions; no free parameters or new entities are introduced.

axioms (2)
  • standard math Natural numbers are well-ordered and support standard induction and recursion.
    Invoked implicitly for the recursive definitions of F_k and for proofs about prefixes.
  • domain assumption Substitution rules on finite alphabets generate infinite morphic words whose prefix lengths and letter counts obey the stated recurrence relations.
    Central to the detour that connects the recursive functions to letter frequencies.

pith-pipeline@v0.9.0 · 5730 in / 1317 out tokens · 51999 ms · 2026-05-25T08:11:18.783441+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

  • IndisputableMonolith.Constants phi_golden_ratio echoes
    ?
    echoes

    ECHOES: this paper passage has the same mathematical shape or conceptual pattern as the Recognition theorem, but is not a direct formal dependency.

    F2(n)=⌊(n+1)/ϕ⌋ where ϕ is the golden ratio; freqk(i)=α_k^{i-1}; lim 1/n Fj_k(n)=α^j_k with α2=1/ϕ

  • IndisputableMonolith.Foundation.ArithmeticFromLogic embed_strictMono_of_one_lt echoes
    ?
    echoes

    ECHOES: this paper passage has the same mathematical shape or conceptual pattern as the Recognition theorem, but is not a direct formal dependency.

    Galois connection F^j_k and L^j_k; pointwise monotonicity Fk ≤ Fk+1 proved via word lengths and letter counts

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

21 extracted references · 21 canonical work pages · 1 internal anchor

  1. [1]

    OEIS Foundation Inc. (2024). The on-line encyclopedia of intege r sequences. Published electronically at https://oeis.org

    work page 2024

  2. [2]

    Jean-Paul Allouche, Julien Cassaigne, Jeffrey Shallit, and Luca Q. Zamboni. A taxonomy of morphic sequences, 2017. arXiv:1711.10807

    work page internal anchor Pith review Pith/arXiv arXiv 2017

  3. [3]

    Automatic Sequences: Theory, Applications, Generalizati ons

    Jean-Paul Allouche and Jeffrey Shallit. Automatic Sequences: Theory, Applications, Generalizati ons. Cambridge University Press, 2003

    work page 2003

  4. [4]

    Downey and Ralph E

    Peter J. Downey and Ralph E. Griswold. On a family of nested recur sions. Fibonacci Quarterly , 22(4):310–317, 1984

    work page 1984

  5. [5]

    Anderson

    Larry Ericksen and Peter G. Anderson. Patterns in differences between rows in k-zeckendorf arrays. Fibonacci Quarterly, 50(1):11–18, 2012. 18

    work page 2012

  6. [6]

    Pytheas Fogg

    N. Pytheas Fogg. Substitutions in dynamics, arithmetics and combinatorics , volume 1794 of Lecture Notes in Mathematics . Springer-Verlag, Berlin, 2002. Edited by V. Berth´ e, S. Ferencz i, C. Mauduit and A. Siegel

    work page 2002

  7. [7]

    Complexity of infinite words associated with beta-expansions

    Christiane Frougny, Zuzana Mas´ akov´ a, and Edita Pelantov´ a. Complexity of infinite words associated with beta-expansions. RAIRO Theor. Informatics Appl. , 38(2):163–185, 2004

    work page 2004

  8. [8]

    Erratum: Corrigendum: Complexity of infinite words associated with beta-expansions

    Christiane Frougny, Zuzana Mas´ akov´ a, and Edita Pelantov´ a. Erratum: Corrigendum: Complexity of infinite words associated with beta-expansions. RAIRO Theor. Informatics Appl. , 38(3):269–271, 2004

    work page 2004

  9. [9]

    Gault and M

    D. Gault and M. Clint. ”Curiouser and curiouser” said Alice. Furthe r reflections on an interesting recursive function. Int. J. Comput. Math. , 26(1):35–43, 1988

    work page 1988

  10. [10]

    Fraenkel

    Lior Goldberg and Aviezri S. Fraenkel. Patterns in the generaliz ed Fibonacci word, applied to games. Discrete Mathematics, 341(6):1675–1687, 2018

    work page 2018

  11. [11]

    Saunders

    Kevin Hare and J.C. Saunders. Generalised Fibonacci sequence s constructed from balanced words. Journal of Number Theory , 231:349–377, 2022

    work page 2022

  12. [12]

    Hofstadter

    Douglas R. Hofstadter. G¨ odel, Escher, Bach: An Eternal Golden Braid. Basic Books, Inc, NY, 1979

    work page 1979

  13. [13]

    The Zeckendorf array equals the Wythoff arra y

    Clark Kimberling. The Zeckendorf array equals the Wythoff arra y. Fibonacci Quarterly, 33(1):3–8, 1995

    work page 1995

  14. [14]

    Coq proofs about Hofstadter’s function G

    Pierre Letouzey. Coq proofs about Hofstadter’s function G. 2015–2024. https://github.com/letouzey/hofstadter g

    work page 2015

  15. [15]

    Hofstadter’s problem for curious readers, 2015

    Pierre Letouzey. Hofstadter’s problem for curious readers, 2015. Research Report, Universit´ e Paris Diderot and INRIA Paris. https://inria.hal.science/hal-01195587v4/document

    work page 2015

  16. [16]

    Meek and G.H.J

    D.S. Meek and G.H.J. Van Rees. The solution of an iterated recurr ence. Fibonacci Quarterly , 22(2):101–104, 1984

    work page 1984

  17. [17]

    Dekking F. Michel. On Hofstadter’s G-Sequence. Journal of Integer Sequences , 26:23.9.2, 2023

    work page 2023

  18. [18]

    Ram ´ ırez, Gustavo N

    Jos´ e L. Ram ´ ırez, Gustavo N. Rubiano, and Rodrigo De Castro . A generalization of the Fibonacci word fractal and the Fibonacci snowflake. Theoretical Computer Science , 528:40–56, 2014

    work page 2014

  19. [19]

    Jeffrey O. Shallit. Proving properties of some greedily-defined in teger recurrences via automata theory. Theoretical Computer Science , 988:114363, 2024

    work page 2024

  20. [20]

    Some properties of the Tribonacci seq uence

    Bo Tan and Zhi-Ying Wen. Some properties of the Tribonacci seq uence. European Journal of Com- binatorics, 28(6):1703–1719, 2007

    work page 2007

  21. [21]

    The Coq proof assistant

    The Coq Development Team. The Coq proof assistant. 1985–20 24. https://coq.inria.fr. (P.L.) Universit ´ e Paris Cit ´ e, CNRS, Inria, IRIF, F-75013 Paris, France Email address : letouzey@irif.fr (S.L.) Department of Mathematics and Statistics, Universi ty of Winnipeg 515 Portage A venue, Winnipeg, MB, R3B 2E9, Canada Email address : sh.li@uwinnipeg.ca (W....

    work page 1985