ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-16

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.

Frobenius on $F_{4}$ swaps the two non-prime-field elements

Example

In $F_{4} = F_{2} [t] / (t^{2} + t + 1)$ , with $a$ the class of $t$ , Frobenius fixes $0, 1$ , sends $a$ to $a + 1$ , and sends $a + 1$ to $a$ . Its square is the identity.

Facts & Assumptions

Given: The quotient description of $F_{4}$ and the class $a$ .

[L1]

In characteristic $2$ , Frobenius $x \mapsto x^{2}$ is an injective field endomorphism, and it is an automorphism when the field is finite; its second iterate is $x \mapsto x^{4}$ (Frobenius $x \mapsto x^{p}$ is an injective endomorphism in characteristic $p$ , and an automorphism for finite fields).

[L2]

The quotient by an irreducible polynomial over a field 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]

The ring $Z / 2$ is a field (For every prime $p$ , the two operations on $Z / p$ make it a field).

Verification

technique · direct

1.1givenL2L3

The modulus has no root in $F_{2}$ , so [L2] and [L3] give the field with relation $a^{2} = a + 1$ .

2.1step 1.1L1algebra

Squaring gives $0^{2} = 0$ , $1^{2} = 1$ , $a^{2} = a + 1$ , and $(a + 1)^{2} = a^{2} + 1 = a$ .

3.1step 2.1L1∎

Thus Frobenius swaps the two non-prime-field elements and fixes the prime field. Applying the swap twice is the identity, agreeing with $x^{4} = x$ from [L1].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

21 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, Section 1 (standard reference, not scraped)

Frobenius on F4F4​ swaps the two non-prime-field elements