Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24
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.

A positive-degree separable polynomial is irreducible exactly when its Galois group is transitive on the roots

Statement

A positive-degree separable polynomial is irreducible if and only if its Galois group acts transitively on its roots.

Facts & Assumptions

Given: A positive-degree separable polynomial f∈F[x], its splitting field L, and the faithful root action of A polynomial Galois group acts faithfully on its roots; the minimal-polynomial correspondence for a simple algebraic extension (The evaluation kernel and the unique monic irreducible minimal polynomial of an algebraic element).

[L1]

An isomorphism between base fields taking one polynomial to another extends to an isomorphism between their splitting fields (A base-field isomorphism extends to an isomorphism between splitting fields of corresponding polynomials).

Proof

technique · direct
1.1L1givenchoose

For the forward direction, suppose f is irreducible and let α,β be roots. The rule sending α to β gives an F-isomorphism F(α)→F(β) because both have minimal polynomial associated to f; by [L1] it extends to an F-automorphism of L. Thus some Galois element sends any chosen root to any other, so the action is transitive. This includes degree one.

2.1givenalgebra∎

For the reverse direction, suppose the action is transitive and let g be a monic irreducible factor of f containing one root α. For every σ∈Gf, the coefficients of g are fixed, so g(σα)=σ(g(α))=0. Transitivity puts every root of f among the roots of g; since f is separable, g has the full degree of f, so f is a scalar multiple of g and is irreducible. A root equal to zero causes no exception.

Depends on

Used by

Dependency tree · two levels

14 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