TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-04

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Every p-adic number has a unique digit expansion

Statement

Every nonzero $x \in Q_{p}$ can be written uniquely in the form

$x = \sum_{n = N}^{\infty} a_{n} p^{n},$

where $N \in Z$ , $a_{N} \neq 0$ , and each digit $a_{n}$ lies in ${0, \dots, p - 1}$ . The zero element has the all-zero expansion.

Facts & Assumptions

Given: A prime $p$ and an element $x \in Q_{p}$ .

[L1]

$Q_{p}$ is the fraction field of $Z_{p}$ (The p-adic completion agrees with the fraction field of Z_p).

[L2]

$Z_{p}$ is the closed unit ball of $Q_{p}$ (Z_p is the valuation ring of Q_p).

[L3]

$Q$ embeds densely in $Q_{p}$ because $Q_{p}$ is the $p$ -adic metric completion (The p-adic numbers as a metric completion).

[L4]

$Q_{p}$ is a complete valued field (The p-adic completion is a complete valued field).

Proof

technique · constructive

1.1

If $x = 0$ , take every digit $a_{n} = 0$ . Now assume $x \neq 0$ . By the density statement in [L3], choose $q \in Q$ with $∣ x - q ∣_{p} < ∣ x ∣_{p}$ . The ultrametric inequality from [L4] then gives $∣ q ∣_{p} = ∣ x ∣_{p}$ . Write $q = p^{N} a / b$ with $N \in Z$ and integers $a, b$ not divisible by $p$ ; then $∣ q ∣_{p} = p^{- N}$ , so $∣ x ∣_{p} = p^{- N}$ . Put $u : = p^{- N} x$ . Then $∣ u ∣_{p} = 1$ , so $u \in Z_{p}$ by [L2], and also $∣ u^{- 1} ∣_{p} = 1$ , so $u^{- 1} \in Z_{p}$ . Hence $u \in Z_{p}^{\times}$ .

L2L3L4givenchoosealgebra

2.1

In the compatible-residue description of $Z_{p}$ from [L1], for each $m \geq 1$ choose the unique digits $a_{0}, \dots, a_{m - 1} \in {0, \dots, p - 1}$ such that $u \equiv a_{0} + a_{1} p + \dots + a_{m - 1} p^{m - 1} (m o d p^{m}) .$ Because $u$ is a unit, its residue modulo $p$ is nonzero, so $a_{0} \neq 0$ . Writing $s_{m} : = \sum_{j = 0}^{m - 1} a_{j} p^{j}$ , one has $u - s_{m} \in p^{m} Z_{p}$ , hence $∣ u - s_{m} ∣_{p} \leq p^{- m}$ . So $(s_{m})$ is Cauchy and converges to $u$ by [L4]. Multiplying by $p^{N}$ gives $x = \sum_{m = 0}^{\infty} a_{m} p^{m + N};$ renaming the digits by index shift yields the claimed expansion with leading digit $a_{N} = a_{0} \neq 0$ .

L1L2L4step 1.1chooseconstruct

3.1

For uniqueness, suppose $\sum_{n = N}^{\infty} a_{n} p^{n} = \sum_{n = M}^{\infty} b_{n} p^{n}$ with digits in ${0, \dots, p - 1}$ and nonzero leading digits. Equality of absolute values forces $N = M$ . If $a_{n} \neq b_{n}$ first occurs at $n = k$ , then the difference of the two series equals $(a_{k} - b_{k}) p^{k} + p^{k + 1} y$ for some $y \in Z_{p}$ . Since $a_{k} - b_{k}$ is not divisible by $p$ , that difference has $p$ -adic absolute value $p^{- k}$ and cannot be $0$ . Therefore all digits agree.

step 2.1L2algebra

4.1

Thus every $p$ -adic number has a unique base- $p$ digit expansion.

step 2.1step 3.1constructdischarge-construct∎

Depends on

Used by

Qₚ is locally compact and totally disconnected Corollary
Zₚ is not the integral closure of Z in Qₚ Counterexample
The p-adic expansion of minus one Example

Dependency tree · two levels

12 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

J. S. Milne, Algebraic Number Theory, Proposition 7.26 (standard reference, not scraped)
Andrew V. Sutherland, 18.782 Lecture 8 (standard reference, not scraped)