Alphabeta Math
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.

The inverse-limit topology on Zp agrees with the p-adic metric topology

Statement

The inverse-limit topology on Zp coincides with the topology induced by the metric dp.

Facts & Assumptions

Given: An element x=(xn) of Zp and an integer n1.

[F1]

The metric on Zp is defined by the largest initial block of equal residue coordinates (The p-adic metric on Zp is determined by the first coordinate at which two compatible residue systems differ).

[L1]

The inverse-limit topology is the subspace topology from the product of the discrete quotients, and cylinder traces form a basis (The inverse limit of finite groups carries the subspace topology from the product of discrete factors).

[L2]

An element of Zp is exactly a compatible residue-class tuple (The p-adic integers are the compatible residue-class tuples in the inverse limit of Z mod p^n).

Proof

technique · direct
1.1

Let Un(x):={y=(yr)Zp:yr=xr for 1rn}. By [F1], this is exactly the metric ball Un(x)={yZp:dp(x,y)pn}, because the first n residue coordinates agree if and only if the largest initial block of equal coordinates has length at least n.

F1L2givenalgebra
2.1

By [L1], the same set Un(x) is the trace on Zp of the cylinder in the product space that fixes the first n coordinates, so every basic metric ball is inverse-limit open. Conversely, let a basic inverse-limit cylinder C contain x and restrict the finite set of coordinates F. Taking nr for every rF, compatibility in [L2] shows that Un(x)C. Thus the sets Un(x) refine every inverse-limit neighbourhood of x.

L1L2step 1.1algebra
3.1

The sets Un(x) therefore form a neighbourhood basis for both topologies at every point x. So the inverse-limit topology and the metric topology coincide.

step 1.1step 2.1

Depends on

Used by

Dependency tree · two levels

7 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