Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07
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 in a small cyclotomic field

Example

Let ζ=ζ5 be a primitive fifth root of unity and L=Q(ζ). Then Gal(L/Q)(Z/5Z)×=C4 by σa(ζ)=ζa. For every prime p5, p is unramified and its arithmetic Frobenius is σpmod5. In particular 2 is inert, with (e,f,g)=(1,4,1).

Facts & Assumptions

Given: The data and hypotheses of the statement.

[F1]

Frobenius cycle type and prime splitting: Let FZ[T] be monic separable with splitting field L, and let p be a rational prime not dividing Disc(F). Then p is unramified in L and FˉFp[T] is squarefree. The degrees of its monic irreducible factors, with each distinct factor counted once, are exactly the cycle lengths of arithmetic Frobenius on the roots of F.

[F2]

Frobenius order is residue degree: For finite Galois L/K and nonzero Pp, the arithmetic Frobenius coset has order f(P/p) in D/I. If P is unramified, FrobP has the same order in D.

[F3]

Galois prime decomposition efg: For a finite Galois extension L/K and nonzero prime p, every P above p has the same ramification index e and residue degree f. If there are g such primes, then efg=[L:K].

[F4]

Eisenstein criterion over the integers: Let f=anxn++a0Z[x] be primitive with n1. If there is a prime p such that pan,pai for every i<n,p2a0, then f is irreducible in Q[x].

[F5]

The discriminant of a monic polynomial as the coefficient expression of Δn2: By prop-vandermonde-square-is-symmetric and thm-fundamental-theorem-of-symmetric-polynomials, there is a unique polynomial DnZ[T1,,Tn] such that Δn(x1,,xn)2=Dn(e1,,en). For a monic polynomial f(t)=tn+a1tn1++an over a commutative ring, its discriminant is Disc(f):=Dn(a1,a2,,(1)nan). Equivalently, in any algebra in which f splits with roots α1,,αn, this coefficient expression evaluates to Δn(α1,,αn)2. The definition therefore depends only on the coefficients and not on a choice or ordering of roots. For a monic constant polynomial, Disc(1)=1.

Verification

1.1

The polynomial Φ(T)=T4+T3+T2+T+1 satisfies Φ(T+1)=T4+5T3+10T2+10T+5, Eisenstein at 5. Translation preserves reducibility, so Phi is irreducible. Its four roots ζa for a=1,2,3,4 already lie in L. They give four automorphisms, with composition multiplying exponents modulo 5. The element 2 has successive powers 2,4,3,1, hence generates this group.

F4
2.1

At a root r of Phi, differentiating (T1)Φ(T)=T51 gives Φ(r)=5r4/(r1). The product over its four roots is 54/5=53: the root product is 1, and (r1)=Φ(1)=5. Pairing opposite root differences shows rΦ(r)=(1)6Disc(Φ)=Disc(Φ). Hence its discriminant is 53.

F5step 1.1
3.1

For p5 the good-reduction theorem gives unramifiedness and distinct root reductions. Frobenius sends the residue of zeta to its p-th power; since ζp is another root, distinctness forces Frob(ζ)=ζp. At p=2 that automorphism has order four, so f=4; e=1 and efg=4 then give g=1, namely inertness.

F1F2F3step 1.1step 2.1

Depends on

Used by

Dependency tree · two levels

22 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