ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17

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.

$Q (\sqrt[3]{2})$ has three embeddings into $\overline{Q}$ but only one $Q$ -automorphism

Example

Let $r = \sqrt[3]{2}$ be the positive real cube root of $2$ . The extension $Q (r) / Q$ has three embeddings into an algebraic closure of $Q$ , but its only $Q$ -automorphism is the identity.

Facts & Assumptions

Given: The positive real cube root $r$ of $2$ and an algebraic closure $Ω / Q$ .

[L1]

Eisenstein's criterion proves irreducibility over $Q$ for a primitive integer polynomial satisfying its divisibility hypotheses (Eisenstein criterion over the integers).

[L2]

Embeddings of a simple algebraic extension correspond to the distinct roots of its minimal polynomial ( $F$ -embeddings of $F (α)$ into an algebraically closed field correspond to the distinct roots of $m_{α}$ ).

[L3]

Characteristic-zero fields are perfect, so their irreducible polynomials are separable (Fields of characteristic zero, finite fields, and algebraically closed fields are perfect).

[L4]

Positive real $n$ th roots exist and are unique (Existence and uniqueness of $n$ -th roots: a unique $a^{1 / n} \geq 0$ with $(a^{1 / n})^{n} = a$ ).

[L5]

The real numbers form an ordered field (The reals form a totally ordered field).

Verification

technique · direct

1.1

The polynomial $x^{3} - 2$ is Eisenstein at $2$ , so [L1] makes it the minimal polynomial of $r$ . By [L3] its three roots in $Ω$ are distinct, and [L2] gives three $Q$ -embeddings of $Q (r)$ into $Ω$ .

L1L2L3

1.2

The field $Q (r)$ lies in $R$ . In an ordered field the map $x \mapsto x^{3}$ is strictly increasing, or directly $u^{3} - v^{3} = (u - v) (u^{2} + u v + v^{2})$ with the second factor positive for $u \neq v$ ; hence [L4] and [L5] make $r$ the only real root of $x^{3} - 2$ .

L4L5algebra

2.1

A $Q$ -automorphism of $Q (r)$ must send $r$ to another root lying inside the same real field. Step 1.2 forces that image to be $r$ , so the automorphism fixes the generator and is the identity.

step 1.2L2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 112 results over 17 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

P. L. Clark, Field Theory, Chapter 4 (standard reference, not scraped)
J. S. Milne, Fields and Galois Theory, Chapters 2 to 6 (standard reference, not scraped)

Q(23)Q(32​) has three embeddings into Q‾Q​ but only one QQ-automorphism