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

An absolute value is nonarchimedean exactly when every integer has absolute value at most one

Statement

Let F be a field with absolute value ∣⋅∣ in the sense of Absolute values on a field. Then ∣⋅∣ is nonarchimedean if and only if

∣n⋅1F∣≤1

for every integer n.

Facts & Assumptions

Given: A field F and an absolute value ∣⋅∣ on F.

[L1]

An absolute value is multiplicative and satisfies both the ordinary and, in the nonarchimedean case, the strong triangle inequality (Absolute values on a field).

Proof

technique · direct
1.1L1givenalgebra

Since 1F≠0, multiplicativity in [L1] gives ∣1F∣=∣1F∣2, hence ∣1F∣=1. Also ∣−1∣2=∣1∣=1, so ∣−1∣=1.

1.2L1givenalgebra

Assume conversely that ∣n1F∣≤1 for every integer n. Fix x,y∈F and put M:=max⁡{∣x∣,∣y∣}. If M=0 there is nothing to prove, so scale by a nonzero element and reduce to M=1. Then every binomial coefficient has absolute value at most 1, so ∣(x+y)m∣≤max⁡0≤k≤m∣(mk)∣ ∣x∣k∣y∣m−k≤1 for every m≥1. Hence ∣x+y∣m≤1 for all m, so ∣x+y∣≤1=M. Undoing the scaling gives ∣x+y∣≤max⁡{∣x∣,∣y∣}.

2.1L1step 1.1induction

Assume first that ∣⋅∣ is nonarchimedean. For n≥1, induction using step 1.1 and ∣(n+1)1F∣≤max⁡{∣n1F∣,∣1F∣} gives ∣n1F∣≤1. For negative n, ∣n1F∣=∣−1∣ ∣(−n)1F∣≤1, and ∣0∣=0≤1.

3.1step 2.1step 1.2∎

Thus the integer bound implies the strong triangle inequality, and step 2.1 proved the reverse implication.

Depends on

Used by

Dependency tree · one level

1 result within one dependency step 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