Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07
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.

Unique extension of a nonarchimedean absolute value

Statement

For every finite field extension L/K with K complete nonarchimedean, the unique extending absolute value is xL=NL/K(x)K1/[L:K]. It is nonarchimedean and makes L complete. Separability and discreteness are not assumed; the trivial valuation is included.

Facts & Assumptions

Given: The data and hypotheses of the statement.

[F1]

Uniqueness of an extended complete field absolute value: For a finite extension E/F of a complete absolutely valued field F, at most one absolute value on E extends the given absolute value on F. Any such extension makes E complete.

[F2]

Irreducible polynomial coefficients in a complete valuation ring: Let F be complete nonarchimedean. If fF[T] is monic irreducible of positive degree and f(0)1, then every coefficient of f has absolute value at most one.

[F3]

Norm is multiplicative, trace is F-linear, and both are transitive in towers: Let K/F be a finite extension and let a,bK. 1. NK/F(ab)=NK/F(a)NK/F(b). 2. TrK/F(a+b)=TrK/F(a)+TrK/F(b) and TrK/F(ca)=cTrK/F(a) for every cF. 3. If L/K/F is a tower of finite extensions, then NL/F=NK/FNL/K,TrL/F=TrK/FTrL/K.

[F4]

Field norm and trace agree with the determinant and trace of multiplication by an element: Let K/F be a finite extension and let aK. If ma ⁣:KK,xax, is the F-linear multiplication operator, then NK/F(a)=det(ma),TrK/F(a)=tr(ma), where the right-hand side uses the published linear-operator determinant and trace.

Proof

1.1

Put n=[L:K] and v(x)=NL/K(x)1/n. The determinant interpretation shows that v vanishes exactly at zero and v(a)=a for aK, since multiplication by a is a scalar n by n matrix. Norm multiplicativity gives v(xy)=v(x)v(y).

F3F4
2.1

For v(x)1, let E=K(x) and m=[E:K]. The tower law and determinant of the scalar E-linear action give NL/K(x)=NE/K(x)[L:E]. The companion matrix of multiplication by x shows that its norm is (1)mf(0) for the monic minimal polynomial f. Thus f(0)1, so all coefficients lie in the valuation ring. It follows that f(1)1, and the same companion-matrix calculation for x+1 gives v(x+1)1.

F2F3F4step 1.1
3.1

For y nonzero and v(x)v(y), apply the preceding step to x/y to obtain v(x+y)v(y). If y=0 there is nothing to prove; interchange x,y when needed. This proves the strong triangle inequality. The uniqueness lemma gives uniqueness and completeness. Its proof applies in arbitrary characteristic; no conjugate count or separability was used. For the trivial base value the norm formula is identically one on nonzero elements.

F1step 1.1step 2.1

Depends on

Used by

Dependency tree · two levels

15 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