Alphabeta Math
Session-authored (Fable 5 assisted)
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.

13 results · all verified · 7 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 6 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

The Fundamental Theorem of Algebra

1 · Prerequisites

2 · Summary

This page proves the fundamental theorem of algebra below the later analytic minimum-modulus proof, so the route here is deliberately different. The route is mostly algebraic, but it still uses two real-analytic inputs: the odd-degree real-root theorem from continuity and the intermediate value theorem, and the real square-root existence used by the published complex square-root theorem. Everything else is field theory and finite Galois theory: splitting fields, fixed fields, Sylow 2-subgroups, and the fact that a quadratic extension of a field of characteristic not 2 is generated by a square root.

Once the Artin proof shows that C is algebraically closed, the page records the main algebraic consequences needed later in the track: splitting of complex polynomials, algebraic-closure statements for R and Q, the classification of irreducible real polynomials, real factorisation into linear and irreducible quadratic factors, and the counted multiplicity form of the theorem.

3 · Logical flowchart

4 · Definitions, theorems and proofs

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-27Open item page →

Every odd-degree real polynomial has a real root

Statement

Let

f(x)=anxn+an1xn1++a0R[x]

have odd degree n1. Then there exists cR with f(c)=0.

Facts & Assumptions

Given: A real polynomial f(x)=anxn++a0 of odd degree n1.

[F1]

The degree hypothesis means an0 and ai=0 for every i>n (Degree, leading coefficient and monic polynomial, with the zero polynomial having no degree).

[L2]

A continuous function on a closed interval takes every intermediate value between its endpoint values (Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on [a,b] takes every value between f(a) and f(b)).

[F2]

The real numbers form an ordered field, so absolute values and the order laws behave as usual (The reals form a totally ordered field).

Proof

technique · direct
1.1

Put S:=i<nai and R:=1+San. Then R>1, and therefore i<naiRiSRn1<anRn.

F1F2algebra
2.1

The estimate in step 1.1 gives i<naiRii<naiRi<anRn. Hence f(R)=anRn+i<naiRi has the same sign as an.

step 1.1F2algebra
2.2

Because n is odd, (R)n=Rn. Also i<nai(R)ii<naiRi<anRn, so f(R)=an(R)n+i<nai(R)i has the opposite sign from an. Thus f(R) and f(R) have opposite signs.

step 1.1F1F2algebra
3.1

By [L1], the polynomial function f is continuous on [R,R]. Since step 2.2 shows that 0 lies between f(R) and f(R), [L2] gives a point c[R,R] with f(c)=0.

L1L2step 2.2
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

An irreducible polynomial over R has degree 1 or an even degree

Statement

If fR[x] is irreducible, then degf=1 or degf is even.

Facts & Assumptions

Given: An irreducible polynomial fR[x].

[L1]

Every odd-degree real polynomial has a real root (Every odd-degree real polynomial has a real root).

[L2]

For a commutative ring R, an element aR, and a polynomial pR[x], one has p(a)=0 if and only if xa divides p (Factor theorem over a commutative ring).

Proof

technique · direct
1.1

Suppose degf is odd. Then [L1] gives aR with f(a)=0.

givenL1
2.1

By [L2], the linear polynomial xa divides f. Since f is irreducible and xa is nonconstant, this forces f to be associated to xa, so degf=1.

step 1.1L2algebra
3.1

Therefore an irreducible real polynomial can have odd degree only in the linear case. If it is not linear, its degree is not odd and hence is even.

step 2.1algebra
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

To prove the fundamental theorem of algebra, it suffices to split every real polynomial over C

Statement

Assume every nonconstant polynomial in R[x] splits over C. Then C is algebraically closed.

Facts & Assumptions

Given: Every nonconstant polynomial in R[x] splits over C, and a nonconstant polynomial gC[x].

[L1]

A field is algebraically closed exactly when every nonconstant polynomial over it has a root in the field (An algebraically closed field: every nonconstant polynomial has a root in the field).

[L2]

A nonzero polynomial splits over a field extension when it is a nonzero scalar times a product of linear factors there (Polynomials that split and splitting fields of a polynomial or a family of polynomials).

Proof

technique · direct
1.1

Write g=u+iv with u,vR[x], and put g:=uiv. Then gg=u2+v2R[x]. Because g is nonconstant, so is gg.

givenF1algebra
2.1

By the standing hypothesis and [L2], the real polynomial gg splits over C, so it has a complex root z. In particular, 0=(gg)(z)=g(z)g(z).

