ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck 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.

$\overline{F_{p}}$ is the union of its finite subfields and is an infinite algebraic extension

Example

For a prime $p$ , an algebraic closure $\overline{F_{p}}$ is the union of its finite subfields. It contains one subfield of order $p^{n}$ for every $n \geq 1$ , the nested fields $F_{p^{n!}}$ for $n \geq 1$ exhaust it, and it is an infinite algebraic extension of $F_{p}$ .

Facts & Assumptions

Given: A prime $p$ and an algebraic closure $Ω = \overline{F_{p}}$ .

[L1]

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

[L2]

Frobenius and all its iterates respect field operations in characteristic $p$ (Frobenius $x \mapsto x^{p}$ is an injective endomorphism in characteristic $p$ , and an automorphism for finite fields).

[L3]

A subset containing $0, 1$ and closed under subtraction, multiplication, and nonzero inverses 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]

Every field of order $q$ is the splitting field of $x^{q} - x$ over its prime field, and all of its elements are roots (A field with $q$ elements is the splitting field of $x^{q} - x$ over its prime subfield).

[L5]

Over every finite field there is an irreducible polynomial of each positive degree (For every finite field $F_{q}$ and every $n \geq 1$ , a monic irreducible polynomial of degree $n$ exists).

[L6]

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

[L7]

A nonzero polynomial is separable exactly when it is coprime to its derivative (A nonzero polynomial over a field is separable exactly when its gcd with its derivative is $1$ ).

[L8]

The degree of a simple algebraic extension is the degree of the minimal polynomial of its generator (A simple algebraic extension is its minimal-polynomial quotient and has power basis $1, a, \dots, a^{n - 1}$ and degree $n$ ).

Verification

technique · direct

1.1L1L6

Every $a \in Ω$ is algebraic over $F_{p}$ by [L6], so [L1] makes $F_{p} (a)$ a finite field. Hence $Ω$ is the union of its finite subfields.

1.2L2L3L4L6L7algebra

For $n \geq 1$ , let $E_{n}$ be the roots in $Ω$ of $x^{p^{n}} - x$ . This polynomial splits by [L6], and its derivative is $- 1$ , so [L7] gives exactly $p^{n}$ distinct roots. By [L2], the root set is closed under subtraction and multiplication, and it is closed under nonzero inverses; hence [L3] makes $E_{n}$ a subfield of order $p^{n}$ . Any other subfield of that order consists entirely of roots by [L4], so it equals $E_{n}$ .

2.1step 1.1step 1.2L2L4

If $a$ lies in a finite subfield of order $p^{d}$ , choose $n \geq d$ . Every element $b$ of that subfield satisfies $b^{p^{d}} = b$ by [L4]. Since $d$ divides $n!$ , iterating Frobenius by [L2] gives $b^{p^{n!}} = b$ , so the subfield lies in $E_{n!}$ . The same argument shows $E_{n!} \subseteq E_{(n + 1)!}$ , and step 1.1 now shows that their nested union is all of $Ω$ .

3.1L5L6L8∎

The irreducibles supplied by [L5] have roots in $Ω$ by [L6], and [L8] makes the generated simple subextensions have arbitrarily large finite degree. Therefore $Ω$ cannot be finite, while it is algebraic by [L6].

Depends on

Used by

FALSE: every algebraic extension is simple False statement

Dependency tree · two levels

42 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

J. S. Milne, Fields and Galois Theory, finite fields and algebraic closures (standard reference, not scraped)

Fp‾Fp​​ is the union of its finite subfields and is an infinite algebraic extension