Papers With

← All papers
First page of Transcendence criteria for the minimal word of the rational base $3/2$

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

Ralf Stephan

math.NT Jul 18, 2026 · v2
formalization number-theory
Read PDF arXiv abstract Code
TL;DR
All results, including a special case of an Adamczewski–Faverjon transcendence theorem, are formalized in Lean 4 on top of a few cited axioms.
Abstract
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.
Problem

The constant K = lim x_n(2/3)^n, attached to the ceiling orbit x_{n+1} = ⌈3x_n/2⌉, has had its irrationality open since 1977. The paper relates K to the parity word w, which is the minimal word of the rational base 3/2 number system.

Approach

The identity 2x_{n+1} = 3x_n + w_n gives a series expansion of K in powers of 2/3. A 2-adic rigidity theorem identifies the length-m factors of w with the orbit residues mod 2^m, which yields linear complexity lower bounds. A Mahler-method transcendence result (Theorem A) then handles the algebraic irrational case, and a separate argument handles the rational case. The whole development is formalized in Lean 4, with axiom footprints checked via #print axioms.

Results

If w is automatic, then K is transcendental. Moreover, either the complexity of w exceeds every linear bound or K is irrational. Everything is machine-checked in Lean except a few cited literature inputs assumed as axioms and some computations in §6.3.