AI 中文总结
研究 $(3/2)^n$ 控制字的子字复杂度，利用相关结果证明其为超线性，论证在Lean - 4中完全形式化，仅依赖子空间定理。
AI 中文摘要
将 $(3/2)^n = m_n + \eps_n$，其中 $m_n$ 为最接近的整数且 $\eps_n\in[-\tfrac12,\tfrac12)$，令 $T=(t_n)$，$t_n=2m_{n + 1}-3m_n$ 为所得的控制字。利用相关结果证明了 $T$ 的子字复杂度 $\pT(k)$ 是超线性的，即 $\pT(k)/k\to\infty$。该论证在Lean - 4中完全形式化，仅依赖于子空间定理。
英文摘要
Write $(3/2)^n = m_n + \varepsilon_n$ with $m_n$ the nearest integer and $\varepsilon_n\in[-\tfrac12,\tfrac12)$, and let $T=(t_n)$, $t_n=2m_{n+1}-3m_n$, be the resulting \emph{steering word}: the step-by-step record of the map $x\mapsto\tfrac32 x$ on the orbit of 1, coded by nearest-integer rounding. Using results by Corvaja--Zannier and Nair--Kumar--Rout we prove that the subword complexity $p_{T}(k)$ of $T$ is superlinear, $p_{T}(k)/k\to\infty$. The argument is completely formalized in Lean~4 and rests on a single external input, the Evertse--Schlickewei $S$-arithmetic subspace theorem, from which both cited results are themselves derived within the formalization.
Commentsadded figures
