TheoremStatement: 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.

The logarithmic unit image is a full lattice

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $K$ be a number field of signature $(r_{1}, r_{2})$ with logarithmic embedding $λ$ and hyperplane $H = {(x_{i}) : \sum_{i} x_{i} = 0}$ (Logarithmic embedding of a number field). The discrete subgroup $λ (O_{K}^{\times}) \subset H$ spans $H$ over $R$ ; hence it is a full lattice in $H$ of rank $r_{1} + r_{2} - 1$ .

Facts & Assumptions

Given: The Axiom of Choice, a number field $K$ of degree $n = r_{1} + 2 r_{2}$ and signature $(r_{1}, r_{2})$ , its logarithmic embedding $λ$ and hyperplane $H$ (Logarithmic embedding of a number field), the subspace $W : = {span}_{R} λ (O_{K}^{\times}) \subseteq H$ , and the fixed constant $A : = \sqrt{∣ d_{K} ∣} (2 / π)^{r_{2}}$ .

[F1]

$λ (x) = (\log ∣ σ_{1} x ∣, \dots, \log ∣ σ_{r_{1}} x ∣, 2 \log ∣ τ_{1} x ∣, \dots, 2 \log ∣ τ_{r_{2}} x ∣)$ for the real embeddings $σ_{1}, \dots, σ_{r_{1}}$ and one chosen embedding $τ_{1}, \dots, τ_{r_{2}}$ from each complex conjugate pair, and $H = {(x_{i}) \in R^{r_{1} + r_{2}} : \sum_{i} x_{i} = 0}$ is a hyperplane of dimension $r_{1} + r_{2} - 1$ (Logarithmic embedding of a number field, Archimedean embeddings and signature).

[F2]

$λ (u) \in H$ for every unit $u \in O_{K}^{\times}$ (Unit logarithms lie in the trace-zero hyperplane), so both $λ (O_{K}^{\times})$ and $W$ lie in $H$ .

[F3]

$λ (O_{K}^{\times})$ is discrete (The logarithmic unit image is discrete).

[F4]

For a subgroup $Γ$ of a finite-dimensional real vector space: if every bounded set meets $Γ$ in a finite set, then there are $R$ -linearly independent $v_{1}, \dots, v_{s} \in Γ$ with $Γ = Z v_{1} \oplus \dots \oplus Z v_{s}$ and ${span}_{R} Γ = R v_{1} \oplus \dots \oplus R v_{s}$ ; conversely such a subgroup is discrete (Discrete subgroups of a real vector space are lattices).

[F5]

Orthogonal complements are taken in the standard inner product on $R^{r_{1} + r_{2}}$ : $U^{⊥} = {v : ⟨ v, u ⟩ = 0$ for all $u \in U}$ , one has $W^{⊥ ⊥} = W$ for every subspace $W$ , and $U_{1} \subseteq U_{2}$ implies $U_{2}^{⊥} \subseteq U_{1}^{⊥}$ . Since $H = {x : ⟨ x, (1, \dots, 1) ⟩ = 0}$ , we have $H^{⊥} = R (1, \dots, 1)$ ; hence $z \notin H^{⊥}$ exactly when the coordinates of $z$ are not all equal (The orthogonal complement $W^{⊥} = {v : ⟨ v, w ⟩ = 0 for all w \in W}$ , In finite dimension, $W^{⊥ ⊥} = W$ and $\dim W + \dim W^{⊥} = \dim V$ ).

[F6]

The Minkowski embedding $σ : K \to R^{r_{1}} \times R^{2 r_{2}} = R^{n}$ is injective, sends $x$ to $(σ_{1} x, \dots, σ_{r_{1}} x, Re τ_{1} x, Im τ_{1} x, \dots, Re τ_{r_{2}} x, Im τ_{r_{2}} x)$ , is additive, and in the complex coordinate pairs $∣ τ_{j} x ∣^{2} = (Re τ_{j} x)^{2} + (Im τ_{j} x)^{2}$ (Unscaled Minkowski embedding).

[F7]

