$p$-adic Hahn series with sparse support

Abstract

Let $p$ be a prime number. We introduce a sparseness condition on the supports of $p$-adic Hahn series, and prove that this condition implies transcendence over ${\breve{\mathbf{Q}}}_p$, the completed maximal unramified extension of ${\mathbf{Q}}_p$. As an application, we prove the order-type conjecture of ${\mathbf{Q}}_p$-algebraic $p$-adic Hahn series with bounded support under the condition that the support has only finitely many accumulation points. All results in this paper have been fully formalized in the Lean theorem prover (v 4.31.0), building over Mathlib.

30 pages. Formalized code available at https://github.com/YijunYuan/FormalizedSparse