givenL2step 1.1
3.1

Since C is a field by [F1], step 2.1 implies either g(z)=0 or g(z)=0.

F1step 2.1
4.1

If g(z)=0 then g already has a root in C. If g(z)=0, then conjugating that equality and using the conjugation law from [F1] gives g(z)=0. Thus g has a root in C in either case.

F1step 3.1algebra
5.1

The polynomial gC[x] was arbitrary. Therefore every nonconstant polynomial over C has a root in C, and [L1] makes C algebraically closed.

L1step 4.1
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-27Open item page →

A quadratic extension in characteristic not 2 is obtained by adjoining a square root

Statement

Let E/F be a field extension with [E:F]=2 and charF2. Then there is dF such that E=F(d). In fact d may be chosen to be a nonsquare in F.

Facts & Assumptions

Given: A quadratic extension E/F with charF2.

[L1]
[L2]

In a finite tower of fields, degrees multiply (Tower law for finite extensions: [L:F]=[L:K][K:F]).

Proof

technique · direct
1.1

Choose αEF. Then FF(α)E. Since [E:F]=2, fact [L2] forces [F(α):F]=2 and hence E=F(α). Therefore [L1] gives mα(x)=x2+bx+c with b,cF.

L1L2choose
2.1

Because charF2, the element 2 is invertible in F. Put δ:=2α+b. Using mα(α)=0, δ2=4α2+4bα+b2=b24cF.

step 1.1algebra
3.1

Also α=δb2, so F(α)=F(δ). Therefore E=F(α)=F(δ)=F(d) with d:=δ2F. If d were already a square in F, then δF and the displayed formula would give αF, contradicting step 1.1. Hence d may be chosen nonsquare.

step 2.1step 1.1algebra
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-27Open item page →

A field is algebraically closed exactly when every nonconstant polynomial splits, equivalently when it has no nontrivial finite extension

Statement

For a field F, the following are equivalent:

  1. F is algebraically closed.
  2. Every nonconstant polynomial in F[x] splits over F.
  3. F has no nontrivial finite extension.

Facts & Assumptions

Given: A field F.

[L1]

A field is algebraically closed exactly when every nonconstant polynomial over it has a root in the field (An algebraically closed field: every nonconstant polynomial has a root in the field).

[L2]

Splitting means factorization into linear factors over the field (Polynomials that split and splitting fields of a polynomial or a family of polynomials).

[L3]

A polynomial p has a as a root exactly when xa divides p (Factor theorem over a commutative ring).

[L4]

An element is algebraic over F if and only if its simple extension over F is finite (An element is algebraic over F if and only if its simple extension F(a)/F is finite).

[L5]

Every nonconstant polynomial over F has a root in some extension of F (Every nonconstant polynomial over a field has a root in some field extension).

[L6]

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

[L7]

Every algebraic element has a unique monic irreducible minimal polynomial, and a polynomial vanishes at that element exactly when the minimal polynomial divides it (The evaluation kernel and the unique monic irreducible minimal polynomial of an algebraic element).

Proof

technique · direct
1.1

Assume F is algebraically closed, and let fF[x] be nonconstant. By [L1] it has a root aF, so [L3] gives f=(xa)q for some qF[x]. Repeating the same argument on q while it remains nonconstant writes f as a product of linear factors, so f splits over F in the sense of [L2].

L1L2L3choose
1.2

Assume every nonconstant polynomial in F[x] splits over F, and let E/F be finite. For any αE, fact [L6] makes α algebraic over F. If αF, let mα be its minimal polynomial over F. Then [L7] makes mα a nonconstant irreducible polynomial with mα(α)=0. By the hypothesis, mα splits over F and therefore has a root aF. Fact [L3] gives xa as a linear factor of mα, contradicting irreducibility. Hence every αE already lies in F, so E=F.

L3L6L7algebra
1.3

Assume F has no nontrivial finite extension, and let fF[x] be nonconstant. By [L5] there is an extension K/F and an element αK with f(α)=0. Then α is algebraic over F, so [L4] makes F(α)/F finite. By the hypothesis this finite extension must be trivial, hence αF. Therefore every nonconstant polynomial over F has a root in F, and [L1] says that F is algebraically closed.

L1L4L5
2.1

Steps 1.1, 1.2, and 1.3 prove (1)(2)(3)(1), so the three conditions are equivalent.