The image $σ (O_{K})$ is a full lattice in $R^{n}$ , and its covolume, for the Lebesgue volume on $R^{r_{1}} \times R^{2 r_{2}}$ induced by the identification $C ≅ R^{2}$ just fixed, is $covol (σ (O_{K})) = 2^{- r_{2}} \sqrt{∣ d_{K} ∣}$ , where $d_{K} = disc (O_{K})$ is the nonzero field discriminant (Number-field integer rings and ideals are full lattices, Covolume of an integral ideal lattice, Discriminant of a basis and order, Number-field discriminant is well-defined and nonzero).

[F8]

Equality case of the lattice point principle: if $Λ \subseteq R^{n}$ is a full lattice and $S \subseteq R^{n}$ is closed, bounded, convex and centrally symmetric with $Vol (S) \geq 2^{n} covol (Λ)$ , then $S \cap Λ$ contains a nonzero point (Minkowski convex-body theorem at equality).

[F9]

For every real $B \geq 1$ only finitely many nonzero integral ideals $a \subseteq O_{K}$ satisfy $N a \leq B$ (Finitely many ideals of bounded norm).

[F10]

For $0 \neq a \in O_{K}$ the principal ideal $(a) = a O_{K} = {c a : c \in O_{K}}$ satisfies $N ((a)) = ∣ N_{K / Q} (a) ∣$ ; if $(a) \subseteq (b)$ then $a = c b$ for some $c \in O_{K}$ , so $(a) = (b)$ gives $a = u b$ and $b = v a$ with $u, v \in O_{K}$ and $u v = 1$ , that is, $u \in O_{K}^{\times}$ (The norm of a principal integral ideal, The ideal generated by a subset and principal ideals).

[F11]

