嵌套递推的Padovan自动机描述
A Padovan-automatic description of a nested recurrence
- ChronoAI Pte Ltd（ChronoAI私人有限公司）
- The Omega Institute（欧米伽研究所）
- National University of Singapore (NUS)（新加坡国立大学）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
本文研究嵌套递推序列，通过贪心Padovan记数系统识别其结构，构造自动机验证递推，确定偏差界与偏移集，并给出显式态射表示及Lean形式化验证。
AI中文摘要：
我们研究序列 $a(0)=0$, $a(1)=1$ 以及对于 $n\ge 2$ 定义的 $a(n)=n-a(n-a(n-a(n-1)))$，该序列在整数序列在线百科中列为 A076502。我们将 $a(n)$ 识别为贪心 Padovan 记数系统中的两位移位，并带有有限状态修正。证明通过精确整数进位不变量构造加法自动机，并通过有限语言包含来验证其完备性；随后一个同步自动机验证嵌套递推。我们建立了与斜率 $c$ 的直线的有界偏差，其中 $c^3-c^2+2c-1=0$，并证明从 $\lfloor cn\rfloor$ 的偏移的精确集合是 $\{-1,0,1,2\}$。我们构造了第一差分词的显式 26 字母非擦除态射表示，证明其最小平衡常数为 4，并给出一个有效程序来将全局偏差极值封闭到任意精度。我们在 Lean 中形式化了递推识别、六位小数偏差界、精确偏移集合、具体态射恒等式、最小平衡常数以及有效极值算法。单独的精确计算细化了数值封闭。
英文摘要：
We study the sequence $a(0)=0$, $a(1)=1$ and $a(n)=n-a(n-a(n-a(n-1)))$ for $n\ge 2$, listed as A076502 in the On-Line Encyclopedia of Integer Sequences. We identify $a(n)$ as a two-position shift in the greedy Padovan numeration system, with a finite-state correction. The proof constructs an addition automaton from an exact integer-carry invariant and certifies its completeness by finite-language inclusion; a synchronized automaton then verifies the nested recurrence. We establish bounded discrepancy from the line of slope $c$, where $c^3-c^2+2c-1=0$, and show that the exact set of offsets from $\lfloor cn\rfloor$ is $\{-1,0,1,2\}$. We construct an explicit 26-letter non-erasing morphic presentation of the first-difference word, prove that its least balance constant is 4, and give an effective procedure for enclosing the global discrepancy extrema to arbitrary accuracy. We formalize the recurrence identification, six-decimal discrepancy bound, exact offset set, concrete morphic identity, least balance constant, and an effective extrema algorithm in Lean. Separate exact computations refine the numerical enclosures.