step 1.1step 1.2step 1.3
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-27Open item page →

The complex numbers are algebraically closed

Statement

The field C is algebraically closed.

Facts & Assumptions

Given: A nonconstant polynomial gC[x].

[L1]

If every nonconstant polynomial in R[x] splits over C, then C is algebraically closed (To prove the fundamental theorem of algebra, it suffices to split every real polynomial over C).

[L2]

Every finite family of nonzero polynomials has a splitting field (Every finite family of nonzero polynomials has a splitting field, obtained from their product).

[L3]

An algebraic extension that is a splitting field of a polynomial is normal (An algebraic extension that is a splitting field of a polynomial is normal).

[L4]

Every field of characteristic zero is perfect, and every algebraic extension of a perfect field is separable (Fields of characteristic zero, finite fields, and algebraically closed fields are perfect, Every algebraic extension of a perfect field is separable).

[L5]

For a finite Galois extension K/F with group G, the maps HKH and EGal(K/E) are inverse inclusion-reversing bijections, and [K:KH]=H,[KH:F]=[G:H]. (The fundamental theorem of finite Galois theory)

[L7]

Every finite group has a Sylow 2-subgroup (Sylow I: every finite group has a Sylow p-subgroup).

[L8]

Every nontrivial finite p-group has a subgroup of index p (Every nontrivial finite p-group has a normal subgroup of index p).

[L9]

Every complex number has a square root in C (Every complex number has a square root, by an explicit Cartesian formula).

[L10]

A square root of 1 in a real field extension determines a unique real-field embedding of C into that extension (A square root of 1 in a real field extension determines a unique real-field homomorphism from C).

[L11]

A quadratic extension in characteristic not 2 is obtained by adjoining a square root (A quadratic extension in characteristic not 2 is obtained by adjoining a square root).

[L12]

An irreducible polynomial over R has degree 1 or an even degree (An irreducible polynomial over R has degree 1 or an even degree).

[L13]

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

[L14]

If α is algebraic over a field F, then the degree of its minimal polynomial equals [F(α):F] (An element is algebraic over F if and only if its simple extension F(a)/F is finite).

Proof

technique · direct
1.1

By [L1], it is enough to prove that every nonconstant polynomial in R[x] splits over C. Fix such a polynomial fR[x].

L1suffices: split every nonconstant real polynomial over C
1.2

Put h:=f(x)(x2+1). By [L2], choose a splitting field E/R of h. The roots of h are algebraic over R, and E is generated by finitely many of them, so [L13] makes E/R finite. Because E is a splitting field of h, [L3] makes it normal, and [L4] makes it separable. Thus E/R is finite Galois.

L2L3L4L13choose
1.3

Let G:=Gal(E/R). By [L7], choose a Sylow 2-subgroup HG, and put M:=EH. Then [L5] gives [M:R]=[G:H], which is odd by the definition of a Sylow 2-subgroup.

L5L7choose
2.1

Since x2+1 splits in E, choose jE with j2=1. By [L10], there is a unique real-field embedding ι:CE sending i to j. Identify C with its image, so that RCE.

L10step 1.2choose
2.2

Let αM. Since RR(α)M, the tower law [L6] shows that [R(α):R] divides [M:R], so [R(α):R] is odd. Because αE and step 1.2 made E/R finite, the element α is algebraic over R. Fact [L14] therefore makes the minimal-polynomial degree of α over R equal to the same odd number [R(α):R]; by [L12] it must have degree 1. Hence αR. Since every element of M lies in R, we get M=R.

L6L12L14step 1.2step 1.3algebra
3.1

Because M=EH=R=EG, the bijection in [L5] forces H=G. Therefore G is a finite 2-group.

L5step 2.2
4.1

Put J:=Gal(E/C). Then JG, so step 3.1 makes J a finite 2-group. Suppose J is nontrivial.

step 2.1step 3.1assume-contra
5.1

By [L8], the nontrivial 2-group J has a subgroup K of index 2. Put L:=EK. Then EJ=C by [L5], and [L5] together with [L6] gives [L:C]=[J:K]=2.

L5L6L8step 4.1construct
6.1

The field C has characteristic zero, hence not 2, so [L11] makes the quadratic extension L/C equal to C(d) for some dC. By [L9], choose eC with e2=d. Then L=C(d)=C(e)=C, contradicting step 5.1. Therefore J is trivial.

L9L11step 5.1discharge-contradiction
7.1

