LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-10-02

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.

Unit logarithms lie in the trace-zero hyperplane

Statement

Assume the Axiom of Choice. Let $H = {(x_{i}) \in R^{r_{1} + r_{2}} : \sum_{i} x_{i} = 0}$ . Then $λ (O_{K}^{\times}) \subseteq H$ ; that is, the coordinate sum of $λ (u)$ is $\log ∣ N_{K / Q} (u) ∣$ , which vanishes for every unit.

Facts & Assumptions

Given: The Axiom of Choice, a number field $K$ of signature $(r_{1}, r_{2})$ with its logarithmic embedding $λ$ (Logarithmic embedding of a number field), and a unit $u \in O_{K}^{\times}$ .

[F1]

The logarithmic embedding is $λ (x) = (\log ∣ σ_{1} x ∣, \dots, \log ∣ σ_{r_{1}} x ∣, 2 \log ∣ τ_{1} x ∣, \dots, 2 \log ∣ τ_{r_{2}} x ∣)$ on $K^{\times}$ , where $σ_{1}, \dots, σ_{r_{1}}$ are the real embeddings and $τ_{1}, \dots, τ_{r_{2}}$ one embedding from each complex conjugate pair (Logarithmic embedding of a number field, Archimedean embeddings and signature).

[F2]

For $x \in K^{\times}$ the product formula reads $\prod_{v} ∣ x ∣_{v} = 1$ , where the finite absolute values are $∣ x ∣_{p} = N p^{- v_{p} (x)}$ with $v_{p} (x) = v_{p} ((x))$ the valuation of the principal fractional ideal, and the archimedean ones are $∣ x ∣_{σ} = ∣ σ (x) ∣$ and $∣ x ∣_{τ} = ∣ τ (x) ∣^{2}$ (Product formula for a number field, Prime-ideal valuations on fractional ideals, Fractional ideals).

[F3]

For $u \in O_{K}$ the element $u$ is a unit if and only if $N_{K / Q} (u) = \pm 1$ (A number-field unit is exactly an algebraic integer of norm plus or minus one).

[F4]

The modulus of a complex number is nonnegative and vanishes only at $0$ , and satisfies $∣ z w ∣ = ∣ z ∣ ∣ w ∣$ (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

[F5]

For $x, y > 0$ the natural logarithm satisfies $\log (x y) = \log x + \log y$ and $\log 1 = 0$ (Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm, The natural logarithm as the inverse of the exponential function).

[F6]

For a finite separable extension such as $K / Q$ the norm is the product of the images under the $[K : Q]$ embeddings $K \to C$ (Norm and trace from embeddings, with the inseparable exponent in the norm formula).

[A1]

The Axiom of Choice is assumed; its only use in this argument is the AC-qualified product formula [F2] (The Axiom of Choice).

Proof

Proof technique: a unit has valuation zero at every finite prime, so the product formula collapses to its archimedean part; taking logarithms turns that product into the coordinate sum of $λ (u)$ .

1.1F2given

The principal fractional ideal of the unit $u$ is $(u) = O_{K}$ , so $v_{p} (u) = v_{p} ((u)) = 0$ for every nonzero prime $p$ , and the normalized finite absolute value $∣ u ∣_{p} = N p^{- v_{p} (u)}$ equals $1$ at every finite place.

1.2F4given

Every modulus $∣ σ_{i} u ∣$ and $∣ τ_{j} u ∣$ is strictly positive: the embeddings are injective field homomorphisms, $u \neq 0$ , and a nonzero complex number has positive modulus.

1.3F3given

Since $u$ is a unit, $N_{K / Q} (u) = \pm 1$ and therefore $∣ N_{K / Q} (u) ∣ = 1$ .

2.1F2step 1.1

For $x = u$ the product formula gives $\prod_{v} ∣ u ∣_{v} = 1$ ; by step 1.1 every finite factor equals $1$ , so the archimedean factors satisfy $(\prod_{i = 1}^{r_{1}} ∣ σ_{i} u ∣) (\prod_{j = 1}^{r_{2}} ∣ τ_{j} u ∣^{2}) = 1$ .

3.1F1F5step 2.1step 1.2

Applying the logarithm to the identity of step 2.1 yields $\sum_{i = 1}^{r_{1}} \log ∣ σ_{i} u ∣ + \sum_{j = 1}^{r_{2}} \log ∣ τ_{j} u ∣^{2} = \log 1 = 0$ ; since $\log (a^{2}) = 2 \log a$ for $a > 0$ by step 1.2, the left-hand side equals $\sum_{k} λ (u)_{k}$ , the coordinate sum of $λ (u)$ ; hence this coordinate sum is $0$ and $λ (u) \in H$ .

4.1F5F6step 1.3step 3.1

The same coordinate sum equals $\log ∣ N_{K / Q} (u) ∣$ : the embedding formula [F6] gives $∣ N_{K / Q} (u) ∣ = (\prod_{i} ∣ σ_{i} u ∣) (\prod_{j} ∣ τ_{j} u ∣^{2})$ , whose logarithm is the sum of step 3.1, and by step 1.3 this is $\log 1 = 0$ .

5.1A1step 3.1step 4.1∎

As $u \in O_{K}^{\times}$ was arbitrary, $λ (O_{K}^{\times}) \subseteq H$ ; the only Choice used is [A1] through the AC-qualified product formula, the remaining computations being evaluations of norms, moduli and logarithms.

Depends on

Used by

Regulator of a number field Definition
A unimodular change of generators preserves the regulator determinants Example
Two independent units in a real cubic field Example
The logarithmic unit image is discrete Lemma
The logarithmic unit image is a full lattice Theorem
The regulator is well defined Theorem

Dependency tree · two levels

56 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 v3.08 (standard reference, not scraped)
Andrew V. Sutherland, MIT 18.785 Lecture 15: Dirichlet's Unit Theorem (Fall 2021) (standard reference, not scraped)