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

Prime decomposition in Q(zeta_12)

Example

For $K = Q (ζ_{12})$ the discriminant is $d_{K} = 144 = 2^{4} \cdot 3^{2}$ . The primes $2$ and $3$ each have a unique prime of $O_{K}$ above them, with $e = f = 2$ ; and a rational prime $ℓ ∤ 12$ splits into four primes of residue degree $1$ when $ℓ \equiv 1 (m o d 12)$ , and into two primes of residue degree $2$ when $ℓ \equiv 5, 7, 11 (m o d 12)$ .

Facts & Assumptions

Given: A primitive twelfth root of unity $ζ_{12}$ and $K = Q (ζ_{12})$ , a reduced index since $4 ∣ 12$ (The cyclotomic extension $K (μ_{n})$ as a splitting field of $t^{n} - 1$ ).

[F1]

Discriminant formula: for a reduced index $f > 1$ with $K = Q (ζ_{f})$ , $d_{K} = (- 1)^{φ (f) / 2} \frac{f^{φ (f)}}{\prod_{p ∣ f} p^{φ (f) / (p - 1)}}$ (Signed discriminant of a cyclotomic field).

[F2]

Prime factorisation: for the reduced index $f = 12$ , a rational prime $ℓ$ , and $f = ℓ^{a} m$ with $\gcd (ℓ, m) = 1$ , one has $ℓ O_{K} = (P_{1} \dots P_{g})^{e}$ with $e = φ (ℓ^{a})$ , $d = {ord}_{m} (ℓ)$ , $g = φ (m) / d$ , and the $P_{i}$ pairwise distinct primes of residue degree $d$ (Prime factorisation in a cyclotomic field).

[F3]

For $ℓ ∤ 12$ every prime above $ℓ$ has residue degree ${ord}_{12} (ℓ)$ and their number is $φ (12) / {ord}_{12} (ℓ)$ (Decomposition of an unramified prime in a cyclotomic field).

[F4]

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

[F5]

$φ (12) = 4$ , and the unit group is $(Z / 12)^{\times} = {1, 5, 7, 11}$ , in which every element has order $1$ or $2$ : $1$ has order $1$ , while $5^{2} \equiv 7^{2} \equiv 11^{2} \equiv 1 (m o d 12)$ with $5, 7, 11 \equiv̸ 1 (m o d 12)$ (The unit group $(Z / n)^{\times}$ and Euler's totient $φ (n) = ∣ (Z / n)^{\times} ∣$ for $n \geq 1$ , The order $∣ G ∣$ of a finite group and the order $ord (g)$ of an element, with $ord (g) = \infty$ when no positive power of $g$ is the identity).

Verification

technique · direct

1.1F1F5

The data $φ (12) = 4$ , $12^{4} = 20736$ and $2^{4} \cdot 3^{2} = 16 \cdot 9 = 144$ give $d_{K} = (- 1)^{2} \cdot 20736 / 144 = 144 = 2^{4} \cdot 3^{2}$ .

1.2F2

For $ℓ = 2$ write $12 = 2^{2} \cdot 3$ , so $a = 2$ , $m = 3$ : $e = φ (4) = 2$ , $d = {ord}_{3} (2) = 2$ (as $2^{2} \equiv 1$ and $2 \equiv̸ 1 (m o d 3)$ ) and $g = φ (3) / 2 = 1$ ; hence $2 O_{K} = P^{2}$ for the unique prime above $2$ , of residue degree $2$ .

1.3F2

For $ℓ = 3$ write $12 = 3 \cdot 4$ , so $a = 1$ , $m = 4$ : $e = φ (3) = 2$ , $d = {ord}_{4} (3) = 2$ (as $3^{2} \equiv 1$ and $3 \equiv̸ 1 (m o d 4)$ ) and $g = φ (4) / 2 = 1$ ; hence $3 O_{K} = P^{' 2}$ for the unique prime above $3$ , of residue degree $2$ .

2.1F3F4F5step 1.1

For a prime $ℓ ∤ 12$ the class of $ℓ$ modulo $12$ is one of $1, 5, 7, 11$ . If $ℓ \equiv 1 (m o d 12)$ then ${ord}_{12} (ℓ) = 1$ , so by [F3] there are $φ (12) = 4$ primes of degree $1$ , and by [F4] $ℓ$ splits completely; if $ℓ \equiv 5, 7, 11 (m o d 12)$ then the order is $2$ by [F5], so there are $4 / 2 = 2$ primes, each of residue degree $2$ .

3.1step 1.1step 1.2step 1.3step 2.1∎

Collecting steps 1.1 through 2.1: $d_{K} = 144$ ; the primes $2$ and $3$ are ramified with a single prime each, of $e = f = 2$ ; and every $ℓ ∤ 12$ splits into four degree-one primes for the class $1$ , or two degree-two primes for the classes $5, 7, 11$ modulo $12$ .

Remarks

Degree check. In every unramified case $e f g = φ (12) = 4$ : four degree-one primes, or two degree-two primes, or (were the order $4$ ) one degree-four prime; the last case does not occur because $(Z / 12)^{\times}$ has exponent $2$ .
Ramified primes. $2$ and $3$ are exactly the prime divisors of the discriminant $d_{K} = 144$ , consistent with the ramification criterion for the reduced index $12$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

52 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 and Ch. 8 (standard reference, not scraped)
Conrad-Landesman, Math 154 Algebraic Number Theory, Chs. 10-11 (standard reference, not scraped)