Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 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.

Ostrowski's theorem for the rationals

Statement

Let ∣⋅∣ be a nontrivial absolute value on Q in the sense of Absolute values on a field. Then exactly one of the following holds.

  1. ∣⋅∣ is equivalent to the usual absolute value on Q.
  2. There is a unique prime p such that ∣⋅∣ is equivalent to ∣⋅∣p of The p-adic absolute value on the rationals.

Facts & Assumptions

Proof

technique · cases
1.1L1L2L3L4assume-case nonarchimedean

Assume as the first case that ∣n∣≤1 for every integer n. Then [L1] makes ∣⋅∣ nonarchimedean. Because the absolute value is nontrivial, there is an integer m with ∣m∣≠1; the inequality ∣m∣≤1 forces ∣m∣<1, so some prime divisor p of m has ∣p∣<1 by [L4]. If also ∣q∣<1 for a different prime q, then [L3] gives up+vq=1, and the nonarchimedean inequality yields 1=∣1∣≤max⁡{∣u∣∣p∣,∣v∣∣q∣}<1, impossible because integers all have absolute value at most 1. Thus there is a unique prime p with ∣p∣<1.

1.2L4givenassume-case archimedeanalgebra

Assume as the second case that ∣n∣>1 for some integer n. Choosing a prime divisor of n and using [L4], at least one prime p satisfies ∣p∣>1. Put α:=log⁡∣p∣/log⁡p>0 and, for each integer t∈{0,…,p−1}, let Cp:=max⁡∣t∣. For every positive integer m, write the base-p expansion m=a0+a1p+⋯+arpr with 0≤ai<p. The triangle inequality gives ∣m∣≤∑i=0r∣ai∣ ∣p∣i≤Cp(r+1)∣p∣r≤Cp(1+log⁡pm) mα, because pr≤m<pr+1. Applying the same estimate to mk and taking k-th roots gives ∣m∣≤(Cp(1+klog⁡pm))1/kmα, so letting k→∞ yields ∣m∣≤mα. Now fix m>1 and put αm:=log⁡∣m∣/log⁡m. Writing pk in base m and repeating the same argument with m in place of p gives ∣p∣k≤Cm(1+klog⁡mp) pkαm for some constant Cm, hence ∣p∣≤pαm after taking k-th roots and letting k→∞. Therefore α≤αm. Since ∣m∣≤mα is exactly αm≤α, we get αm=α for every m>1. Thus ∣m∣=mα for every positive integer m, and then ∣a/b∣=∣a∣/∣b∣=∣a/b∣∞α for every nonzero rational.

2.1step 1.1L4L5algebra

For any prime q≠p, step 1.1 and [L3] applied to p and q give ∣q∣=1. Hence if x=±pka/b with p∤ab, uniqueness of factorisation [L4] gives ∣x∣=∣p∣k. Writing c:=−log⁡∣p∣/log⁡p>0, this becomes ∣x∣=∣x∣pc, so ∣⋅∣ is equivalent to ∣⋅∣p by [L5].

3.1step 2.1step 1.2L2cases-exhaustive∎

Step 2.1 gives the nonarchimedean case and step 1.2 gives the archimedean case, and the two cases are disjoint because [L2] says every p-adic absolute value is nonarchimedean. Therefore every nontrivial absolute value on Q is equivalent either to the usual absolute value or to a unique p-adic one.

Depends on

Used by

Dependency tree · two levels

51 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