ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck 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 four roots of $t^{4} + t + 1$ over $F_{2}$ are the Frobenius powers of any one of them

Example

Let $K : = F_{2} [t] / (t^{4} + t + 1)$ and let $α$ be the class of $t$ , so $α^{4} = α + 1$ . Then $K$ is a field of order $16$ , and the four conjugates of $α$ over $F_{2}$ ,

$α, α^{2}, α^{4} = α + 1, α^{8} = α^{2} + 1,$

are pairwise distinct, are exactly the roots of $t^{4} + t + 1$ in $K$ , and satisfy $α^{16} = α$ , so the Frobenius orbit closes at length four.

Facts & Assumptions

Given: The polynomial $π : = t^{4} + t + 1 \in F_{2} [t]$ , the ring $K = F_{2} [t] / (π)$ , and the class $α$ of $t$ , so $α^{4} = α + 1$ since $- 1 = 1$ in characteristic two; squaring is additive there.

[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]

$f (a) = 0$ if and only if $x - a$ divides $f$ (Factor theorem over a commutative ring); and over an integral domain $\deg (f g) = \deg f + \deg g$ for nonzero $f, g$ (Over an integral domain, degrees add under multiplication of nonzero polynomials, Degree, leading coefficient and monic polynomial, with the zero polynomial having no degree).

[L3]

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).

[L4]

A monic irreducible vanishing at $a$ is the minimal polynomial of $a$ (The evaluation kernel and the unique monic irreducible minimal polynomial of an algebraic element), and then $F (a)$ has power basis $1, a, \dots, a^{n - 1}$ with $[F (a) : F] = n$ its degree (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).

[L5]

An extension of finite fields of degree $n$ over $F_{q}$ is Galois with cyclic Galois group generated by $σ_{q} (x) = x^{q}$ , and has $q^{n}$ elements (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$ ).

[L6]

A monic irreducible $π$ of degree $d$ over $F_{q}$ with a root $α$ has the $d$ distinct roots $α, α^{q}, \dots, α^{q^{d - 1}}$ and $π = \prod_{i < d} (t - α^{q^{i}})$ (A monic irreducible of degree $d$ over $F_{q}$ has the $d$ distinct roots $α, α^{q}, \dots, α^{q^{d - 1}}$ ).

Verification

technique · direct

1.1L2given

$π$ has no root in $F_{2}$ , since $π (0) = 1$ and $π (1) = 1 + 1 + 1 = 1$ ; so by [L2] it has no factor of degree one.

1.2L1L2given

The only monic irreducible quadratic in $F_{2} [t]$ is $t^{2} + t + 1$ : the four monic quadratics are $t^{2}$ , $t^{2} + 1$ , $t^{2} + t$ and $t^{2} + t + 1$ , and the first three have the root $0$ , $1$ and $0$ respectively, so [L1] leaves only the last.

2.1step 1.1step 1.2L2given

$π$ is irreducible. A factorisation of $π$ into two nonconstant factors has degrees summing to four by [L2], so it is either $1 + 3$ , excluded by step 1.1, or $2 + 2$ ; and every monic quadratic factor would have to be irreducible, hence equal to $t^{2} + t + 1$ by step 1.2, giving $π = (t^{2} + t + 1)^{2} = t^{4} + t^{2} + 1$ , which is not $π$ .

3.1step 2.1L3L4L5

By [L3] the ring $K$ is a field; $π$ is monic irreducible with $π (α) = 0$ , so $[K : F_{2}] = 4$ with power basis $1, α, α^{2}, α^{3}$ by [L4], and $∣ K ∣ = 2^{4} = 16$ by [L5].

4.1step 3.1given

Compute the conjugates in that basis: $α^{4} = α + 1$ by hypothesis, and $α^{8} = (α^{4})^{2} = (α + 1)^{2} = α^{2} + 1$ . So the four elements $α, α^{2}, α^{4}, α^{8}$ have coordinate lists $(0, 1, 0, 0)$ , $(0, 0, 1, 0)$ , $(1, 1, 0, 0)$ and $(1, 0, 1, 0)$ , which are pairwise different, so the four elements are pairwise distinct.

5.1step 4.1given

$α^{16} = (α^{8})^{2} = (α^{2} + 1)^{2} = α^{4} + 1 = (α + 1) + 1 = α$ , so the orbit closes after four steps.

6.1step 2.1step 4.1step 5.1L6∎

By [L6] applied to $π$ , of degree four, the elements $α, α^{2}, α^{4}, α^{8}$ are exactly the roots of $π$ and $π = (t - α) (t - α^{2}) (t - α^{4}) (t - α^{8})$ in $K [t]$ ; steps 4.1 and 5.1 verify the distinctness and the closing of the orbit directly.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

49 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.10 (standard reference, not scraped)
K. Conrad, Roots and Irreducibles (expository blurb), Theorem 5.4 (standard reference, not scraped)

The four roots of t4+t+1t4+t+1 over F2F2​ are the Frobenius powers of any one of them