Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17
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.

In characteristic p, every irreducible polynomial is uniquely g(xpe) with g irreducible and separable

Statement

Let F have characteristic p>0 and let fF[x] be nonconstant and irreducible. There are unique eN and gF[x] such that

f(x)=g(xpe),

g is irreducible and separable, and e is maximal with this property. The case e=0 occurs exactly when f is separable.

Facts & Assumptions

Given: A field F of characteristic p>0 and a nonconstant irreducible polynomial fF[x].

[L1]

A nonzero polynomial is separable exactly when it is coprime to its formal derivative (A nonzero polynomial over a field is separable exactly when its gcd with its derivative is 1).

[L2]

In characteristic p, Frobenius is an injective endomorphism and (a+b)p=ap+bp (Frobenius xxp is an injective endomorphism in characteristic p, and an automorphism for finite fields).

[L3]

Every nonzero nonunit polynomial over a field factors into irreducibles (Every nonzero nonunit polynomial over a field factors into irreducible polynomials).

Proof

technique · direct
1.1

The derivative f is zero exactly when every exponent occurring in f is divisible by p; in that case there is a unique hF[x] with f(x)=h(xp). Repeating this finite descent in degree gives a unique maximal e and a polynomial g with f(x)=g(xpe) and g0.

L2algebra
2.1

If g=uv with both factors nonconstant, then f=u(xpe)v(xpe), contradicting irreducibility of f; hence g is irreducible.

step 1.1algebra
3.1

Since g0, any nonunit common divisor of g and g has an irreducible factor by [L3], which would divide the irreducible g and hence force gg, impossible by degree; thus gcd(g,g)=1 and [L1] makes g separable.

step 1.1step 2.1L1L3
4.1

The exponents occurring in f determine their largest common power pe, so e and then the coefficient-preserving core g are unique. Moreover e=0 exactly when f0, which for irreducible f is equivalent to separability by [L1].

step 1.1step 3.1L1

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 66 results over 12 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