CorollaryStatement: Literature-sourcedProof: Literature-sourcedPipeline-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.

Nontrivial number fields have discriminant of absolute value greater than one

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $K$ be a number field of degree $n = [K : Q] > 1$ . Then $∣ d_{K} ∣ > 1$ ; in particular $d_{K}$ is neither $1$ nor $- 1$ .

Facts & Assumptions

Given: The Axiom of Choice and a number field $K$ of degree $n > 1$ with signature $(r_{1}, r_{2})$ , so that $0 \leq r_{2} \leq n / 2$ .

[F1]

Minkowski bound: every class of $Cl (O_{K})$ contains an integral ideal $b$ with $N b \leq M_{K} = (4 / π)^{r_{2}} (n! / n^{n}) \sqrt{∣ d_{K} ∣}$ (Minkowski bound for ideal classes, The ideal class group).

[F2]

For a nonzero integral ideal $b$ the absolute norm $N b = ∣ O_{K} / b ∣$ is a finite positive integer, hence at least $1$ (The absolute norm of an integral ideal, A nonzero number-field ideal has finite quotient).

[F3]

Bernoulli's inequality: $(1 + x)^{n} \geq 1 + n x$ for $x \geq - 1$ and natural $n$ (Bernoulli's inequality $(1 + x)^{n} \geq 1 + n x$ ).

[F4]

Gregory-Leibniz: for every natural $N$ , $π / 4 = \sum_{k = 0}^{N} (- 1)^{k} / (2 k + 1) + R_{N}$ with $R_{N} = (- 1)^{N + 1} \int_{0}^{1} x^{2 N + 2} / (1 + x^{2}) d x$ (The Gregory-Leibniz series: pi over four equals 1-1/3+1/5-1/7+...).

Proof

1.1F1F2given

The principal class of $Cl (O_{K})$ exists, so by [F1] it contains an integral ideal $b$ with $N b \leq M_{K}$ ; by [F2] the norm $N b$ is a positive integer, so $N b \geq 1$ and therefore $1 \leq (4 / π)^{r_{2}} (n! / n^{n}) \sqrt{∣ d_{K} ∣}$ .

1.2F4algebra

Take $N = 1$ and $N = 2$ in [F4]: $π / 4 = 1 - 1 / 3 + R_{1}$ with $R_{1} = \int_{0}^{1} x^{4} / (1 + x^{2}) d x > 0$ gives $π > 8 / 3 > 2$ , and $π / 4 = 1 - 1 / 3 + 1 / 5 + R_{2}$ with $R_{2} = - \int_{0}^{1} x^{6} / (1 + x^{2}) d x < 0$ gives $π < 52 / 15 < 4$ . Hence $2 / π < 1$ and $4 / π > 1$ .

2.1step 1.2algebra

Put $U_{m} : = (4 / π)^{m / 2} m! / m^{m}$ for $m \geq 2$ . Then $U_{2} = (4 / π) \cdot 2 / 4 = 2 / π < 1$ by step 1.2.

2.2F3step 1.2algebra

For $m \geq 2$ , Bernoulli's inequality [F3] with $x = 1 / m$ gives $(1 + 1 / m)^{m} \geq 2$ , so $(m / (m + 1))^{m} \leq 1 / 2$ and $\frac{U_{m + 1}}{U_{m}} = \frac{2}{\sqrt{π}} {(\frac{m}{m + 1})}^{m} \leq \frac{1}{\sqrt{π}} < 1$ .

3.1step 2.1step 2.2algebra

Consequently $U_{m} \leq U_{2} (\sqrt{π})^{- (m - 2)} < 1$ for every $m \geq 2$ ; in particular $U_{n} < 1$ .

4.1step 3.1givenalgebra

Since $r_{2} \leq n / 2$ and $4 / π > 1$ by step 1.2, $(4 / π)^{r_{2}} \leq (4 / π)^{n / 2}$ , so $c : = (4 / π)^{r_{2}} n! / n^{n} \leq U_{n} < 1$ with $c > 0$ .

5.1step 1.1step 4.1algebra

Step 1.1 gives $1 \leq c \sqrt{∣ d_{K} ∣}$ with $0 < c < 1$ , so $\sqrt{∣ d_{K} ∣} \geq 1 / c > 1$ and hence $∣ d_{K} ∣ > 1$ .

6.1step 5.1given∎

Thus every number field of degree $n > 1$ has $∣ d_{K} ∣ > 1$ , so its discriminant is neither $1$ nor $- 1$ ; the degree-one case is excluded by the hypothesis.

Remarks

The estimate compares the Minkowski constant against the smallest possible norm of an integral ideal, namely $1$ . Two elementary inequalities drive it: the two-sided bound $2 < π < 4$ , extracted here from the Gregory-Leibniz series with two and three terms respectively (so that $2 / π < 1$ and $4 / π > 1$ ), and Bernoulli's inequality $(1 + 1 / m)^{m} \geq 2$ , which makes the auxiliary sequence $U_{m}$ strictly decreasing. The hypothesis $n > 1$ is essential: $d_{Q} = 1$ , so the conclusion fails for the degree-one field.

Depends on

Used by

Every nontrivial number field has a ramified finite prime Corollary
No nontrivial everywhere unramified number field over Q Example
Signature constant rules out discriminant ±1 Example

Dependency tree · two levels

45 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)
William A. Stein, Algebraic Number Theory: A Computational Approach (standard reference, not scraped)