Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16
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 elements of an extension algebraic over the base field form a subfield

Statement

For a field extension K/F, the set

A={a∈K:a is algebraic over F}

is a subfield of K containing F.

Facts & Assumptions

Given: A field extension K/F and algebraic elements a,b∈K.

[L1]

A field generated by finitely many algebraic elements is finite over the base (An extension generated by finitely many algebraic elements is finite).

[L2]

Every element of a finite extension is algebraic over the base (Every finite field extension is algebraic).

[L3]

A subset containing 1 and closed under subtraction, multiplication, and inverses of nonzero elements is a subfield (Subfield: a subring of a field closed under inverses of its nonzero elements, and therefore a field with the restricted operations).

[L4]

Algebraic means annihilated by a nonzero polynomial over the base field (Algebraic and transcendental elements and algebraic extensions).

Proof

technique · direct
1.1

Every c∈F is algebraic over F, since it is a root of t−c, so F⊆A and in particular 0,1∈A.

L4
1.2

By [L1], F(a,b)/F is finite. Thus [L2] makes all of its elements algebraic over F, including a−b and ab.

givenL1L2
1.3

If a≠0, then a−1∈F(a)⊆F(a,b) and is algebraic by the same argument.

givenL1L2
2.1

Therefore A satisfies the subfield criterion [L3] and is a subfield containing F.

step 1.1step 1.2step 1.3L3∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 50 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