Alphabeta Math
False statementConstruction: AI-adaptedVerification: AI-generatedSession-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.

FALSE: an algebraic closure is unique up to a unique base-field isomorphism

Statement

For any two algebraic closures of a field F, there is exactly one F-isomorphism between them.

Facts & Assumptions

Given: The axiom of Choice and the field Q.

[L1]

Assuming Choice, every field has an algebraic closure (Assuming Choice, every field has an algebraic closure).

[L2]

Embeddings of a simple 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]

Assuming Choice, a base embedding extends across an algebraic extension into an algebraically closed field (Assuming Choice, a base-field embedding extends across every algebraic extension).

[L4]

Assuming Choice, any two algebraic closures of the same field are isomorphic over that field (Assuming Choice, any two algebraic closures are base-isomorphic).

[L5]

An algebraic closure is algebraic over its base and algebraically closed (An algebraic closure of a field).

[L6]

Every algebraic element has a monic irreducible minimal polynomial over the base (The evaluation kernel and the unique monic irreducible minimal polynomial of an algebraic element).

Refutation

technique · direct
1.1

Choose Ω by [L1]. The polynomial x2+1 is irreducible over Q and has a root aΩ by [L5]. Its roots a and a are distinct because Q has characteristic zero. By [L2], the assignment aa gives a nonidentity Q-embedding of Q(a) into Ω.

L1L2L5algebra
2.1

Extend that embedding across the algebraic extension Ω/Q(a) using [L3]. Its image E is algebraically closed because it is isomorphic to Ω. Every bΩ is algebraic over QE by [L5], so [L6] gives a minimal polynomial over E; it has a root in E and is therefore linear. Thus the resulting embedding τ:ΩΩ is surjective, hence is a nonidentity Q-automorphism with τ(a)=a.

step 1.1L3L5L6
3.1

The identity and τ are distinct Q-isomorphisms from the same algebraic closure to itself. Therefore uniqueness of the base-field isomorphism is false, although existence is true by [L4].

step 2.1L4

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: 48 results over 8 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