Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

For a monic separable polynomial in characteristic not two, the Galois group lies in An exactly when the discriminant is a square

Statement

Let fF[x] be a monic separable polynomial of degree n, where charF2. The Galois group lies in An exactly when the discriminant is a square in the base field.

Facts & Assumptions

Given: A splitting field L/F, an ordered root list, the discriminant definition of The discriminant of a monic polynomial as the coefficient expression of Δn2, the root formula Disc(f)=δ2 and the fact that separability makes it nonzero (The discriminant is i<j(αiαj)2 and vanishes exactly when a monic polynomial has a repeated root), the definition An=ker(sgn) (The alternating group An=ker(sgn) of even permutations), and the finite Galois correspondence, which gives LGal(L/F)=F (The fundamental theorem of finite Galois theory).

[L1]

For the Vandermonde product, σ(δ)=sgn(σ)δ for every Galois automorphism (The Vandermonde product transforms by the sign of the root permutation).

Proof

technique · direct
1.1

For the forward direction, suppose the Galois group lies in An. Then every sign is 1, so [L1] shows that every automorphism fixes δ. The fixed field is F, hence δF and Disc(f)=δ2 is a square in F. This also covers n=0 and n=1, when δ=1.

L1given
2.1

For the reverse direction, suppose Disc(f)=d2 for some dF. Since δ2=d2, the field law gives δ=d or δ=d, so δF. Thus every automorphism fixes δ, and [L1] gives sgn(σ)δ=δ. Separability gives δ0, so cancellation and 11 in characteristic not two force sgn(σ)=1. Therefore every Galois permutation lies in An.

L1givenalgebra

Remarks

The characteristic hypothesis is essential to this argument: in characteristic two the two signs have the same scalar action, so the Vandermonde equation cannot detect parity.

Depends on

Used by

Dependency tree · two levels

25 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