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.

$Gal (F_{8} / F_{2})$ is cyclic of order three with no proper intermediate field

Example

Let $K : = F_{2} [t] / (t^{3} + t + 1)$ and let $α$ be the class of $t$ . Then $K$ is a field of order $8$ , the squaring map $σ (x) = x^{2}$ generates

$Gal (K / F_{2}) = {i d, σ, σ^{2}},$

cyclic of order three, its two orbits on $K ∖ F_{2}$ are

${α, α^{2}, α^{2} + α} and {α + 1, α^{2} + 1, α^{2} + α + 1},$

and $K / F_{2}$ has no intermediate field other than $F_{2}$ and $K$ .

Facts & Assumptions

Given: The polynomial $π : = t^{3} + t + 1 \in F_{2} [t]$ , the ring $K = F_{2} [t] / (π)$ and the class $α$ of $t$ , so that $α^{3} = α + 1$ because $α^{3} + α + 1 = 0$ and $- 1 = 1$ in characteristic two.

[L1]

A polynomial of degree $2$ or $3$ over a field is irreducible if and only if it has no root in that field (A polynomial of degree two or three over a field is irreducible exactly when it has no root in the field).

[L2]

For a field $F$ and nonconstant $p \in F [x]$ , $p$ is irreducible if and only if $F [x] / (p)$ is a field (For a nonconstant $p$ in $F [x]$ , the ideal $(p)$ is maximal and $F [x] / (p)$ is a field exactly when $p$ is irreducible).

[L3]

If $a$ is algebraic over $F$ with minimal polynomial $m_{a}$ of degree $n$ , then $F (a)$ has power basis $1, a, \dots, a^{n - 1}$ and $[F (a) : F] = n$ (A simple algebraic extension is its minimal-polynomial quotient and has power basis $1, a, \dots, a^{n - 1}$ and degree $n$ , The degree $[K : F] = \dim_{F} K$ of a finite field extension); a monic irreducible vanishing at $a$ is that minimal polynomial (The evaluation kernel and the unique monic irreducible minimal polynomial of an algebraic element).

[L4]

An extension $E / F_{q}$ of finite fields of degree $n$ is Galois with $Gal (E / F_{q}) = ⟨ σ_{q} ⟩$ cyclic of order $n$ , where $σ_{q} (x) = x^{q}$ , and $∣ E ∣ = q^{n}$ (A finite extension of a finite field of order $q$ is Galois with cyclic Galois group generated by $x \mapsto x^{q}$ , The relative Frobenius $x \mapsto x^{q}$ of an extension of finite fields, For a degree- $n$ extension of a field of order $q$ , the $q$ -power map has order exactly $n$ , Finite fields and their order).

[L5]

The intermediate fields of $F_{q^{n}} / F_{q}$ are the $F_{q^{d}}$ for the positive divisors $d$ of $n$ , one for each divisor (The intermediate fields of $F_{q^{n}} / F_{q}$ are the $F_{q^{d}}$ , one for each positive divisor $d$ of $n$ , Divisibility in $Z$ : $d ∣ a$ when $a = d q$ for some integer $q$ ).

Verification

technique · direct

1.1

$π$ has no root in $F_{2}$ : $π (0) = 1$ and $π (1) = 1 + 1 + 1 = 1$ . By [L1] it is irreducible, so $K$ is a field by [L2].

L1L2given

2.1

$π$ is monic irreducible with $π (α) = 0$ , so it is the minimal polynomial of $α$ over $F_{2}$ and $[K : F_{2}] = 3$ with power basis $1, α, α^{2}$ by [L3]; hence $∣ K ∣ = 2^{3} = 8$ by [L4].

step 1.1L3L4

3.1

By [L4] the extension $K / F_{2}$ is Galois with Galois group generated by $σ (x) = x^{2}$ and of order three.

step 2.1L4

4.1

The orbit of $α$ : $α^{2}$ is $α^{2}$ ; $α^{4} = α \cdot α^{3} = α (α + 1) = α^{2} + α$ ; and $(α^{2} + α)^{2} = α^{4} + α^{2} = (α^{2} + α) + α^{2} = α$ , using that squaring is additive in characteristic two. So ${α, α^{2}, α^{2} + α}$ is one orbit of size three.

step 2.1step 3.1given

5.1

The orbit of $α + 1$ : $(α + 1)^{2} = α^{2} + 1$ , $(α^{2} + 1)^{2} = α^{4} + 1 = α^{2} + α + 1$ , and $(α^{2} + α + 1)^{2} = α^{4} + α^{2} + 1 = α + 1$ . So ${α + 1, α^{2} + 1, α^{2} + α + 1}$ is the other orbit of size three, and together with ${0}$ and ${1}$ these account for all eight elements.

step 2.1step 3.1step 4.1given

6.1

The positive divisors of three are $1$ and $3$ , so by [L5] the intermediate fields are exactly two: $F_{2}$ and $K$ itself. There is no field strictly between them.

step 2.1step 3.1L5∎

Remarks

Why the two nontrivial orbits have the same size. Each is an orbit of a group of prime order acting without fixed points outside $F_{2}$ : a fixed point of $σ$ is an element with $x^{2} = x$ , and those are exactly the two elements of $F_{2}$ (The elements of a finite extension fixed by the $q$ -power map are exactly the base field).

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

48 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), Examples 4.3-4.5 (standard reference, not scraped)
J. S. Milne, Fields and Galois Theory, v5.10, Chapter 4, Finite fields (standard reference, not scraped)

Gal⁡(F8/F2)Gal(F8​/F2​) is cyclic of order three with no proper intermediate field