Counterexamples to a late-iterate ordering conjecture for generalized Hofstadter functions

Dev D. Goyal

Counterexamples to a late-iterate ordering conjecture for generalized Hofstadter functions

Dev D. Goyal · 2026 · Research preprint, not externally peer reviewed

Problem and result

Problem: Letouzey–Li–Steiner late-iterate ordering conjecture for generalized Hofstadter functions
Posed in: Letouzey, Li and Steiner, Journal of Integer Sequences 29 (2026), Article 26.3.3, conjecture before Lemma 7.6
Status: Disproved
Result: For every k ≥ 4 some input n has Fₖ^(2k+1)(n) > Fₖ₊₁^(2k+2)(n), contradicting the conjectured order Fₖ^j ≤ Fₖ₊₁^(j+1) for j > 2k; an explicit witness is F₄⁹(132) = 8 > 7 = F₅¹⁰(132).

Abstract

For every k≥4, some input n satisfies Fₖ^(2k+1)(n)>Fₖ₊₁^(2k+2)(n). The proof constructs inverse iterates whose exact gap is k−3. The finite witness F₄⁹(132)=8>7=F₅¹⁰(132) gives the first instance. The result concerns infinitely many parameters, not infinitely many violating inputs for each fixed parameter.

Details

Year: 2026
Discipline: Mathematics
Area: Integer sequences and combinatorics
Subject: Integer sequences and combinatorics
Result type: Counterexamples for every parameter k≥4
Formal proof: Shared Lean library
Family: hofstadter-iteration
Keywords: Hofstadter functions, nested recursions, iterated functions, counterexample, integer sequences

Statement and scope

Result summary. The catalogue summary repeats the abstract above, including its stated limits. The formally checked statements are listed under Formal proof.

A Lean check establishes only the formal statement that is checked. It does not establish novelty, historical priority or a faithful transcription of an external source. Known gaps are listed in UNFINISHED.md; the authorship disclosure describes how the results were produced.

Manuscript

PDF on this site: manuscript.pdf 301 KB
PDF on GitHub: papers/mathematics/hofstadter-iteration/paper.pdf
LaTeX source: papers/mathematics/hofstadter-iteration/paper.tex
Bibliography: papers/mathematics/hofstadter-iteration/references.bib

Formal proof

The selected theorems of this result are proved in the shared Lean 4 library of the repository. Its Comparator configuration checks each one against the matching statement in the Challenge module and permits only the axioms propext, Classical.choice and Quot.sound.

Proof module: lean/MathAndTheory/Mathematics/Hofstadter/Family.lean
Family sources: lean/MathAndTheory/Mathematics/Hofstadter/
Challenge: lean/Challenges/Mathematics/Hofstadter/Main.lean
Solution interface: lean/Solutions/Mathematics/Hofstadter/Main.lean
Comparator file: lean/comparator/mathematics/hofstadter-iteration.json
Statement guide: lean/docs/mathematics/hofstadter-iteration.md
Toolchain: leanprover/lean4:v4.35.0

Checked theorems

Namespace MathAndTheory.Hofstadter.Family

HofstadterChallenge.result

Reproduce

The commands below are quoted from papers/mathematics/hofstadter-iteration/verification/README.md, which gives their context and working directory.

Reproduce the computation

python3 papers/mathematics/hofstadter-iteration/verification/scripts/verify.py

Reproduce the formal checks

cd lean
lake build MathAndTheory.Mathematics.Hofstadter.Family Solutions.Mathematics.Hofstadter.Main
lake env lean Solutions/Mathematics/Hofstadter/Main.lean

Reproduce the formal checks

bash scripts/verify-comparator.sh comparator/mathematics/hofstadter-iteration.json

README: papers/mathematics/hofstadter-iteration/README.md
Verification guide: papers/mathematics/hofstadter-iteration/verification/README.md
Repository guide: verification/README.md
Unfinished proofs: UNFINISHED.md

Source and prior work

Original problem. Letouzey, Li, and Steiner, Journal of Integer Sequences 29 (2026), 26.3.3, conjecture before Lemma 7.6.

Questions and answers

Is the Letouzey–Li–Steiner ordering conjecture for Hofstadter iterates true?

No. It asserts Fₖ^j(n) ≤ Fₖ₊₁^(j+1)(n) for all k ≥ 1, j > 2k and n; the preprint gives F₄⁹(132) = 8 > 7 = F₅¹⁰(132) and a violating input for every k ≥ 4 at j = 2k + 1. It does not claim infinitely many violating inputs for each fixed k or classify all iteration indices.

How does it relate to earlier comparisons?

The inverse relations and earlier comparisons are due to Letouzey, Li and Steiner, and Letouzey's Rocq development gives witnesses in this direction only for j ≤ 2k. No priority is claimed.

Is the proof formally verified?

Yes. Lean 4 constructs the functions on all natural numbers from their recurrence and proves both the finite witness and the family for every k ≥ 4.

Cite

Citation file papers/mathematics/hofstadter-iteration/citation.bib. For the whole collection, use CITATION.cff or CITATION.bib.

@misc{goyal2026hofstadter,
  author = {Dev D. Goyal},
  title = {Counterexamples to a late-iterate ordering conjecture for generalized Hofstadter functions},
  year = {2026},
  month = oct,
  howpublished = {Preprint},
  version = {1.0.0},
  url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/hofstadter-iteration},
  note = {Preprint, 26 October 2026. Not peer reviewed. Includes a Lean 4.35.0 formalization. See the collection's authorship disclosure for the autonomous research process.}
}