LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 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.

Bounded primitive integral element for Hermite-Minkowski

Statement

Assume the Axiom of Choice (The Axiom of Choice). Fix an integer $n \geq 2$ and a real number $B \geq 1$ . Let $K$ be a number field of degree $n = [K : Q]$ whose discriminant satisfies $∣ d_{K} ∣ \leq B$ . Then there is an integral element $α \in O_{K}$ with $K = Q (α)$ such that every conjugate of $α$ has modulus at most $\sqrt{B + 2}$ .

Facts & Assumptions

Given: The Axiom of Choice, an integer $n \geq 2$ , a real number $B \geq 1$ , and a number field $K$ of degree $n$ with $∣ d_{K} ∣ \leq B$ . Write $(r_{1}, r_{2})$ for the signature of $K$ , so $n = r_{1} + 2 r_{2}$ , and $D : = ∣ d_{K} ∣$ , so $1 \leq D \leq B$ .

[A1]

The Axiom of Choice implies the Axiom of Countable Choice (AC implies DC implies countable choice), which is the choice hypothesis of the volume fact [F5], invoked in steps 2.2 and 2.3; the strict Minkowski theorem [F2] is applied under the Axiom of Choice assumed in the statement, and no other selection is made in this proof.

[F1]

$σ (O_{K})$ is a full lattice in $R^{n}$ with $covol (σ (O_{K})) = 2^{- r_{2}} \sqrt{∣ d_{K} ∣}$ (Number-field integer rings and ideals are full lattices, Covolume of an integral ideal lattice, Full Euclidean lattice and covolume).

[F2]

Minkowski convex-body theorem, strict form: under the Axiom of Choice, a Lebesgue measurable convex centrally symmetric $C \subseteq R^{n}$ with $λ_{n} (C) > 2^{n} covol (Λ)$ contains a nonzero point of the full lattice $Λ$ (Minkowski convex-body theorem, strict form, Full Euclidean lattice and covolume).

[F3]

The unscaled Minkowski embedding is $σ (x) = (σ_{1} (x), \dots, σ_{r_{1}} (x), τ_{1} (x), \dots, τ_{r_{2}} (x))$ with each complex coordinate $τ_{j} (x)$ split into its real and imaginary parts, and it is injective (Unscaled Minkowski embedding).

[F4]

The embeddings of $K$ into $C$ over $Q$ are the $r_{1}$ real embeddings $σ_{i}$ , and the two members $τ_{j}, {\overset{ˉ}{τ}}_{j}$ of each complex conjugate pair. For every $0 \neq α \in O_{K}$ the norm is $N_{K / Q} (α) = \prod_{i = 1}^{r_{1}} σ_{i} (α) \prod_{j = 1}^{r_{2}} τ_{j} (α) {\overset{ˉ}{τ}}_{j} (α)$ , this product is nonzero because embeddings are injective field homomorphisms, and $N_{K / Q} (α) \in Z$ ; hence $∣ N_{K / Q} (α) ∣ \geq 1$ and $∣ N_{K / Q} (α) ∣ = \prod_{i} ∣ σ_{i} (α) ∣ \prod_{j} ∣ τ_{j} (α) ∣^{2}$ (Norm and trace from embeddings, with the inseparable exponent in the norm formula, Trace and norm of an algebraic integer).

[F5]

