ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

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.

The full $S_{3}$ correspondence for the splitting field of $x^{3} - 2$

Example

Let $a$ be the real cube root of $2$ , let $ω^{2} + ω + 1 = 0$ with $ω \neq 1$ , and put $L = Q (a, ω)$ . Define

$r (a) = ω a, r (ω) = ω, s (a) = a, s (ω) = ω^{2} .$

Then $Gal (L / Q) = ⟨ r, s : r^{3} = s^{2} = 1, s r s = r^{- 1} ⟩ ≅ S_{3}$ . Its fixed-field table, with products of automorphisms read right to left, is

Subgroup	Fixed field
${1}$	$L$
$⟨ r ⟩ = A_{3}$	$Q (ω)$
$⟨ s ⟩$	$Q (a)$
$⟨ r s ⟩$	$Q (ω^{2} a)$
$⟨ r^{2} s ⟩$	$Q (ω a)$
$S_{3}$	$Q$

The three order-two subgroups correspond to three cubic fields that are not normal over $Q$ . Among the strict intermediate fields, $Q (ω)$ is the single normal one.

Facts & Assumptions

Given: Eisenstein's irreducibility criterion at $2$ (Eisenstein criterion over the integers) and the degree formulas in The fundamental theorem of finite Galois theory.

[L1]

An intermediate field $E / F$ is Galois exactly when its corresponding subgroup is normal (Normal subgroups, conjugate fields, and quotient groups in the Galois correspondence).

[L2]

For a finite extension $L / E$ with $G = Aut (L / E)$ , being Galois, being the splitting field of a separable polynomial, $∣ G ∣ = [L : E]$ , and $L^{G} = E$ are equivalent (Equivalent characterizations of a finite Galois extension).

[L3]

For $b$ algebraic over a field $F$ there is a unique monic irreducible $m_{b} \in F [x]$ generating the kernel of evaluation at $b$ , and $f (b) = 0$ exactly when $m_{b} ∣ f$ (The evaluation kernel and the unique monic irreducible minimal polynomial of an algebraic element).

[L4]

If $b$ is algebraic over $F$ with minimal polynomial of degree $n$ , then $1, b, \dots, b^{n - 1}$ is an $F$ -basis of $F (b)$ and $[F (b) : F] = n$ (A simple algebraic extension is its minimal-polynomial quotient and has power basis $1, a, \dots, a^{n - 1}$ and degree $n$ ).

[L5]

For fields $F \subseteq K \subseteq L$ with $K / F$ and $L / K$ finite, $L / F$ is finite and $[L : F] = [L : K] [K : F]$ (Tower law for finite extensions: $[L : F] = [L : K] [K : F]$ ).

Verification

technique · direct

1.1givenL3L4L5algebra

Eisenstein at $2$ makes $x^{3} - 2$ irreducible over $Q$ , so by [L3] it is the minimal polynomial of $a$ and by [L4] $[Q (a) : Q] = 3$ . Since $a$ is real, $Q (a) \subseteq R$ , whereas the two roots $ω, ω^{2}$ of $x^{2} + x + 1$ are nonreal; that quadratic therefore has no root in $Q (a)$ , is irreducible over $Q (a)$ , and by [L3] and [L4] gives $[L : Q (a)] = 2$ . By [L5], $[L : Q] = [L : Q (a)] [Q (a) : Q] = 6$ . The three cube roots of $2$ are $a, ω a, ω^{2} a$ , all in $L$ , and they generate $L$ over $Q$ because $ω = (ω a) a^{- 1}$ ; hence $L$ is the splitting field of $x^{3} - 2$ over $Q$ .

2.1step 1.1L2construct

The displayed maps permute the three roots and preserve the defining relations, so they are automorphisms. Direct calculation gives $r^{3} = s^{2} = 1$ and $s r s = r^{- 1}$ , and the six maps $1, r, r^{2}, s, r s, r^{2} s$ are distinct. The three roots $a, ω a, ω^{2} a$ of $x^{3} - 2$ are distinct, so that polynomial is separable and step 1.1 makes $L$ its splitting field; by [L2], $L / Q$ is finite Galois with $∣ Gal (L / Q) ∣ = [L : Q] = 6$ . The six maps therefore exhaust the automorphism group.

3.1step 2.1givenL3L4algebra

Each listed generator fixes its displayed field: $r$ fixes $Q (ω)$ , $s$ fixes $Q (a)$ , while $r s$ sends $a$ to $ω a$ and $ω$ to $ω^{2}$ , so it fixes $ω^{2} a$ , and $r^{2} s$ sends $a$ to $ω^{2} a$ and $ω$ to $ω^{2}$ , so it fixes $ω a$ . Each of $a, ω a, ω^{2} a$ is a root of the irreducible $x^{3} - 2$ and $ω$ is a root of the irreducible $x^{2} + x + 1$ , so by [L3] and [L4] the four fields have degrees $3, 3, 3$ and $2$ over $Q$ , matching the indices of the corresponding subgroups. Each displayed field therefore sits inside the fixed field of its subgroup with the same finite degree over $Q$ , so the two coincide, and the fundamental theorem's bijection makes the table complete.

4.1step 3.1L1∎

The subgroup $A_{3}$ is normal in $S_{3}$ , while none of the three order-two subgroups is normal. By [L1], $Q (ω) / Q$ is Galois and the three cubic fields are not; the base and splitting fields give the two normal endpoints.

Depends on

Used by

x³-2 has discriminant -108 and Galois group S₃ over ℚ Example
FALSE: every subgroup in the Galois correspondence gives a normal subextension False statement

Dependency tree · two levels

38 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

K. Conrad, The Galois Correspondence, Examples 4.6 and 5.8 (standard reference, not scraped)
J. S. Milne, Fields and Galois Theory, v5.10, Chapter 3 (standard reference, not scraped)

The full S3S3​ correspondence for the splitting field of x3−2x3−2