Certified Finite-State Induction for a Perturbed Hofstadter Recursion

TL;DR

This paper presents a computer-certified finite-state induction proof demonstrating that a parity-perturbed Hofstadter recursion is well-defined for all positive integers, using symbolic models and independent checkers.

Contribution

It introduces a novel finite-state certification method for recursive definitions, extracting and verifying symbolic models to ensure global well-definedness.

Findings

Proves the recursion is well-defined for all n ≥ 1

Develops a symbolic recursive model and verification framework

Uses independent checkers to validate the certification

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.