Since Gal(E/C)=1, the fixed field of the trivial subgroup is E; by [L5], that fixed field is also C. Thus E=C. Because E is a splitting field of h and f divides h, the polynomial f splits over C. By step 1.1 and [L1], this proves that C is algebraically closed.

L1L5step 1.1step 1.2step 2.1step 6.1
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

Every nonconstant polynomial in C[x] splits into linear factors

Statement

Every nonconstant polynomial in C[x] splits over C.

Facts & Assumptions

Given: A nonconstant polynomial fC[x].

[L1]

The field C is algebraically closed (The complex numbers are algebraically closed).

[L2]

A field is algebraically closed exactly when every nonconstant polynomial over it splits (A field is algebraically closed exactly when every nonconstant polynomial splits, equivalently when it has no nontrivial finite extension).

Proof

technique · direct
1.1

By [L1], the field C is algebraically closed.

L1
2.1

Applying [L2] to the field C and the given polynomial f shows that f splits over C.

step 1.1L2
3.1

Since f was arbitrary, every nonconstant polynomial in C[x] splits over C.

step 2.1
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

The complex numbers form an algebraic closure of R

Statement

The field extension C/R is an algebraic closure of R.

Facts & Assumptions

Given: The field extension C/R.

[L1]

The field C is algebraically closed (The complex numbers are algebraically closed).

[L2]

The complex field is a simple algebraic extension of R of degree 2 (C/R has power basis 1,i and degree 2).

[L3]

An algebraic closure of a field is an algebraic extension whose top field is algebraically closed (An algebraic closure of a field).

Proof

technique · direct
1.1

Fact [L1] gives the algebraically closed part of the definition in [L3].

L1
1.2

Fact [L2] gives the algebraic-extension part of the definition in [L3].

L2
2.1

Therefore [L3] makes C/R an algebraic closure of R.

L3step 1.1step 1.2
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

The algebraic numbers in C form an algebraic closure of Q

Statement

Let

A:={zC:z is algebraic over Q}.

Then A is an algebraic closure of Q.

Facts & Assumptions

Given: The subset AC of elements algebraic over Q.

[L1]

The algebraic elements in an extension form a subfield (The elements of an extension algebraic over the base field form a subfield).

[L2]

The field C is algebraically closed (The complex numbers are algebraically closed).

[L3]

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

[L4]

An element is algebraic over a field if and only if its simple extension over that field is finite (An element is algebraic over F if and only if its simple extension F(a)/F is finite).

[L6]

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

[L7]

An algebraic closure of a field is an algebraic extension whose top field is algebraically closed (An algebraic closure of a field).

Proof

technique · direct
1.1

By [L1], the set A is a subfield of C containing Q.

L1
1.2

Let f(x)=anxn++a0A[x] be nonconstant. Since C is algebraically closed by [L2], the polynomial f has a root zC.

L2
2.1

The coefficients a0,,an are algebraic over Q, so F:=Q(a0,,an) is a finite extension of Q by [L3]. The element z is a root of a nonzero polynomial over F, so it is algebraic over F; therefore [L4] makes F(z)/F finite. By [L5], the extension F(z)/Q is finite, and then [L6] makes z algebraic over Q. Hence zA.

L3L4L5L6step 1.2
3.1

Step 2.1 shows that every nonconstant polynomial in A[x] has a root in A, so A is algebraically closed. Since every element of A is algebraic over Q by definition, [L7] makes A an algebraic closure of Q.

L7step 2.1
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-27Open item page →

A nonreal root of a real polynomial comes with its complex conjugate

Statement

Let fR[x] and let zCR. If f(z)=0, then f(z)=0.

Facts & Assumptions

Given: A real polynomial fR[x] and a nonreal complex number z with f(z)=0.

[L1]

Complex conjugation is a field automorphism of C that fixes R pointwise (The only real-field automorphisms of C are the identity and complex conjugation).

Proof

technique · direct
1.1

By [L1], complex conjugation fixes every coefficient of f.

L1
1.2

Apply conjugation to the equality f(z)=0. Because conjugation is a field automorphism and fixes the coefficients of f, this gives 0=f(z)=f(z).

L1givenalgebra
2.1

Therefore z is also a root of f. Since zR, one has zz, so the two roots form a conjugate pair.

step 1.2algebra
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-27Open item page →

An irreducible polynomial in R[x] has degree 1 or 2

Statement

If fR[x] is irreducible, then degf=1 or degf=2.

