Certified Return-Word Induction for a Perturbed Hofstadter Recursion

Abstract

We study the parity-perturbed Hofstadter recursion $$ Q(1)=Q(2)=1,\qquad Q(n)=Q(n-Q(n-1))+Q(n-Q(n-2))+(-1)^n. $$ We prove that it is well-defined for every $n\ge 1$ by a computer-assisted return-word induction. The recurrence is first reduced to a binary sequence $s_n$ together with two backward cursor heads. Its local semantics is encoded by 13 return-word types, 92 synchronized cursor states, and 122 exact two-source transition rules. Exhaustive finite checks verify the local recurrence identity, cursor synchronization, rule selection, and exclusion of the unique configuration that could produce a nonbinary value. The global argument is not inferred from a long finite trace. Instead, all unbounded word families are handled by explicit induction: four stationary chunk families and four linear bridge-tail families reduce to ten parameterized zero-loop schemas. Ordered rank-word factorizations assemble complete epochs and bridges at every level. A marked factor induction then propagates absolute source-block addresses through the resulting four-factor cycle, while a finite potential certificate yields the uniform lag bounds $$ j-p_A\ge 38,\qquad j-p_B\ge 38, $$ so every source read lies strictly in the previously generated prefix. Finally, defining $Q(n)=n+1-T_{n+1}$ from the constructed binary system gives a two-periodic recurrence residual that vanishes in the two base cases. Hence the original recursion holds globally, all recursive arguments are positive and strictly smaller than the current index, and the sequence is uniquely determined.