Euclidean volume is multiplicative over Borel product sets (On Borel subsets of R^{m+n}, the product lambda_m times lambda_n agrees with lambda_{m+n}, Tonelli's theorem for nonnegative measurable functions on a sigma-finite product), and the open disc of radius $ρ$ in $R^{2}$ has area $π ρ^{2}$ (Polar coordinates decompose Lebesgue measure into r^{n-1} dr d sigma).

[F6]

A product of convex sets is convex, and a product of sets each symmetric about the origin is centrally symmetric; bounded open intervals and open discs are convex and symmetric about the origin (A convex subset of $R^{m}$ contains every line segment between two of its points).

[F7]

For the finite tower $Q \subseteq Q (α) \subseteq K$ , restriction ${Hom}_{Q} (K, C) \to {Hom}_{Q} (Q (α), C)$ is surjective and every fibre has cardinality $[K : Q (α)]_{s}$ , the separable degree (Restriction partitions embeddings in a finite tower into extension fibres).

[F8]

Fields of characteristic zero are perfect and algebraic extensions of perfect fields are separable; hence $K / Q (α)$ is separable and $[K : Q (α)]_{s} = [K : Q (α)]$ (Fields of characteristic zero, finite fields, and algebraically closed fields are perfect, Every algebraic extension of a perfect field is separable).

[F9]

For $N = 1$ , the Gregory--Leibniz finite-remainder formula has partial sum $1 - 1 / 3 = 2 / 3$ and remainder $\int_{0}^{1} x^{4} / (1 + x^{2}) d x > 0$ . For example, the integrand is at least $1 / 32$ on $[1 / 2, 1]$ , so the remainder is at least $1 / 64$ . Thus $π / 4 > 2 / 3$ and $π > 8 / 3 > 2$ (The Gregory-Leibniz series: pi over four equals 1-1/3+1/5-1/7+...).

[F10]

A finite tower of field extensions satisfies $[K : Q] = [K : Q (α)] [Q (α) : Q]$ (Tower law for finite extensions: $[L : F] = [L : K] [K : F]$ ).

[F11]

A rational algebraic integer is an integer (The rational algebraic integers are exactly the integers).

Proof

1.1F3given

Exactly one of the cases $r_{1} \geq 1$ and $r_{1} = 0$ holds; in the second case $n = r_{1} + 2 r_{2} = 2 r_{2} \geq 2$ gives $r_{2} \geq 1$ . We treat the two cases in turn and produce the same conclusion in each.

1.2F3given

Case $r_{1} \geq 1$ . Let $X$ be the set of $(x_{1}, \dots, x_{r_{1}}, z_{1}, \dots, z_{r_{2}}) \in R^{r_{1}} \times C^{r_{2}}$ with $∣ x_{1} ∣ < \sqrt{D + 1}$ , $∣ x_{i} ∣ < 1$ for $2 \leq i \leq r_{1}$ , and $∣ z_{j} ∣ < 1$ for all $j$ ; in the real coordinates of [F3] this is $∣ x_{1} ∣ < \sqrt{D + 1}$ , $∣ x_{i} ∣ < 1$ , $(Re z_{j})^{2} + (Im z_{j})^{2} < 1$ .

1.3F3given

Case $r_{1} = 0$ . Here $n = 2 r_{2}$ with $r_{2} \geq 1$ . Let $Y$ be the set of $(z_{1}, \dots, z_{r_{2}}) \in C^{r_{2}}$ with $∣ Re z_{1} ∣ < 1$ , $∣ Im z_{1} ∣ < \sqrt{D + 1}$ , and $∣ z_{j} ∣ < 1$ for $j \geq 2$ ; written in real coordinates, $Y$ is the product of the rectangle $(- 1, 1) \times (- \sqrt{D + 1}, \sqrt{D + 1})$ in the first complex coordinate with $r_{2} - 1$ open unit discs.

2.1F6step 1.2

$X$ is a product of bounded open intervals and open discs, hence open and therefore Lebesgue measurable, and by [F6] it is convex and centrally symmetric.

2.2A1F5step 1.2

By [F5] and step 1.2, $λ_{n} (X) = (2 \sqrt{D + 1}) \cdot 2^{r_{1} - 1} \cdot π^{r_{2}} = 2^{r_{1}} π^{r_{2}} \sqrt{D + 1}$ .

2.3A1F5F6step 1.3

$Y$ is open and hence measurable, convex and centrally symmetric by [F6], and by [F5] it has $λ_{n} (Y) = (2 \cdot 2 \sqrt{D + 1}) \cdot π^{r_{2} - 1} = 4 π^{r_{2} - 1} \sqrt{D + 1}$ .

2.4step 1.3givenalgebra

Every $(z_{1}, \dots, z_{r_{2}}) \in Y$ has $∣ z_{1} ∣^{2} = (Re z_{1})^{2} + (Im z_{1})^{2} < 1 + (D + 1) = D + 2 \leq B + 2$ by the defining coordinate bounds and $D \leq B$ . Thus $∣ z_{1} ∣ < \sqrt{B + 2}$ .

3.1F1F9step 2.2algebra

By [F1] and step 2.2, $λ_{n} (X) / (2^{n} covol (σ (O_{K}))) = (π / 2)^{r_{2}} \sqrt{1 + 1 / D}$ . If $r_{2} = 0$ , the square-root factor is greater than $1$ ; if $r_{2} > 0$ , [F9] gives $π / 2 > 1$ and again the ratio is greater than $1$ . Thus $λ_{n} (X) > 2^{n} covol (σ (O_{K}))$ .

3.2F1F2F9step 2.3algebra

By [F1] and step 2.3, $λ_{n} (Y) / (2^{n} covol (σ (O_{K}))) = 2 (π / 2)^{r_{2} - 1} \sqrt{1 + 1 / D} > 1$ , since $r_{2} \geq 1$ , [F9] gives $π / 2 > 1$ , and $D \geq 1$ . Applying [F2] gives in this case an element $0 \neq α \in O_{K}$ with $σ (α) \in Y$ .

4.1F1F2step 2.1step 3.1

Applying [F2] with $Λ = σ (O_{K})$ and $C = X$ , whose hypotheses are verified in steps 2.1 and 3.1, gives in this case an element $0 \neq α \in O_{K}$ with $σ (α) \in X$ .

4.2F4step 3.2

In the totally complex case with $r_{2} \geq 2$ , every $j \geq 2$ has $0 < ∣ τ_{j} (α) ∣ < 1$ . There is at least one such factor, so $Q : = \prod_{j \geq 2} ∣ τ_{j} (α) ∣^{2} < 1$ . By [F4], $∣ N_{K / Q} (α) ∣ = ∣ τ_{1} (α) ∣^{2} Q \geq 1$ , hence $∣ τ_{1} (α) ∣ > 1$ .

4.3F4F10F11step 3.2step 2.4

If $r_{1} = 0$ and $r_{2} = 1$ , then $[K : Q] = 2$ . The element from step 3.2 is nonzero and satisfies $∣ Re τ_{1} (α) ∣ < 1$ . If $α \in Q$ , [F11] makes $α \in Z$ ; since an embedding fixes $Q$ , this would give $∣ α ∣ < 1$ and hence $α = 0$ , a contradiction. Therefore $α \notin Q$ , so $[Q (α) : Q] > 1$ . By the tower law [F10] this degree divides $[K : Q] = 2$ , and thus $K = Q (α)$ . Its two complex embeddings give the two conjugates, which are distinct because $α$ generates $K$ ; both have modulus less than $\sqrt{B + 2}$ by step 2.4 and conjugation.

5.1F4step 4.1

For this $α$ in the real-embedding case and every $i \geq 2$ one has $∣ σ_{i} (α) ∣ < 1$ , and for every $j$ one has $∣ τ_{j} (α) ∣ < 1$ . There are $r_{1} - 1 + 2 r_{2} = n - 1 \geq 1$ factors in $P : = \prod_{i \geq 2} ∣ σ_{i} (α) ∣ \prod_{j} ∣ τ_{j} (α) ∣^{2}$ , each positive and less than $1$ , so $P < 1$ and $∣ N_{K / Q} (α) ∣ = ∣ σ_{1} (α) ∣ P$ . Since the norm has absolute value at least $1$ by [F4], necessarily $∣ σ_{1} (α) ∣ > 1$ .

5.2F7F8step 1.3step 4.2

If $r_{1} = 0$ and $r_{2} \geq 2$ , every embedding other than $τ_{1}$ and ${\overset{ˉ}{τ}}_{1}$ sends $α$ to a value of modulus $< 1$ . The values $τ_{1} (α)$ and ${\overset{ˉ}{τ}}_{1} (α)$ have modulus $> 1$ by step 4.2 and are distinct: equality would make $τ_{1} (α)$ real, contrary to $∣ Re τ_{1} (α) ∣ < 1$ . Thus the fibre of [F7] over $τ_{1} ∣_{Q (α)}$ is the singleton ${τ_{1}}$ , so $[K : Q (α)]_{s} = 1$ , and [F8] gives $[K : Q (α)] = 1$ , that is, $K = Q (α)$ .

6.1F4step 1.2step 5.1

So in this case every embedding $φ$ of $K$ other than $σ_{1}$ sends $α$ to a complex number of modulus $< 1$ , while $∣ σ_{1} (α) ∣ > 1$ ; in particular $φ (α) = σ_{1} (α)$ holds only for $φ = σ_{1}$ . Also $∣ σ_{1} (α) ∣ < \sqrt{D + 1} \leq \sqrt{B + 2}$ by step 1.2, and $D + 1 \leq B + 2$ since $D \leq B$ .

7.1F7F8step 6.1

The fibre of the restriction map [F7] over $σ_{1} ∣_{Q (α)}$ is the set ${φ : φ (α) = σ_{1} (α)}$ , and the fibre is nonempty because it contains $σ_{1}$ ; by step 6.1 it is the singleton ${σ_{1}}$ . Hence $[K : Q (α)]_{s} = 1$ by [F7], and [F8] upgrades this to $[K : Q (α)] = 1$ , that is, $K = Q (α)$ .

8.1step 5.1step 2.4step 6.1step 5.2step 4.3step 7.1∎

Steps 7.1, 5.2, and 4.3 cover respectively the real-embedding case, the totally complex case with $r_{2} \geq 2$ , and the totally complex quadratic case; each gives $K = Q (α)$ for the constructed integral $α$ . In the real-embedding case step 6.1 bounds the distinguished real conjugate and all others have modulus $< 1$ . In the totally complex cases step 2.4 bounds $τ_{1} (α)$ and its conjugate, while all other conjugates have modulus $< 1$ by the chosen window. Since $B \geq 1$ , these bounds are all at most $\sqrt{B + 2}$ .

Remarks

The two windows are the ones used by Milne: the real case enlarges the first real coordinate, and the totally complex case enlarges the imaginary part of the first complex coordinate while keeping its real part in $(- 1, 1)$ . For $r_{2} \geq 2$ , the norm makes the first conjugate pair the unique values outside the unit circle, and the asymmetry separates the pair. For $r_{2} = 1$ , the strict real-coordinate bound rules out a rational integral element, and degree two then makes the nonzero element primitive. The uniform bound $\sqrt{B + 2}$ absorbs both coordinate bounds. This lemma is the analytic input to the Hermite-Minkowski finiteness theorem proved later on this page; the finiteness of the possible minimal polynomials there is a separate, purely algebraic step.

Depends on

Used by

Hermite-Minkowski finiteness Theorem

Dependency tree · two levels

98 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)
Brian Conrad and Aaron Landesman, Math 154 Algebraic Number Theory (standard reference, not scraped)