ExampleConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26

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 intermediate fields of $F_{2^{12}} / F_{2}$ match the divisors of twelve

Example

Let $E$ be a field with $F_{2}$ as a subfield and $[E : F_{2}] = 12$ , so that $∣ E ∣ = 2^{12}$ . Its intermediate fields over $F_{2}$ are exactly

$F_{2}, F_{2^{2}}, F_{2^{3}}, F_{2^{4}}, F_{2^{6}}, F_{2^{12}} = E,$

one for each of the six positive divisors $1, 2, 3, 4, 6, 12$ of twelve, with $F_{2^{d}} \subseteq F_{2^{e}}$ exactly when $d$ divides $e$ . Neither of $F_{2^{4}}$ and $F_{2^{6}}$ contains the other, and

$F_{2^{4}} \cap F_{2^{6}} = F_{2^{2}}, F_{2^{4}} F_{2^{6}} = F_{2^{12}} .$

Facts & Assumptions

Given: A field $E$ with subfield $F_{2}$ and $[E : F_{2}] = 12$ (The degree $[K : F] = \dim_{F} K$ of a finite field extension); divisibility as in Divisibility in $Z$ : $d ∣ a$ when $a = d q$ for some integer $q$ , with $\gcd$ and $lcm$ as in Common divisor, and the greatest common divisor $\gcd (a, b)$ , with the convention $\gcd (0, 0) : = 0$ and Common multiple, and the least common multiple $lcm (a, b)$ , taken to be $0$ when $a = 0$ or $b = 0$ .

[L1]

$E / F_{2}$ is Galois with cyclic Galois group generated by $x \mapsto x^{2}$ (A finite extension of a finite field of order $q$ is Galois with cyclic Galois group generated by $x \mapsto x^{q}$ ), and $∣ E ∣ = 2^{12}$ (For a degree- $n$ extension of a field of order $q$ , the $q$ -power map has order exactly $n$ , Finite fields and their order).

[L2]

The intermediate fields of $F_{q^{n}} / F_{q}$ are exactly the $F_{q^{d}} = {x : x^{q^{d}} = x}$ for the positive divisors $d$ of $n$ , one for each divisor, with $[F_{q^{d}} : F_{q}] = d$ and $F_{q^{d}} \subseteq F_{q^{e}}$ if and only if $d ∣ e$ (The intermediate fields of $F_{q^{n}} / F_{q}$ are the $F_{q^{d}}$ , one for each positive divisor $d$ of $n$ ).

[L3]

A field of order $p^{m}$ has, for each positive divisor $e$ of $m$ , exactly one subfield of order $p^{e}$ , namely ${a : a^{p^{e}} = a}$ , and these are all of its subfields (The subfields of $F_{p^{n}}$ are the unique fields $F_{p^{d}}$ for positive divisors $d$ of $n$ ).

[L4]

Every common divisor of two integers divides their greatest common divisor, and their least common multiple divides every common multiple (Every common divisor of $a$ and $b$ divides $\gcd (a, b)$ ; consequently $d = \gcd (a, b)$ exactly when $d \geq 0$ , $d ∣ a$ , $d ∣ b$ , and every common divisor of $a$ and $b$ divides $d$ — a characterisation that holds at $(a, b) = (0, 0)$ as well, Every common multiple of $a$ and $b$ is a multiple of $lcm (a, b)$ , and $\gcd (a, b) \cdot lcm (a, b) = ∣ a b ∣$ ).

Verification

technique · direct

1.1

The positive divisors of twelve are $1, 2, 3, 4, 6, 12$ , six in all, since a positive divisor $d$ of $12$ satisfies $d \leq 12$ and direct inspection of $1, \dots, 12$ leaves exactly these.

givenalgebra

2.1

By [L1] and [L2] the intermediate fields of $E / F_{2}$ are the $F_{2^{d}}$ for those six $d$ , one for each, with $F_{2^{d}} \subseteq F_{2^{e}}$ exactly when $d ∣ e$ .

step 1.1L1L2

3.1

Neither $4 ∣ 6$ nor $6 ∣ 4$ , so by step 2.1 neither of $F_{2^{4}}$ and $F_{2^{6}}$ contains the other.

step 2.1given

4.1

Their intersection is an intermediate field of $E / F_{2}$ , being a subfield of $E$ containing $F_{2}$ , so it is $F_{2^{c}}$ for a unique divisor $c$ of $12$ by step 2.1; from $F_{2^{c}} \subseteq F_{2^{4}}$ and $F_{2^{c}} \subseteq F_{2^{6}}$ one gets $c ∣ 4$ and $c ∣ 6$ , so [L4] gives $c ∣ \gcd (4, 6) = 2$ ; and $2 ∣ 4$ and $2 ∣ 6$ put $F_{2^{2}}$ inside both, so $2 ∣ c$ . Hence $c = 2$ and the intersection is $F_{2^{2}}$ .

step 2.1step 3.1L4

5.1

Their compositum is likewise an intermediate field $F_{2^{c^{'}}}$ , and it contains both, so $4 ∣ c^{'}$ and $6 ∣ c^{'}$ by step 2.1. Thus [L4] gives $lcm (4, 6) = 12 ∣ c^{'}$ ; since $c^{'} ∣ 12$ , $c^{'} = 12$ and the compositum is $E = F_{2^{12}}$ .

step 2.1step 4.1L4

6.1

The same six fields are what [L3] produces for $E$ , whose order is $2^{12}$ : its subfields are the ${a : a^{2^{e}} = a}$ for the divisors $e$ of $12$ , and these are the sets named in [L2]. So the Galois indexing and the elementary one agree here.

step 2.1step 5.1L2L3∎

Remarks

Where the two descriptions coincide. Because the base field is the prime field, the divisors of $[E : F_{2}]$ and the divisors of $\log_{2} ∣ E ∣$ are the same list; over a larger base field the two indexings differ by the factor $[F_{q} : F_{p}]$ , and The Galois description of the subfields of a finite field and the elementary divisibility criterion agree records the translation.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

51 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

K. Conrad, Finite Fields (expository blurb), Example 2.9 (standard reference, not scraped)
J. S. Milne, Fields and Galois Theory, v5.10, Corollary 4.21 (standard reference, not scraped)

The intermediate fields of F212/F2F212​/F2​ match the divisors of twelve