Transcendence criteria for the minimal word of the rational base $3/2$

RESUMO

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 $\omega_{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.