针对扰动的霍夫达特递归的认证有限状态归纳
Certified Return-Word Induction for a Perturbed Hofstadter Recursion
AI总结：
本文研究了一种扰动的霍夫达特型递归，并通过计算机认证的有限状态归纳法证明了该递归对所有n≥1都是良定义的。
摘要：
我们研究了扰动的霍夫达特型递归 $$ Q(1)=Q(2)=1,\qquad Q(n)=Q(n-Q(n-1))+Q(n-Q(n-2))+(-1)^n . $$ 通过计算机认证的有限状态归纳法证明，该递归对所有$(n\ge 1)$都是良定义的。证明从直接验证的初始轨迹中提取出有限符号递归模型，然后通过独立检查者验证导出的机器可读证书。证书由有限符号词系统、半径为$(R)$的上下文、上下文扩展记录、符号实现以及算术递归记录组成。检查者验证符号闭包、循环因子分解、对独立重新计算的轨迹的忠实性、算术正确性、奇偶一致性以及所有认证递归依赖的严格逆向性。计算的轨迹长度不作为全局良定义性的证据。相反，通过声明的有限符号转移系统的穷尽性进行认证。结合最小反例归纳法，有限证书排除了第一个未定义的递归调用。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