If $0 \neq a \in O_{K}$ then $N_{K / Q} (a) = \prod_{i = 1}^{r_{1}} σ_{i} (a) \cdot \prod_{j = 1}^{r_{2}} ∣ τ_{j} (a) ∣^{2}$ and $N_{K / Q} (a) \in Z$ ; consequently $N_{K / Q} (a) \neq 0$ and $∣ N_{K / Q} (a) ∣ \geq 1$ (Norm and trace from embeddings, with the inseparable exponent in the norm formula, Trace and norm of an algebraic integer, Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

[F12]

AC implies Countable Choice (AC implies DC implies countable choice). Under Countable Choice, each closed real interval $[- c, c]$ has Lebesgue measure $2 c$ (A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included). Each closed disc of radius $c > 0$ is a bounded Jordan-measurable region between continuous graphs (Riemann area between continuous graphs equals Jordan content) with Jordan content $π c^{2}$ (A closed disc of radius $r \geq 0$ has Jordan content $π r^{2}$ ), so its Lebesgue measure is $π c^{2}$ (Lebesgue outer measure is at most Jordan outer content, and a bounded Jordan measurable set is Lebesgue measurable with Lebesgue measure equal to its Jordan content). Each Euclidean Lebesgue measure $λ_{d}$ is sigma-finite, since the cubes $[- N, N]^{d}$ exhaust $R^{d}$ and have finite measure by the box formula. For Borel sets $E_{i} \subseteq R^{d_{i}}$ with $d_{i} \in {1, 2}$ , the measure of a finite Cartesian product is the product of the factor measures: iterate the rectangle formula for sigma-finite product measures and the agreement of product measure with Euclidean Lebesgue measure on Borel sets (For sigma-finite factors, the product measure exists, has the rectangle formula, is sigma-finite, and is unique, On Borel subsets of R^{m+n}, the product lambda_m times lambda_n agrees with lambda_{m+n}). Therefore the Euclidean volume of the product of these intervals and discs is the product of their Lebesgue measures.

[F13]

The natural logarithm is strictly increasing, maps $(0, \infty)$ onto $R$ , satisfies $\log (x y) = \log x + \log y$ and $\log 1 = 0$ , so $\log t \to \infty$ as $t \to \infty$ and $\log (s / t) = \log s - \log t$ for $s, t > 0$ (Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm).

[F14]

Since $d_{K} \neq 0$ by [F7], $∣ d_{K} ∣ > 0$ and its nonnegative square root is positive; also $π > 0$ . Thus the fixed constant $A : = \sqrt{∣ d_{K} ∣} (2 / π)^{r_{2}}$ is positive (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ , Pi as twice the smallest positive zero of cosine).

[A1]

The Axiom of Choice is assumed; it is used through the equality-case lattice point principle [F8], the discreteness input [F3] whose own AC use is inherited, and the Countable Choice measure interfaces in [F12]. AC supplies Countable Choice by [F12] (The Axiom of Choice).

Proof

technique · contraposition on a linear functional. If some $z$ is not orthogonal to $H$, products of intervals and discs of fixed volume produce, through the equality case of the lattice point principle, an algebraic integer of bounded norm; the finite list of principal ideals of bounded norm converts it to a unit $u$ with $f(u)$ bounded away from a tunable number $t_c$, and rescaled logarithms make $|t_c|$ exceed that bound, forcing $f(u)\ne0$

1.1F1F2F5

The image $λ (O_{K}^{\times})$ is a subgroup of $R^{r_{1} + r_{2}}$ contained in $H$ , so $W$ is a subspace of $H$ ; also $H^{⊥} = R (1, \dots, 1)$ .

1.2F1F2F4

If $r_{1} + r_{2} = 1$ then $H = {0}$ by [F1], so $λ (O_{K}^{\times}) = {0} = H$ by [F2], and the image is a full lattice of rank $0$ in $H$ ; hence assume $r_{1} + r_{2} \geq 2$ from now on.

1.3F5

Fix $z \in R^{r_{1} + r_{2}}$ with $z \notin H^{⊥}$ ; then the coordinates $z_{1}, \dots, z_{r_{1} + r_{2}}$ of $z$ are not all equal, by [F5].

1.4F1algebra

Define $f (x) : = ⟨ z, λ (x) ⟩ = \sum_{i = 1}^{r_{1}} z_{i} \log ∣ σ_{i} x ∣ + \sum_{j = 1}^{r_{2}} 2 z_{r_{1} + j} \log ∣ τ_{j} x ∣$ for $x \in K^{\times}$ , a group homomorphism $K^{\times} \to (R, +)$ ; since $λ (O_{K}^{\times})$ spans $W$ and $⟨ z, \cdot ⟩$ is linear, $f (u) = 0$ for every $u \in O_{K}^{\times}$ exactly when $z \in W^{⊥}$ , so it suffices to exhibit one unit $u$ with $f (u) \neq 0$ .

1.5F12F14algebra

Let $c_{1}, \dots, c_{r_{1} + r_{2}}$ be positive reals with $\prod_{i = 1}^{r_{1}} c_{i} \cdot \prod_{j = 1}^{r_{2}} c_{r_{1} + j}^{2} = A$ , and let $S_{c} \subseteq R^{n}$ be the set of points whose first $r_{1}$ coordinates $y_{i}$ satisfy $∣ y_{i} ∣ \leq c_{i}$ and whose $j$ -th complex pair $(u_{j}, v_{j})$ satisfies $u_{j}^{2} + v_{j}^{2} \leq c_{r_{1} + j}^{2}$ ; then $S_{c}$ is closed, bounded, convex and centrally symmetric. Positivity of $A$ is established in [F14]. By [F12], its volume is $\prod_{i = 1}^{r_{1}} (2 c_{i}) \cdot \prod_{j = 1}^{r_{2}} π c_{r_{1} + j}^{2} = 2^{r_{1}} π^{r_{2}} A = 2^{n} \cdot 2^{- r_{2}} \sqrt{∣ d_{K} ∣}$ .

1.6F14

The fixed positive constant $A$ depends only on $K$ , as recorded in [F14].

2.1F7F8step 1.5

By [F7] we have $covol (σ (O_{K})) = 2^{- r_{2}} \sqrt{∣ d_{K} ∣}$ , so $Vol (S_{c}) = 2^{n} covol (σ (O_{K}))$ ; applying [F8] to the full lattice $σ (O_{K})$ and the set $S_{c}$ produces a nonzero point $x \in S_{c} \cap σ (O_{K})$ .

3.1F6step 2.1

Write $x = σ (a)$ with $a \in O_{K}$ ; then $a \neq 0$ and the coordinates of $a$ satisfy $∣ σ_{i} (a) ∣ \leq c_{i}$ for $i \leq r_{1}$ and $(Re τ_{j} a)^{2} + (Im τ_{j} a)^{2} \leq c_{r_{1} + j}^{2}$ , that is $∣ τ_{j} (a) ∣^{2} \leq c_{r_{1} + j}^{2}$ .

4.1F11step 3.1

By [F11], $∣ N_{K / Q} (a) ∣ = \prod_{i = 1}^{r_{1}} ∣ σ_{i} (a) ∣ \cdot \prod_{j = 1}^{r_{2}} ∣ τ_{j} (a) ∣^{2} \leq \prod_{i = 1}^{r_{1}} c_{i} \cdot \prod_{j = 1}^{r_{2}} c_{r_{1} + j}^{2} = A$ ; since also $a \neq 0$ and $N_{K / Q} (a) \in Z ∖ {0}$ , we get $1 \leq ∣ N (a) ∣ \leq A$ , and in particular $A \geq 1$ .

5.1step 4.1algebra

If for some $i \leq r_{1}$ one had $∣ σ_{i} (a) ∣ < c_{i} / A$ , then the remaining factors of $∣ N (a) ∣$ being bounded by $A / c_{i}$ would give $∣ N (a) ∣ < (c_{i} / A) (A / c_{i}) = 1$ , contradicting $∣ N (a) ∣ \geq 1$ ; hence $∣ σ_{i} (a) ∣ \geq c_{i} / A$ . Likewise, if $∣ τ_{j} (a) ∣^{2} < c_{r_{1} + j}^{2} / A$ for some $j \leq r_{2}$ , then $∣ N (a) ∣ < (c_{r_{1} + j}^{2} / A) (A / c_{r_{1} + j}^{2}) = 1$ , again a contradiction, so $∣ τ_{j} (a) ∣^{2} \geq c_{r_{1} + j}^{2} / A$ .

5.2F9F10step 4.1

Let $B_{0} : = \max {1, A} \geq 1$ ; by [F9] only finitely many nonzero integral ideals of $O_{K}$ have norm at most $B_{0}$ , hence only finitely many have norm at most $A$ . The finite subcollection of principal ideals is nonempty because $(1)$ has norm $1 \leq A$ by [F10] and step 4.1. Choose generators $0 \neq b_{1}, \dots, b_{m} \in O_{K}$ for these principal ideals, so that $(b_{1}), \dots, (b_{m})$ are exactly the principal ideals of norm at most $A$ ; choosing these $m$ generators is a selection from finitely many nonempty sets. Since $N ((a)) = ∣ N (a) ∣ \leq A$ by [F10], $(a) = (b_{j})$ for some $j$ , and then $a = u b_{j}$ with $u \in O_{K}^{\times}$ .

6.1F13step 4.1step 5.2

Put $t_{c} : = \sum_{i = 1}^{r_{1}} z_{i} \log c_{i} + \sum_{j = 1}^{r_{2}} z_{r_{1} + j} \log (c_{r_{1} + j}^{2})$ ; the finite numbers $f (b_{j}) = ⟨ z, λ (b_{j}) ⟩$ being fixed, $B : = \max_{j} ∣ f (b_{j}) ∣ + \log A \cdot \sum_{i = 1}^{r_{1} + r_{2}} ∣ z_{i} ∣$ is a real number depending only on $z$ , on $K$ and on the chosen list, not on $c$ .

7.1F13step 5.1step 5.2step 6.1

For the unit $u$ of step 5.2 we have $∣ f (u) - t_{c} ∣ = ∣ f (a) - f (b_{j}) - t_{c} ∣ \leq ∣ f (b_{j}) ∣ + ∣ f (a) - t_{c} ∣$ , and expanding $f (a) - t_{c} = \sum_{i = 1}^{r_{1}} z_{i} \log (∣ σ_{i} (a) ∣ / c_{i}) + \sum_{j = 1}^{r_{2}} z_{r_{1} + j} \log (∣ τ_{j} (a) ∣^{2} / c_{r_{1} + j}^{2})$ shows, by step 5.1 and by $∣ σ_{i} (a) ∣ \leq c_{i}$ , $∣ τ_{j} (a) ∣^{2} \leq c_{r_{1} + j}^{2}$ , that each logarithm lies in $[- \log A, 0]$ ; hence $∣ f (a) - t_{c} ∣ \leq \log A \cdot \sum_{i} ∣ z_{i} ∣$ and $∣ f (u) - t_{c} ∣ \leq B$ .

7.2F13step 1.3step 6.1

Choose indices $p < q$ with $z_{p} \neq z_{q}$ , possible by step 1.3. Since $\log d \to \infty$ as $d \to \infty$ and $z_{p} - z_{q} \neq 0$ , the absolute value of $(z_{p} - z_{q}) \log d + z_{q} \log A$ tends to infinity; hence choose $d > 0$ with $∣ (z_{p} - z_{q}) \log d + z_{q} \log A ∣ > B$ .

8.1F13step 7.2

Set $d_{p} : = d$ , $d_{q} : = A / d$ and $d_{i} : = 1$ for the remaining indices $i$ ; then $\prod_{i = 1}^{r_{1} + r_{2}} d_{i} = A$ and $\sum_{i} z_{i} \log d_{i} = z_{p} \log d + z_{q} \log (A / d) = (z_{p} - z_{q}) \log d + z_{q} \log A$ , so this $d$ can be chosen with $∣ \sum_{i} z_{i} \log d_{i} ∣ > B$ .

9.1step 8.1algebra

Define the admissible tuple $c$ by $c_{i} : = d_{i}$ for $i \leq r_{1}$ and $c_{r_{1} + j} : = \sqrt{d_{r_{1} + j}}$ for $1 \leq j \leq r_{2}$ ; then $\prod_{i = 1}^{r_{1}} c_{i} \cdot \prod_{j = 1}^{r_{2}} c_{r_{1} + j}^{2} = \prod_{i} d_{i} = A$ and $t_{c} = \sum_{i} z_{i} \log d_{i}$ , so $∣ t_{c} ∣ > B$ .

10.1step 1.4step 1.5step 5.2step 7.1step 9.1

Applying the fixed-product construction and bounded-norm argument of steps 1.5 through 5.2 to the admissible tuple $c$ from step 9.1 yields a unit $u \in O_{K}^{\times}$ with $∣ f (u) - t_{c} ∣ \leq B$ ; since $∣ t_{c} ∣ > B$ , the triangle inequality gives $∣ f (u) ∣ \geq ∣ t_{c} ∣ - ∣ f (u) - t_{c} ∣ > 0$ , so $f (u) \neq 0$ and therefore $z \notin W^{⊥}$ by step 1.4.

11.1step 1.3step 10.1

As $z \notin H^{⊥}$ was arbitrary, every $z$ outside $H^{⊥}$ lies outside $W^{⊥}$ , which means $W^{⊥} \subseteq H^{⊥}$ .

12.1F5step 1.1step 11.1

Since $W \subseteq H$ we have $H^{⊥} \subseteq W^{⊥}$ , and with step 11.1 this gives $H^{⊥} = W^{⊥}$ ; taking orthogonal complements and using $W^{⊥ ⊥} = W$ and $H^{⊥ ⊥} = H$ yields $W = H$ , so $λ (O_{K}^{\times})$ spans $H$ over $R$ .

13.1F1F3F4step 12.1

By the discreteness of $λ (O_{K}^{\times})$ and [F4], there are $R$ -linearly independent $v_{1}, \dots, v_{s} \in λ (O_{K}^{\times})$ with $λ (O_{K}^{\times}) = Z v_{1} \oplus \dots \oplus Z v_{s}$ and ${span}_{R} λ (O_{K}^{\times}) = R v_{1} \oplus \dots \oplus R v_{s}$ ; this span is $H$ by step 12.1, so $s = \dim_{R} H = r_{1} + r_{2} - 1$ and $λ (O_{K}^{\times})$ is a full lattice in $H$ of rank $r_{1} + r_{2} - 1$ .

14.1A1F3F8F9F12step 1.2step 5.2step 7.2∎

Choice accounting: AC is invoked through [F8], the discreteness input [F3], and the Countable Choice measure interfaces in [F12]. The only other selections are the finitely many generators $b_{1}, \dots, b_{m}$ of step 5.2 and the single positive real $d$ of step 7.2; the rank-zero case of step 1.2 is choice-free.

Depends on

Used by

Dependency tree · two levels

145 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

William A. Stein, Algebraic Number Theory: A Computational Approach (standard reference, not scraped)
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)
Brian Conrad and Aaron Landesman, Math 154 Algebraic Number Theory (standard reference, not scraped)