ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedaudited 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.

A cyclotomic different preview

Example

For a prime $p$ and $K = Q (ζ_{p})$ , $D_{K} = (1 - ζ_{p})^{p - 2}$ .

Verification

Given: $O_{K} = Z [ζ_{p}]$ and $Φ_{p} (X) = 1 + \dots + X^{p - 1}$ .

1.1

At $r = 1$ , $Φ_{p^{r}} (t) = \sum_{k < p} t^{k p^{r - 1}}$ , and $Φ_{p^{r}} (t + 1)$ is Eisenstein at $p$ makes $Φ_{p}$ irreducible over $Q$ . Since it is monic and vanishes at the primitive root $ζ_{p}$ , it is its minimal polynomial. The monogenic formula gives $D_{K} = (Φ_{p}^{'} (ζ_{p}))$ .

givenalgebra

2.1

For $p = 2$ the claim is immediate. For odd $p$ , differentiating the factorisation of $Φ_{p}$ into its roots gives $Φ_{p}^{'} (ζ_{p}) = \prod_{j = 2}^{p - 1} (ζ_{p} - ζ_{p}^{j}) = ζ_{p}^{p - 2} \prod_{k = 1}^{p - 2} (1 - ζ_{p}^{k}) .$ For $1 \leq k \leq p - 2$ , the quotient $(1 - ζ_{p}^{k}) / (1 - ζ_{p}) = 1 + ζ_{p} + \dots + ζ_{p}^{k - 1}$ is a unit: if $k ℓ \equiv 1 (m o d p)$ , the reverse quotient is likewise a cyclotomic integer. Since $ζ_{p}$ is also a unit, the displayed product generates the ideal $(1 - ζ_{p})^{p - 2}$ .

step 1.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

29 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

Keith Conrad, The Different Ideal, Examples 4.5--4.6 (standard reference, not scraped)