pith. sign in

arxiv: 2603.29622 · v2 · pith:UYCYPB6Lnew · submitted 2026-03-31 · 🧮 math.CO · math.NT

Certified Finite-State Induction for a Perturbed Hofstadter Recursion

Marco Mantovanelli This is my paper

Pith reviewed 2026-05-21 10:23 UTC · model grok-4.3

classification 🧮 math.CO math.NT
keywords Hofstadter recursionfinite-state inductioncomputer certificationwell-defined recursionsymbolic modelparity perturbationcombinatoricsrecursive sequences
0
0 comments X

The pith

A perturbed Hofstadter recursion is well-defined for every positive integer via certified finite-state induction.

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

The paper studies a recursion that modifies the classic Hofstadter form by adding an alternating sign based on parity. It seeks to prove that the recursion never fails to produce a defined value no matter how large n becomes. The proof begins with a directly checked initial segment of the sequence and extracts a compact symbolic model that represents every reachable state. Computer checkers then confirm that this model is closed under the recursion rules, that its cycles are properly factored, and that no path leads to an undefined call. Minimal-counterexample induction then lifts the local verification to a global guarantee that the sequence exists for all n.

Core claim

The recursion defined by Q(1) = Q(2) = 1 and Q(n) = Q(n - Q(n-1)) + Q(n - Q(n-2)) + (-1)^n is well-defined for every integer n at least 1. The proof proceeds by building a finite symbolic recursive model from a verified initial trace, exporting a machine-readable certificate consisting of symbolic word systems, context records, and arithmetic recurrences, and having independent checkers verify symbolic closure, cycle factorization, faithfulness to the trace, arithmetic correctness, and strict backwardness of dependencies. Exhaustiveness of the finite model together with minimal-counterexample induction rules out any first undefined recursive call at larger n.

What carries the argument

The finite symbolic recursive model extracted from the initial trace, which encodes all possible future behaviors as a closed transition system whose verification rules out undefined calls.

If this is right

  • The sequence Q(n) produces a defined integer for every positive integer n.
  • Global well-definedness follows from local closure properties of the finite model rather than from the length of any computed trace.
  • The same certificate format can certify other recursive sequences that risk undefined calls at large arguments.
  • Independent checkers can re-verify the result without recomputing the entire sequence.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Similar finite-state certification could be attempted for other Hofstadter-like recursions that include different perturbations or additional terms.
  • The method separates the discovery of a candidate model from its machine-checked proof, which may allow reuse across families of recursive definitions.
  • One could search for the smallest perturbation that makes a related recursion undefined and compare the resulting model size with the one obtained here.

Load-bearing premise

The finite symbolic recursive model extracted from the initial trace is exhaustive and captures every possible future behavior of the recursion.

What would settle it

An explicit n at which the recursion first attempts to call a non-positive index, or an independent run of the checkers that reports a violation of closure or cycle factorization in the exported certificate.

Figures

Figures reproduced from arXiv: 2603.29622 by Marco Mantovanelli.

