ExampleConstruction: Literature-sourcedVerification: 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.

Arithmetic of Q(zeta_5)

Example

For $K = Q (ζ_{5})$ one has $O_{K} = Z [ζ_{5}]$ and $d_{K} = 5^{3} = 125$ . The prime $5$ is totally ramified: $(5) = (1 - ζ_{5})^{4}$ is a fourth power of the unique prime above $5$ , whose residue field is $F_{5}$ . The prime $2$ is unramified with a single prime above it of residue degree $4$ (residue field $F_{16}$ ) and trivial inertia group; and $11$ splits completely into four degree-one primes.

Facts & Assumptions

Given: A primitive fifth root of unity $ζ = ζ_{5}$ and $K = Q (ζ)$ , of degree $φ (5) = 4$ (The cyclotomic extension $K (μ_{n})$ as a splitting field of $t^{n} - 1$ ).

[F1]

$O_{K} = Z [ζ]$ , with integral basis $1, ζ, ζ^{2}, ζ^{3}$ (Ring of integers of every cyclotomic field).

[F2]

Discriminant: for the reduced index $f = 5$ , $d_{K} = (- 1)^{φ (5) / 2} 5^{φ (5)} / \prod_{p ∣ 5} p^{φ (5) / (p - 1)}$ (Signed discriminant of a cyclotomic field).

[F3]

Total ramification at a prime-power level: with $λ = 1 - ζ$ , $5 O_{K} = (λ)^{φ (5)} = (λ)^{4}$ , and $λ O_{K}$ is the unique prime of $O_{K}$ above $5$ , with residue field $F_{5}$ (Total ramification at a prime-power cyclotomic level).

[F4]

Unramified decomposition: for the reduced index $5$ and a prime $ℓ ∤ 5$ , every prime above $ℓ$ has residue degree ${ord}_{5} (ℓ)$ and there are $φ (5) / {ord}_{5} (ℓ) = 4 / {ord}_{5} (ℓ)$ of them (Decomposition of an unramified prime in a cyclotomic field).

[F5]

Complete splitting: for $ℓ ∤ 5$ , the prime $ℓ$ splits completely in $K$ if and only if $ℓ \equiv 1 (m o d 5)$ (Complete splitting criterion for a cyclotomic field).

[F6]

For finite Galois extensions the inertia group at a prime has order equal to the ramification exponent, $∣ I (P / p) ∣ = e (P / p)$ , and $P$ is unramified over $p$ if and only if its inertia group is trivial (Inertia group of a prime, Orders of decomposition and inertia groups).

Verification

technique · direct

1.1F2

Since $φ (5) = 4$ , the discriminant formula gives $d_{K} = (- 1)^{2} \cdot 5^{4} / 5^{4 / 4} = 5^{4} / 5 = 5^{3} = 125$ .

1.2F4

The multiplicative order of $2$ modulo $5$ is $4$ : the powers of $2$ modulo $5$ are $2, 4, 3, 1$ , so ${ord}_{5} (2) = 4$ .

1.3F5

The class $11 \equiv 1 (m o d 5)$ is the identity of $(Z / 5)^{\times}$ .

1.4F3F6

By [F3], $5 O_{K} = (λ)^{4}$ with $λ O_{K}$ the unique prime above $5$ and residue field $F_{5}$ ; its ramification exponent is $4 = [K : Q]$ , so $5$ is totally ramified and its inertia group at $λ$ has order $4$ , the full Galois group.

2.1F4F6step 1.2

By [F4] and step 1.2 applied with $ℓ = 2$ , there is exactly $4 / 4 = 1$ prime above $2$ , of residue degree $4$ ; its residue field has $2^{4} = 16$ elements, and since $2$ is unramified its inertia group is trivial by [F6], so $e = 1, f = 4, g = 1$ with $e f g = 4 = [K : Q]$ .

2.2F5step 1.3

By [F5] and step 1.3, $11$ splits completely in $K$ : there are $φ (5) = 4$ distinct primes above $11$ , each of ramification exponent $1$ and residue degree $1$ .

3.1F1step 1.1step 1.4step 2.1step 2.2∎

Collecting the results: $O_{K} = Z [ζ_{5}]$ with $1, ζ, ζ^{2}, ζ^{3}$ an integral basis, $d_{K} = 125$ , the prime $5$ is totally ramified with $(5) = (1 - ζ)^{4}$ , the prime $2$ has one prime above it of residue degree $4$ and trivial inertia, and $11$ splits into four degree-one primes.

Remarks

Unramified decomposition has three cases. For a prime $ℓ \neq 5$ , the orders modulo $5$ are $1, 2, 4$ for the classes $1, 4, {2, 3}$ , respectively. Thus [F4] gives four degree-one primes, two degree-two primes, or one degree-four prime. In particular $2$ is inert, while $19 \equiv 4 (m o d 5)$ gives two primes, each of residue degree $2$ .
Frobenius orders. The arithmetic Frobenius at $2$ has order $4$ and generates the full group $(Z / 5)^{\times}$ , while the Frobenius at $11$ is trivial, which is complete splitting in the sense of Complete splitting criterion for a cyclotomic field.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

60 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, Ch. 6, Proposition 6.2 and Remark 6.6(c) (standard reference, not scraped)
Conrad-Landesman, Math 154 Algebraic Number Theory, Chs. 10-12 (standard reference, not scraped)