Papers With

← All papers
First page of The order types of the supports of $p$-adic algebraic Hahn series

The order types of the supports of $p$-adic algebraic Hahn series

Shanwen Wang, Yijun Yuan

math.NT Oct 9, 2026 · v1
formalization number-theory mathlib ai-agents
Read PDF arXiv abstract Code
TL;DR
All main theorems are formalized sorry-free in Lean 4 with mathlib4, built by agentic autoformalization systems on a standalone library, TrustworthyKedlaya.
Abstract
Let $p$ be a prime number. In 1986, David Lampert asked if one expands a $\mathbf{Q}_p$-algebraic number as a $p$-adic Hahn series, then what is the possible order type of its support? In 2001, Kedlaya made a vague conjecture that the possible ordinals can only be finite ordinals, $ω$ and $ω^ω$, where $ω$ is the first infinite ordinal. In this article, we solve Lampert's problem by confirming Kedlaya's intuition. Moreover, we completely characterize the $\mathbf{Q}_p$-algebraic numbers with order type of support at most $ω$. As an application, we determine the bi-algebraic set of the $p$-adic shadow map.
Problem

Lampert asked in 1986 what order types can occur for the support of a Q_p-algebraic number expanded as a p-adic Hahn series. Kedlaya conjectured that the only possibilities are finite ordinals, ω, and ω^ω.

Approach

The authors establish a uniform upper bound on v_p(P(f_{≤B})) for truncations of algebraic Hahn series with positive essential rank. The bound comes from carry-free coefficient analysis, digit vectors, and interleavings of words. Comparing this bound with the growth forced by P(f)=0 rules out order types strictly between ω and ω^ω. All main results are formalized in Lean 4 with mathlib4 by the agentic systems Archon-Horizon and SHEAF, using a standalone library, TrustworthyKedlaya, for supporting results.

Results

Kedlaya's conjecture is confirmed, and Q_p-algebraic numbers with support order type at most ω are fully characterized. Algebraic series with bounded support are shown to have finite support, and the bi-algebraic set of the p-adic shadow map is determined. The formalization is sorry-free, uses only the standard axioms, and passes the Lean Comparator challenge.