ExampleConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-26

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.

$Φ_{1}$ through $Φ_{12}$ computed from the divisor recursion

Example

Running the recursion of The cyclotomic polynomials $Φ_{n} \in Z [t]$ , defined by $\prod_{d ∣ n} Φ_{d} = t^{n} - 1$ gives

$\begin{aligned} Φ_{1} & = t - 1, & Φ_{2} & = t + 1, & Φ_{3} & = t^{2} + t + 1, \\ Φ_{4} & = t^{2} + 1, & Φ_{5} & = t^{4} + t^{3} + t^{2} + t + 1, & Φ_{6} & = t^{2} - t + 1, \\ Φ_{7} & = t^{6} + t^{5} + t^{4} + t^{3} + t^{2} + t + 1, & Φ_{8} & = t^{4} + 1, & Φ_{9} & = t^{6} + t^{3} + 1, \\ Φ_{10} & = t^{4} - t^{3} + t^{2} - t + 1, & Φ_{11} & = \sum_{k = 0}^{10} t^{k}, & Φ_{12} & = t^{4} - t^{2} + 1, \end{aligned}$

each monic in $Z [t]$ , with degrees

$1, 1, 2, 2, 4, 2, 6, 4, 6, 4, 10, 4$

matching $φ (1), \dots, φ (12)$ (The unit group $(Z / n)^{\times}$ and Euler's totient $φ (n) = ∣ (Z / n)^{\times} ∣$ for $n \geq 1$ ).

Facts & Assumptions

Given: The recursion $Φ_{1} = t - 1$ and $Φ_{n} = (t^{n} - 1) / \prod_{d ∣ n, d < n} Φ_{d}$ (The cyclotomic polynomials $Φ_{n} \in Z [t]$ , defined by $\prod_{d ∣ n} Φ_{d} = t^{n} - 1$ , The sum $\sum_{i \in S} a_{i}$ over a finite index set, and its product form, Divisibility in $Z$ : $d ∣ a$ when $a = d q$ for some integer $q$ ); and the elementary identity $(t^{a} - 1) (t^{a (b - 1)} + \dots + t^{a} + 1) = t^{a b} - 1$ for $a, b \geq 1$ .

[L1]

For every $n \geq 1$ , $Φ_{n}$ is monic in $Z [t]$ with $\prod_{d ∣ n} Φ_{d} = t^{n} - 1$ and $\deg Φ_{n} = φ (n)$ (The recursion defines a unique monic $Φ_{n} \in Z [t]$ , of degree $φ (n)$ , Degree, leading coefficient and monic polynomial, with the zero polynomial having no degree).

[L2]

For a prime $p$ and $r \geq 1$ , $Φ_{p^{r}} = \sum_{k = 0}^{p - 1} t^{k p^{r - 1}}$ ( $Φ_{p^{r}} (t) = \sum_{k < p} t^{k p^{r - 1}}$ , and $Φ_{p^{r}} (t + 1)$ is Eisenstein at $p$ ).

[L3]

$Z [t]$ is an integral domain (A polynomial ring over an integral domain is an integral domain), so a nonzero factor may be cancelled; and division by a monic polynomial has a unique quotient and remainder (Division by a monic polynomial over a commutative ring).

[L4]

$φ (1) = 1$ and $φ (p) = p - 1$ for a prime $p$ ( $φ (1) = 1$ , and $φ (p) = p - 1$ for every prime $p$ ); $φ (p^{k}) = p^{k} - p^{k - 1}$ (For a prime $p$ and $k \geq 1$ , $φ (p^{k}) = p^{k} - p^{k - 1}$ ); and for $n \geq 1$ with prime divisors $p_{0}, \dots, p_{r - 1}$ and $k_{i} = v_{p_{i}} (n)$ , $φ (n) = \prod_{i < r} (p_{i}^{k_{i}} - p_{i}^{k_{i} - 1})$ (Euler's product formula $φ (n) = n \prod_{p ∣ n} (1 - 1 / p) = \prod_{p^{k} ∥ n} (p^{k} - p^{k - 1})$ for $n \geq 1$ , stated through a finite injective list of its prime divisors).

Verification

technique · direct

1.1

$Φ_{1} = t - 1$ is the base clause of the recursion, of degree $1 = φ (1)$ by [L4].

L4given

1.2

The prime powers among $2, \dots, 12$ are $2, 3, 4, 5, 7, 8, 9, 11$ , and [L2] gives their cyclotomic polynomials directly: $Φ_{2} = 1 + t$ , $Φ_{3} = 1 + t + t^{2}$ , $Φ_{4} = 1 + t^{2}$ , $Φ_{5} = 1 + t + t^{2} + t^{3} + t^{4}$ , $Φ_{7} = \sum_{k = 0}^{6} t^{k}$ , $Φ_{8} = 1 + t^{4}$ , $Φ_{9} = 1 + t^{3} + t^{6}$ and $Φ_{11} = \sum_{k = 0}^{10} t^{k}$ .

2.1

For $n = 6$ : the positive divisors of $6$ are $1, 2, 3, 6$ and those of $3$ are $1, 3$ , so [L1] gives $Φ_{1} Φ_{2} Φ_{3} Φ_{6} = t^{6} - 1$ and $Φ_{1} Φ_{3} = t^{3} - 1$ ; dividing and using the given identity with $a = 3$ , $b = 2$ yields $Φ_{2} Φ_{6} = (t^{6} - 1) / (t^{3} - 1) = t^{3} + 1$ . Since $(t + 1) (t^{2} - t + 1) = t^{3} + 1$ and $Φ_{2} = t + 1$ is nonzero, cancelling in $Z [t]$ by [L3] gives $Φ_{6} = t^{2} - t + 1$ .

step 1.2L1L3given

2.2

For $n = 10$ : the divisors of $10$ are $1, 2, 5, 10$ and those of $5$ are $1, 5$ , so $Φ_{2} Φ_{10} = (t^{10} - 1) / (t^{5} - 1) = t^{5} + 1$ by [L1] and the given identity with $a = 5$ , $b = 2$ ; and $(t + 1) (t^{4} - t^{3} + t^{2} - t + 1) = t^{5} + 1$ , so cancelling gives $Φ_{10} = t^{4} - t^{3} + t^{2} - t + 1$ .

step 1.2L1L3given

3.1

For $n = 12$ : the divisors of $12$ are $1, 2, 3, 4, 6, 12$ and those of $6$ are $1, 2, 3, 6$ , so $Φ_{4} Φ_{12} = (t^{12} - 1) / (t^{6} - 1) = t^{6} + 1$ by [L1] and the given identity with $a = 6$ , $b = 2$ ; and $(t^{2} + 1) (t^{4} - t^{2} + 1) = t^{6} + 1$ with $Φ_{4} = t^{2} + 1$ , so cancelling gives $Φ_{12} = t^{4} - t^{2} + 1$ .

step 1.2step 2.1L1L3given

4.1

The degrees read off the displayed polynomials are $1, 1, 2, 2, 4, 2, 6, 4, 6, 4, 10, 4$ . By [L4] these are $φ (1) = 1$ , $φ (2) = 1$ , $φ (3) = 2$ , $φ (4) = 2^{2} - 2 = 2$ , $φ (5) = 4$ , $φ (6) = (2 - 1) (3 - 1) = 2$ , $φ (7) = 6$ , $φ (8) = 2^{3} - 2^{2} = 4$ , $φ (9) = 3^{2} - 3 = 6$ , $φ (10) = (2 - 1) (5 - 1) = 4$ , $φ (11) = 10$ and $φ (12) = (2^{2} - 2) (3 - 1) = 4$ , so every degree matches [L1].

step 1.1step 1.2step 2.1step 2.2step 3.1L1L4∎

Remarks

Every division in the recursion is exact and stays over $Z$ . That is not visible from the table and is not a coincidence of small $n$ : it is The recursion defines a unique monic $Φ_{n} \in Z [t]$ , of degree $φ (n)$ , and it is what makes the recursion a definition rather than a computation that might fail.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

78 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

K. Conrad, Cyclotomic Extensions (expository blurb), Example 5.1 (standard reference, not scraped)
P. L. Clark, Field Theory (course notes/monograph), Section 9.1.2 (standard reference, not scraped)

Φ1Φ1​ through Φ12Φ12​ computed from the divisor recursion