Figure 1
Figure 1. Figure 1: The compatibility graph (Λadm, Ψ). The graph has two connected components, corre￾sponding to debt 0 and debt 2. Solid arrows indicate the principal chain structure inside the regimes R1, R2, and R3; dashed arrows indicate the additional compatibility edges from the full explicit list in Appendix B. 9 [PITH_FULL_IMAGE:figures/full_fig_p009_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Automaton-style rendering of the compressed successor relation. Ordinary circles denote [PITH_FULL_IMAGE:figures/full_fig_p039_2.png] view at source ↗
read the original abstract

We study the parity-perturbed Hofstadter-type recursion $$ Q(1)=Q(2)=1,\qquad Q(n)=Q(n-Q(n-1))+Q(n-Q(n-2))+(-1)^n . $$ We prove, by computer-certified finite-state induction, that this recursion is well-defined for all $(n\ge 1)$. The proof extracts a finite symbolic recursive model from a directly verified initial trace and then verifies an exported machine-readable certificate by independent checkers. The certificate consists of finite symbolic word systems, radius-$(R)$ contexts, context-extension records, symbolic realizations, and arithmetic recurrence records. The checkers verify symbolic closure, cycle factorization, faithfulness to an independently recomputed trace, arithmetic correctness, parity consistency, and strict backwardness of all certified recursive dependencies. The length of the computed trace is not used as evidence for global well-definedness. Instead, exhaustiveness is certified over the declared finite symbolic transition system. Together with a minimal-counterexample induction, the finite certificate rules out a first undefined recursive call.

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

1 major / 0 minor

Summary. The paper claims to prove, via computer-certified finite-state induction, that the parity-perturbed Hofstadter recursion Q(1)=Q(2)=1, Q(n)=Q(n-Q(n-1))+Q(n-Q(n-2))+(-1)^n is well-defined for all n≥1. The proof extracts a finite symbolic recursive model (with radius-R contexts, context-extension records, and cycle factorization) from a directly verified initial trace, then verifies an exported machine-readable certificate by independent checkers for symbolic closure, faithfulness to a recomputed trace, arithmetic correctness, parity consistency, and strict backwardness. Minimal-counterexample induction is combined with the certified closure to rule out any first undefined recursive call; the trace length itself is not used as evidence for global well-definedness.

Significance. If the certification is complete, the result establishes well-definedness for this specific recursion and introduces a reusable methodology of finite-state induction with machine-readable certificates and independent checkers. This approach avoids circularity in trace-length arguments and could apply to other Hofstadter-type or recursive combinatorial sequences where direct analytic proofs are difficult. The explicit separation of model extraction, certificate export, and checker verification is a methodological strength that enhances verifiability.

major comments (1)
  1. [Proof outline and symbolic model description] The exhaustiveness of the finite symbolic recursive model is load-bearing for the central claim. The manuscript asserts that the model extracted from the initial trace (via radius-R contexts and context-extension records) captures every possible future evolution, so that certified closure plus strict backwardness rules out undefined calls at any larger n. However, the step guaranteeing that no new states or arithmetic combinations arise beyond the trace is not independently secured by an additional checker or explicit argument; any missed reachable context would allow a path to an undefined call outside the certified system. This needs a concrete justification or supplementary verification in the section describing model extraction and the minimal-counterexample argument.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful reading of the manuscript and for the positive evaluation of its significance and methodological contributions. We address the single major comment below, agreeing that additional clarification on model exhaustiveness is warranted.

read point-by-point responses

  1. Referee: The exhaustiveness of the finite symbolic recursive model is load-bearing for the central claim. The manuscript asserts that the model extracted from the initial trace (via radius-R contexts and context-extension records) captures every possible future evolution, so that certified closure plus strict backwardness rules out undefined calls at any larger n. However, the step guaranteeing that no new states or arithmetic combinations arise beyond the trace is not independently secured by an additional checker or explicit argument; any missed reachable context would allow a path to an undefined call outside the certified system. This needs a concrete justification or supplementary verification in the section describing model extraction and the minimal-counterexample argument.

    Authors: We agree that the manuscript would benefit from a more explicit argument establishing that the extracted finite symbolic model is exhaustive for all reachable contexts. The current proof relies on the symbolic closure checker (which verifies that every transition under the recursion rules stays inside the declared set of radius-R contexts and extension records) together with the minimal-counterexample induction and strict backwardness. To make the exhaustiveness step fully explicit, we will add a short lemma in the model-extraction section showing that any context arising after the initial trace must be an extension of a context already appearing in that trace; this follows from the local dependence structure of the recursion and the fact that all arithmetic combinations consistent with the parity perturbation are already realized in the verified prefix. We will also augment the exported certificate with a supplementary reachability check confirming that the symbolic transition system generates no external contexts. These additions will be placed immediately before the minimal-counterexample argument and will not alter the verified certificate or the independent checkers. revision: yes

Circularity Check

0 steps flagged

No significant circularity in certified finite-state induction

full rationale

The paper extracts a finite symbolic recursive model from a verified initial trace but then certifies exhaustiveness, symbolic closure, cycle factorization, faithfulness to a recomputed trace, arithmetic correctness, and strict backwardness using independent checkers on an exported machine-readable certificate. Global well-definedness follows from minimal-counterexample induction over this certified finite transition system rather than from the trace length or any fitted parameter. No step reduces by construction to its inputs, no self-citation is load-bearing, and the verification is externally checkable, rendering the derivation self-contained.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on standard mathematical assumptions about recursive definitions and induction, plus the correctness of the computer checkers and the exhaustiveness of the extracted symbolic model. No new free parameters or invented entities are introduced beyond the recursion itself.

axioms (2)
  • standard math Standard principle of mathematical induction and minimal-counterexample reasoning apply to the positive integers.
    Invoked to combine the finite model check with the argument that rules out any first undefined call.
  • domain assumption The independent checkers correctly verify symbolic closure, cycle factorization, faithfulness to the trace, and arithmetic correctness.
    The proof delegates verification to these checkers; their soundness is assumed rather than re-proven inside the paper.

pith-pipeline@v0.9.0 · 5707 in / 1548 out tokens · 52053 ms · 2026-05-21T10:23:40.106704+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.

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

20 extracted references · 20 canonical work pages

  1. [1]

    A. Alkan. On a generalization of Hofstadter’s Q-sequence: A family of chaotic generational structures.Complexity, page Article 8517125, 2018

    work page 2018

  2. [2]

    Alkan, N

    A. Alkan, N. Fox, and O. O. Aybar. On Hofstadter heart sequences.Complexity, page Article 2614163, 2017

    work page 2017

  3. [3]

    Balamohan, A

    B. Balamohan, A. Kuznetsov, and S. Tanny. On the behavior of a variant of Hofstadter’s Q-sequence.Journal of Integer Sequences, 10:Article 07.1.2, 2007

    work page 2007

  4. [4]

    Bodirsky and D

    M. Bodirsky and D. Kr´ al’. Locally consistent constraint satisfaction problems with binary constraints. InGraph-Theoretic Concepts in Computer Science, volume 3787 ofLecture Notes in Computer Science, pages 235–246. Springer, 2005

    work page 2005

  5. [5]

    J. M. Campbell and B. Cloitre. Meta-automatic sequences.arXiv preprint, 2026. 40

    work page 2026

  6. [6]

    Celaya and Frank Ruskey

    M. Celaya and Frank Ruskey. An undecidable nested recurrence relation. InHow the World Computes, volume 7318 ofLecture Notes in Computer Science, pages 138–149. Springer, 2012

    work page 2012

  7. [7]

    Finding linear-recurrent solutions to Hofstadter-like recurrences using symbolic computation.arXiv preprint, 2016

    Nathan Fox. Finding linear-recurrent solutions to Hofstadter-like recurrences using symbolic computation.arXiv preprint, 2016

    work page 2016

  8. [8]

    A new approach to the Hofstadter Q-recurrence.arXiv preprint, 2018

    Nathan Fox. A new approach to the Hofstadter Q-recurrence.arXiv preprint, 2018

    work page 2018

  9. [9]

    The behavior of a three-term Hofstadter-like recurrence with linear initial condi- tions.arXiv preprint, 2024

    Nathan Fox. The behavior of a three-term Hofstadter-like recurrence with linear initial condi- tions.arXiv preprint, 2024

    work page 2024

  10. [10]

    Oxford University Press, 2004

    Pavol Hell and Jaroslav Neˇ setˇ ril.Graphs and Homomorphisms. Oxford University Press, 2004

    work page 2004

  11. [11]

    Hofstadter.G¨ odel, Escher, Bach: An Eternal Golden Braid

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

    work page 1979

  12. [12]

    Entry a394051 in the on-line encyclopedia of integer sequences.https: //oeis.org/A394051, 2026

    OEIS Foundation Inc. Entry a394051 in the on-line encyclopedia of integer sequences.https: //oeis.org/A394051, 2026. Accessed: 2026-03-31

    work page 2026

  13. [13]

    Cam- bridge University Press, 1995

    Douglas Lind and Brian Marcus.An Introduction to Symbolic Dynamics and Coding. Cam- bridge University Press, 1995

    work page 1995

  14. [14]

    Dyadic self-similarity in a perturbed Hofstadter recursion.arXiv preprint, 2026

    Marco Mantovanelli. Dyadic self-similarity in a perturbed Hofstadter recursion.arXiv preprint, 2026

    work page 2026

  15. [15]

    a finite-state proof of the well- definedness of a perturbed Hofstadter sequence

    Marco Mantovanelli. Verification code for “a finite-state proof of the well- definedness of a perturbed Hofstadter sequence”.https://github.com/Mantovanelli1110/ perturbed-hofstadter-well-definedness, 2026. Version corresponding to the paper

    work page 2026

  16. [16]

    Order and chaos in Hofstadter’s Q-sequence.Complexity, 4(3):41–46, 1999

    Klaus Pinn. Order and chaos in Hofstadter’s Q-sequence.Complexity, 4(3):41–46, 1999

    work page 1999

  17. [17]

    Stephen M. Tanny. A well-behaved cousin of the Hofstadter sequence.Discrete Mathematics, 105:227–239, 1992

    work page 1992

  18. [18]

    Trojovsk´ y

    P. Trojovsk´ y. On some properties of a meta-fibonacci sequence connected to Hofstadter se- quence and m¨ obius function.Chaos, Solitons & Fractals, 134:109719, 2020

    work page 2020

  19. [19]

    Trojovsk´ y

    P. Trojovsk´ y. On some properties of the Hofstadter–Mertens function.Complexity, page Article 1816756, 2020

    work page 2020

  20. [20]

    On properties of Hofstadter’s Q-sequence.Chaos, Solitons & Fractals, 133:109644, 2020

    Pavel Trojovsk´ y. On properties of Hofstadter’s Q-sequence.Chaos, Solitons & Fractals, 133:109644, 2020. 41

    work page 2020