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 be a primitive fifth root of unity and . Then by . For every prime , p is unramified and its arithmetic Frobenius is . In particular 2 is inert, with .
Facts & Assumptions
Given: The data and hypotheses of the statement.
Frobenius cycle type and prime splitting: Let be monic separable with splitting field L, and let p be a rational prime not dividing . Then p is unramified in L and 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.
Frobenius order is residue degree: For finite Galois L/K and nonzero , the arithmetic Frobenius coset has order in D/I. If P is unramified, has the same order in D.
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 .
Eisenstein criterion over the integers: Let be primitive with . If there is a prime such that then is irreducible in .
The discriminant of a monic polynomial as the coefficient expression of : By prop-vandermonde-square-is-symmetric and thm-fundamental-theorem-of-symmetric-polynomials, there is a unique polynomial such that For a monic polynomial over a commutative ring, its discriminant is Equivalently, in any algebra in which splits with roots , this coefficient expression evaluates to . The definition therefore depends only on the coefficients and not on a choice or ordering of roots. For a monic constant polynomial, .
Verification
The polynomial satisfies , Eisenstein at 5. Translation preserves reducibility, so Phi is irreducible. Its four roots 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.
At a root r of Phi, differentiating gives . The product over its four roots is : the root product is 1, and . Pairing opposite root differences shows . Hence its discriminant is .
For the good-reduction theorem gives unramifiedness and distinct root reductions. Frobenius sends the residue of zeta to its p-th power; since is another root, distinctness forces . At p=2 that automorphism has order four, so f=4; e=1 and efg=4 then give g=1, namely inertness.
Depends on
Used by
- Decomposition groups in a tower Example
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
- Chapter 8, Example 8.18, p.143 (standard reference, not scraped)