Facts & Assumptions

Given: An irreducible polynomial fR[x].

[L1]

The field C is algebraically closed, so every nonconstant polynomial in C[x] has a complex root (The complex numbers are algebraically closed).

[L2]

A nonreal root of a real polynomial comes with its complex conjugate (A nonreal root of a real polynomial comes with its complex conjugate).

[L3]

The minimal polynomial of an algebraic element divides every polynomial that vanishes at that element (The evaluation kernel and the unique monic irreducible minimal polynomial of an algebraic element).

Proof

technique · direct
1.1

By [L1], choose a root zC of f. If zR, then the minimal polynomial of z over R is xz, and [L3] makes xz divide f. Since f is irreducible, this forces degf=1.

L1L3choose
2.1

Suppose instead that zR. Then [L2] gives f(z)=0. Put q(x):=(xz)(xz)=x2(z+z)x+zzR[x]. Because q(z)=0, fact [L3] makes the minimal polynomial of z over R divide q and also divide f. Since f is irreducible, that minimal polynomial is associated to f, so degfdegq=2. The degree cannot be 1 in the nonreal case, hence degf=2.

L2L3step 1.1algebra
3.1

The real-root and nonreal-root cases are exhaustive, so every irreducible polynomial in R[x] has degree 1 or 2.

step 1.1step 2.1
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

Every real polynomial factors into linear and irreducible quadratic factors

Statement

Every nonzero polynomial fR[x] can be written as a nonzero real scalar times a product of linear polynomials and irreducible quadratic polynomials.

Facts & Assumptions

Given: A nonzero polynomial fR[x].

[L1]

Every nonzero nonunit polynomial over a field factors into irreducible polynomials (Every nonzero nonunit polynomial over a field factors into irreducible polynomials).

[L2]

An irreducible polynomial in R[x] has degree 1 or 2 (An irreducible polynomial in R[x] has degree 1 or 2).

Proof

technique · direct
1.1

If f is a nonzero constant, then it already has the required form: it is itself the nonzero scalar multiplying the empty product. Now assume that f is a nonzero nonunit polynomial. By [L1], it factors as f=up1pr with uR× and each pj irreducible in R[x].

L1algebra
2.1

By [L2], each irreducible factor pj has degree 1 or 2. Therefore each pj is either linear or an irreducible quadratic, so the factorization of step 1.1 is exactly the required one.

L2step 1.1
3.1

The constant and nonconstant cases together prove the statement for every nonzero polynomial in R[x].

step 1.1step 2.1
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-27Open item page →

A complex polynomial of degree n has exactly n roots counted with multiplicity

Statement

Let fC[x] have degree n1. Then there exist distinct complex numbers α1,,αr and positive integers m1,,mr such that

f(x)=cj=1r(xαj)mj

for some cC×, with

m1++mr=n.

These exponents are uniquely determined by f. Equivalently, f has exactly n roots counted with multiplicity.

Facts & Assumptions

Given: A polynomial fC[x] of degree n1.

[L1]

Every nonconstant polynomial in C[x] splits over C (Every nonconstant polynomial in C[x] splits into linear factors).

[L2]

Splitting means a nonzero scalar times a product of linear factors (Polynomials that split and splitting fields of a polynomial or a family of polynomials).

[L3]

The polynomial ring C[x] is a unique factorization domain (For every field F, F[x] is a unique factorisation domain).

Proof

technique · direct
1.1

By [L1] and [L2], there are cC× and complex numbers β1,,βn such that f(x)=ck=1n(xβk). Let α1,,αr be the distinct values among the βk, and let mj be the number of indices k with βk=αj. Then f(x)=cj=1r(xαj)mj, and by construction m1++mr=n.

L1L2construct
2.1

Suppose also that f(x)=cj=1s(xγj)nj with cC×, distinct γj, and positive integers nj. In the UFD C[x], each linear factor xα is irreducible, hence prime. Therefore the exponent with which xα appears in a factorization of f is uniquely determined. After reordering, this gives r=s,γj=αj,nj=mj for every j. So the multiplicities are well defined.

L3step 1.1algebra
3.1

Step 1.1 gives a factorization whose exponents sum to n, and step 2.1 gives uniqueness of those exponents. This is exactly the statement that a degree-n complex polynomial has exactly n roots counted with multiplicity.

step 1.1step 2.1

5 · Examples, counterexamples and false statements

None yet.

Sources