Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (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.

Over Fp(t), the polynomial xpxt gives a cyclic Artin-Schreier extension

Example

Let F=Fp(t). Then the polynomial

xpxt

is irreducible over F, and for any root α the extension F(α)/F is cyclic of degree p. Its full root set is

α, α+1, , α+(p1).

Facts & Assumptions

Given: The rational function field F=Fp(t) and the polynomial xpxt.

[L2]

In characteristic p, a degree-p extension is cyclic exactly when it is generated by a root of an irreducible polynomial xpxa (In characteristic p, a degree-p extension is cyclic exactly when it is generated by a root of xpxa with aF and that polynomial irreducible).

[L3]

A finite extension is Galois when it is the splitting field of a separable polynomial, and then the order of its Galois group equals its degree (Equivalent characterizations of a finite Galois extension).

Verification

technique · direct
1.1

Suppose t=bpb for some bFp(t). Write b=u/v in lowest terms. At the pole t=, if b has pole order m>0 then bpb has pole order pm, a multiple of p; if b has no pole there, neither does bpb. Both alternatives contradict the simple pole of t at infinity. Therefore no such b exists.

L1algebra
2.1

Let α be a root in an algebraic closure and let mα have degree d over F. Every conjugate of α is a root of xpxt, hence has the form α+i with iFp and therefore lies in F(α). The polynomial mα thus splits in F(α), and it is separable because it divides a polynomial with derivative 1. By [L3], F(α)/F is Galois. Its automorphisms inject into the additive group of Fp by σ(α)=α+i, so d is 1 or p. Step 1.1 excludes d=1, hence d=p and mα=xpxt. Thus this polynomial is irreducible.

L3step 1.1algebra
3.1

Now [L2] makes F(α)/F cyclic of degree p. Its full root set is α+i for iFp, since (α+i)p(α+i)=αpα=t.

L2step 2.1algebra

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

20 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