AI 中文总结
本文证明有理基数3/2的最小词若为自动词则对应常数K为超越数，并证明K的无理性与词复杂度超线性增长之间的二选一关系，且结果经Lean 4形式化验证。
AI 中文摘要
设 $x_{0}$ 为正整数，令 $x_{n}=\lceil 3x_{n-1}/2\rceil$，并令 $w_{n}=2x_{n+1}-3x_{n}\in\{0,1\}$ 为 Dubickas 所研究的关联词；对于 $x_{0}=1$，该轨道为 A061419，且 $w$ 是 Akiyama、Frougny 和 Sakarovitch 的有理基数记数系统的最小词 $g_{3/2}$。该轨道编码一个实常数 $K=\lim_{n}x_{n}(2/3)^{n}$，当 $x_{0}=1$ 时等于 $\omega_{3/2}=K(3)=1.6222705028\ldots$，其无理性自 1977 年以来一直悬而未决。我们证明：若 $w$ 是自动的，则 $K$ 是超越数；等价地，代数数 $K$ 迫使 $w$ 非自动。进一步，我们证明要么 $w$ 的复杂度超过一切线性界，要么 $K$ 是无理数。所有结果均在 Lean~4 证明助手中基于三条引用的公理得到形式化验证。
英文摘要
Let $x_{0}$ be a positive integer, let $x_{n}=\lceil 3x_{n-1}/2\rceil$, and let $w_{n}=2x_{n+1}-3x_{n}\in\{0,1\}$ be the associated word studied by Dubickas; for $x_{0}=1$ the orbit is A061419 and $w$ is the minimal word $g_{3/2}$ of the rational base number system of Akiyama, Frougny and Sakarovitch. The orbit encodes a real constant $K=\lim_{n}x_{n}(2/3)^{n}$, equal for $x_{0}=1$ to $ω_{3/2}=K(3)=1.6222705028\ldots$, whose irrationality has been open since 1977. We prove that if $w$ is automatic then $K$ is transcendental; equivalently, an algebraic $K$ forces $w$ to be non-automatic. Further we prove that either the complexity of $w$ exceeds every linear bound or $K$ is irrational. All results are formally verified in the Lean~4 proof assistant, on three cited axioms.
