Superlinear complexity of the $(3\mathrm{/}2{)}^n$ steering word

Write $(3\mathrm{/}2{)}^n=m_n+{\text{eps}}_n$ with $m_n$ the nearest integer and ${\text{eps}}_n\in [-\frac{1}{2},\frac{1}{2})$, 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 \frac{3}{2}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 $\text{pT}(k)$ of $T$ is superlinear, $\text{pT}(k)\mathrm{/}k\to \mathrm{\infty }$. The argument is completely formalized in Lean-4, depending only on the Subspace Theorem.