Certified Finite-State Induction for a Perturbed Hofstadter Recursion
Fuente:
arXiv
Enregistré dans:
| Auteur principal: | |
|---|---|
| Format: | Preprint |
| Publié: |
2026
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866914577206214656 |
|---|---|
| author | Mantovanelli, Marco |
| author_facet | Mantovanelli, Marco |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_29622 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Certified Finite-State Induction for a Perturbed Hofstadter Recursion Mantovanelli, Marco Combinatorics Number Theory 11B37, 68Q45, 37B10, 03D25, 68Q60, 68W30 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. |
| title | Certified Finite-State Induction for a Perturbed Hofstadter Recursion |
| topic | Combinatorics Number Theory 11B37, 68Q45, 37B10, 03D25, 68Q60, 68W30 |
| url | https://arxiv.org/abs/2603.29622 |