$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.

Disclosure

“{ f : 𝕃_[p] | ∃ f' : HahnSeries ℚ (𝔽ᵃ_[p]), IsAlgebraic 𝔽ᵃ_[p] f' ∧ (exists_canonical_expansion f).choose.val = f'.coeff } := by admit A.2. AI-assisted formalization. — The agentic auto-formalization system Archon, which is based on Claude Opus 4.8 and developed by the AI4Math team at BICMR, Peking University, greatly accelerated our formalization process. By design, once the blueprint or the corresponding informal proof of the project is provided, Archon works fully autonomously”

PDF page 28

Classification

Code generation, completion, or debugging

Multiplier

2

Verified

2026-08-24T00:34:15.228Z

Structural counts