ExampleConstruction: AI-adaptedVerification: 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.

Higher-degree class group by norm exclusions

Example

Assume the Axiom of Choice. Let $α$ be a root of $f = X^{5} - X - 1$ and $K = Q (α)$ . Then $O_{K} = Z [α]$ , $d_{K} = 2869 = 19 \cdot 151$ , the Minkowski constant satisfies $M_{K} < 4$ , and $Cl (O_{K})$ is trivial, because no nonzero integral ideal of $O_{K}$ has norm $2$ or $3$ and every class has a representative of norm $< 4$ .

Facts & Assumptions

Given: The Axiom of Choice, the polynomial $f = X^{5} - X - 1 \in Z [X]$ , and a root $α$ of $f$ with $K = Q (α)$ .

[F1]

Reduction modulo a prime: if $f \in Z [x]$ is primitive of positive degree, $p$ does not divide its leading coefficient, and the reduction $\overset{ˉ}{f} \in F_{p} [x]$ is irreducible, then $f$ is irreducible in $Q [x]$ (Irreducibility after reduction modulo a prime implies irreducibility over $Q$ when the leading coefficient survives).

[F2]

Discriminant and resultant: for monic $f$ of degree $n$ , $Res (f, f^{'}) = (- 1)^{n (n - 1) / 2} Disc (f)$ (For monic $f$ of degree $n$ , $Res (f, f^{'}) = (- 1)^{n (n - 1) / 2} Disc (f)$ ), and in an algebra in which $f$ splits with roots $r_{1}, \dots, r_{n}$ one has $Res (f, f^{'}) = \prod_{i} f^{'} (r_{i})$ and $Disc (f) = \prod_{i < j} (r_{i} - r_{j})^{2}$ (The monic resultant $Res (f, g)$ from the symmetric coefficient expression of $\prod_{i} g (x_{i})$ , The discriminant of a monic polynomial as the coefficient expression of $Δ_{n}^{2}$ ).

[F3]

Vieta: if $f = t^{n} + a_{1} t^{n - 1} + \dots + a_{n}$ splits in a commutative algebra as $f (t) = \prod_{i = 1}^{n} (t - α_{i})$ , then $a_{k} = (- 1)^{k} e_{k} (α_{1}, \dots, α_{n})$ (Vieta's formulas identify the coefficients of a split monic polynomial with elementary symmetric functions of its roots).

[F4]

Power-basis discriminant: if $f$ is the degree- $n$ monic minimal polynomial of $α$ , then $disc (1, α, \dots, α^{n - 1}) = Disc (f)$ (Power-basis and polynomial discriminants).

[F5]

If integral $α$ generates $K$ and its power-basis discriminant is squarefree, then $O_{K} = Z [α]$ (Squarefree power discriminant criterion).

[F6]

$α \in O_{K}$ exactly when its monic minimal polynomial over $Q$ lies in $Z [X]$ (Minimal-polynomial criterion for algebraic integers).

[F7]

For a nonzero integral ideal $a$ of norm $N a = p$ with $p$ a rational prime: $N a = ∣ O_{K} / a ∣$ , and for a nonzero prime $P$ one has $N P = p^{f} \geq 2$ (The absolute norm of an integral ideal, The norm of a prime ideal).

[F8]

Minkowski bound: every class of $Cl (O_{K})$ contains an integral ideal $b$ with $N b \leq M_{K}$ (Minkowski bound for ideal classes, The ideal class group).

[F9]

Gregory-Leibniz: the partial sum of $\sum_{k} (- 1)^{k} / (2 k + 1)$ through $N = 7$ is $33976 / 45045 > 3 / 4$ with positive remainder, giving $π > 3$ (The Gregory-Leibniz series: pi over four equals 1-1/3+1/5-1/7+...).

Proof

1.1algebra

Reduction modulo 3: $\overset{ˉ}{f} = X^{5} + 2 X + 2$ has values $2, 2, 2$ at $0, 1, 2$ , so it has no linear factor; division by the three monic irreducible quadratics leaves remainders $2$ for $X^{2} + 1$ (where $X^{2} \equiv - 1$ ), $X + 2$ for $X^{2} + X + 2$ (where $X^{2} \equiv - X - 2$ ), and $X + 2$ for $X^{2} + 2 X + 2$ (where $X^{2} \equiv - 2 X - 2$ ); hence $\overset{ˉ}{f}$ has no factor of degree at most $2$ , and a degree- $5$ reducible polynomial would have one, so $\overset{ˉ}{f}$ is irreducible over $F_{3}$ .

1.2F2F3algebra

Discriminant: in $C$ write $f = \prod_{i = 1}^{5} (t - r_{i})$ ; by [F2] and [F3], $Disc (f) = Res (f, f^{'}) = \prod_{i} (5 r_{i}^{4} - 1)$ and $\prod_{i} r_{i} = - a_{5} = 1$ . Since $f (r_{i}) = 0$ and $r_{i} \neq 0$ (as $f (0) = - 1$ ), we have $r_{i}^{4} = (r_{i} + 1) / r_{i}$ and $5 r_{i}^{4} - 1 = (4 r_{i} + 5) / r_{i}$ ; moreover $\prod_{i} (4 r_{i} + 5) = 4^{5} \prod_{i} (r_{i} + 5 / 4) = - 4^{5} f (- 5 / 4) = - 1024 (- \frac{3125}{1024} + \frac{5}{4} - 1) = 2869$ . Hence $Disc (f) = 2869$ .

2.1F1F6step 1.1

By [F1] with $p = 3$ the polynomial $f$ is irreducible over $Q$ , so it is the minimal polynomial of $α$ , $K = Q (α)$ has degree $5$ , and $α \in O_{K}$ by [F6].

2.2F7step 1.1algebra

No ideal of norm $2$ or $3$ : if $N a = p \in {2, 3}$ , then $O_{K} / a$ is a commutative ring with $p$ elements, hence isomorphic to $F_{p}$ ; the composite $Z [X] \to O_{K} \to F_{p}$ with $X \mapsto \overset{ˉ}{α}$ kills $f$ , so $f$ has a root mod $p$ by [F7]; but $f m o d 3$ has values $2, 2, 2$ and $f m o d 2$ has values $1, 1$ at all elements of their prime fields, a contradiction.

3.1F4F5step 2.1step 1.2algebra

The factorisation $2869 = 19 \cdot 151$ consists of distinct primes, so $Disc (f)$ is squarefree; by [F2] and [F4] the power-basis discriminant of $α$ is $2869$ , so [F5] gives $O_{K} = Z [α]$ and $d_{K} = 2869$ .

3.2step 2.1algebra

Signature: $f^{'} = 5 X^{4} - 1$ vanishes exactly at $\pm c$ with $c = 5^{- 1 / 4}$ ; since $c^{4} = 1 / 5$ , $f (- c) = - c^{5} + c - 1 = \frac{4}{5} c - 1 < 0$ and $f (c) = c^{5} - c - 1 = - \frac{4}{5} c - 1 < 0$ , using $0 < c < 1$ . The derivative is positive on $(- \infty, - c)$ , negative on $(- c, c)$ , and positive on $(c, \infty)$ , so the local maximum and local minimum are both negative. Since $f (x) \to - \infty$ as $x \to - \infty$ and $f (x) \to + \infty$ as $x \to + \infty$ , there is exactly one real root and two conjugate pairs of nonreal roots, that is $(r_{1}, r_{2}) = (1, 2)$ .

4.1F9step 3.1step 3.2algebra

Minkowski constant: $M_{K} = (4 / π)^{2} \frac{5!}{5^{5}} \sqrt{2869} = \frac{120}{3125} (\frac{4}{π})^{2} \sqrt{2869} < \frac{120}{3125} \cdot \frac{16}{9} \cdot 54 = \frac{11520}{3125} < 4$ , using $π > 3$ of [F9] and $\sqrt{2869} < 54$ .

5.1F8step 3.1step 4.1step 2.2

Every class of $Cl (O_{K})$ has an integral representative $b$ with $N b \leq M_{K} < 4$ by [F8] and step 4.1; the norm is a positive integer, so $N b \in {1, 2, 3}$ , and step 2.2 rules out $2$ and $3$ , leaving $N b = 1$ , i.e. $b = O_{K}$ ; hence every class is principal and $Cl (O_{K})$ is trivial.

6.1step 3.1step 4.1step 5.1∎

Therefore $O_{K} = Z [α]$ , $d_{K} = 2869 = 19 \cdot 151$ , $M_{K} < 4$ , and $Cl (O_{K})$ is trivial.

Remarks

The example illustrates the standard norm-exclusion computation in degree $5$ : irreducibility modulo the small prime $3$ produces the field, the resultant computation of the discriminant certifies the ring of integers because $2869 = 19 \cdot 151$ is squarefree, and the small primes $2$ and $3$ are eliminated by checking that $f$ has no root modulo them. A root modulo $p$ is exactly what a nonzero ideal of norm $p$ would produce.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

65 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)