ExampleConstruction: Literature-sourcedVerification: Literature-sourcedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13

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-element field $(Z / 2) [x] / (x^{2} + x + 1)$

Example

Let $F = Z / 2$ , with its quotient arithmetic (For every $n \in N$ , the congruence-class ring $Z / n$ is the quotient ring $Z / n Z$ ). This is a field (For every prime $p$ , the two operations on $Z / p$ make it a field). Then $K = F [x] / (x^{2} + x + 1) = {0, 1, a, 1 + a}, a = x + (x^{2} + x + 1),$ is a field of four elements.

Facts & Assumptions

Given: The field $F = Z / 2$ and the polynomial $x^{2} + x + 1$ .

[F1]

A quadratic over a field is irreducible exactly when 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).

[F2]

The quotient by a monic irreducible degree- $n$ polynomial is a field and has unique representatives of degree below $n$ ( $F [x] / (p)$ for monic irreducible $p$ is a field extension containing the root $x + (p)$ with unique reduced representatives).

Verification

technique · direct

1.1

The values of $x^{2} + x + 1$ at $0$ and $1$ are both $1$ in $F$ , so [F1] makes it irreducible.

F1algebra

2.1

By [F2], $K$ is a field and its unique linear representatives are exactly $0, 1, x, 1 + x$ , giving the displayed four classes.

F2step 1.1

3.1

The defining relation is $a^{2} + a + 1 = 0$ , hence $a^{2} = a + 1$ in characteristic two. Consequently $a (a + 1) = 1$ and $(a + 1)^{2} = a$ , which determines the products of the nonzero elements.

step 2.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 85 results over 16 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

T. Judson, Abstract Algebra: Theory and Applications, Extension Fields (standard reference, not scraped)

The four-element field (Z/2)[x]/(x2+x+1)(Z/2)[x]/(x2+x+1)