Papers With

← All papers
First page of $p$-adic Hahn series with sparse support

$p$-adic Hahn series with sparse support

Shanwen Wang, Yijun Yuan

math.NT Jul 8, 2026 · v1 math.CO
formalization number-theory
Read PDF arXiv abstract
TL;DR
Fully formalizes transcendence results for sparse-support p-adic Hahn series in Lean 4 over Mathlib.
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.
Problem

Determining transcendence of p-adic Hahn series over the completed maximal unramified extension of Q_p, and addressing an order-type conjecture for algebraic Hahn series with bounded support.

Approach

A sparseness condition on the supports of p-adic Hahn series is introduced and shown to imply transcendence over the completed maximal unramified extension of Q_p. This is applied to the order-type conjecture for Q_p-algebraic p-adic Hahn series with bounded support having finitely many accumulation points. All results were formalized in the Lean 4 theorem prover (v4.31.0) using Mathlib.

Results

The sparseness condition implies transcendence, and the order-type conjecture is proved under the finitely-many-accumulation-points condition. The full development is verified in Lean.