ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck 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 complete Galois correspondence for $Q (\sqrt{2}, \sqrt{3}) / Q$

Example

$Q (\sqrt{2}, \sqrt{3}) / Q$ is Galois with group $V_{4}$ . Its correspondence is

Subgroup	Fixed field
${1}$	$Q (\sqrt{2}, \sqrt{3})$
$⟨ σ_{2} ⟩$	$Q (\sqrt{3})$
$⟨ σ_{3} ⟩$	$Q (\sqrt{2})$
$⟨ σ_{6} ⟩$	$Q (\sqrt{6})$
$V_{4}$	$Q$

Here $σ_{2}$ changes the sign of $\sqrt{2}$ , $σ_{3}$ changes the sign of $\sqrt{3}$ , and $σ_{6} = σ_{2} σ_{3}$ . The trivial subgroup fixes the whole biquadratic extension, while each order-two subgroup fixes a quadratic field.

Facts & Assumptions

Given: Positive square roots $\sqrt{2}, \sqrt{3}$ and the tower law (Tower law for finite extensions: $[L : F] = [L : K] [K : F]$ ).

[L1]

In the finite Galois correspondence, $[K : K^{H}] = ∣ H ∣$ and $[K^{H} : F] = [G : H]$ , and the subgroup and intermediate-field assignments are mutually inverse bijections (The fundamental theorem of finite Galois theory).

[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).

Verification

technique · direct

1.1

The field $Q (\sqrt{2})$ has degree two, and $\sqrt{3} \notin Q (\sqrt{2})$ : squaring an equation $\sqrt{3} = a + b \sqrt{2}$ forces $2 a b = 0$ , and either case contradicts rationality. Thus $1, \sqrt{2}, \sqrt{3}, \sqrt{6}$ is a basis and the extension has degree four. Independent sign changes of the two square roots give four automorphisms. The field is the splitting field over $Q$ of $(x^{2} - 2) (x^{2} - 3)$ , whose four roots $\pm \sqrt{2}, \pm \sqrt{3}$ are distinct, so [L2] makes the extension finite Galois with $∣ G ∣ = 4$ ; the four sign changes therefore exhaust $G$ , which has exponent two and is thus $V_{4}$ .

givenL2algebra

2.1

For $x = a + b \sqrt{2} + c \sqrt{3} + d \sqrt{6}$ , invariance under $σ_{2}$ , $σ_{3}$ , or $σ_{6}$ respectively forces $(b, d) = (0, 0)$ , $(c, d) = (0, 0)$ , or $(b, c) = (0, 0)$ . Their fixed fields are therefore $Q (\sqrt{3})$ , $Q (\sqrt{2})$ , and $Q (\sqrt{6})$ , which are distinct quadratic fields.

step 1.1algebra

3.1

The degrees in step 2.1 equal the subgroup indices prescribed by [L1], and [L1] is a bijection, so the table includes every subgroup and every intermediate field, including both endpoints.

step 2.1L1∎

Depends on

Used by

x⁴-10x²+1 has Galois group V₄ over ℚ Example
FALSE: the Galois correspondence preserves inclusion False statement

Dependency tree · two levels

16 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, biquadratic examples (standard reference, not scraped)
J. S. Milne, Fields and Galois Theory, v5.10, Chapter 3 (standard reference, not scraped)

The complete Galois correspondence for Q(2,3)/QQ(2​,3​)/Q