LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16

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 prime $q$ and $d \geq 1$ , the congruence $x^{d} \equiv 1 (m o d q)$ has at most $d$ residue-class solutions

Statement

If $q$ is prime and $d \geq 1$ , then

$x^{d} \equiv 1 (m o d q)$

has at most $d$ distinct solution classes modulo $q$ .

Facts & Assumptions

Given: A prime $q$ and an integer $d \geq 1$ .

[L1]

The residue-class ring $Z / q$ is a field when $q$ is prime (For every prime $p$ , the two operations on $Z / p$ make it a field).

[L2]

Every field is a commutative ring and has no zero divisors (Every field is a commutative ring with $1 \neq 0$ ; it is an integral domain, and it is a commutative division ring).

[L3]

A nonzero polynomial of degree $d$ over an integral domain has at most $d$ roots (A nonzero polynomial of degree $n$ over an integral domain has at most $n$ distinct roots).

[L4]

Congruence modulo $q$ is equality of classes in $Z / q$ , and a root is an element at which polynomial evaluation is zero (The congruence class $[a]_{n}$ and the quotient set $Z / n$ , Evaluation and roots of a polynomial in a commutative target ring).

Proof

technique · direct

1.1

By [L1] and [L2], $Z / q$ is an integral domain. The polynomial $f (X) = X^{d} - 1$ over this domain is nonzero and has degree $d$ .

L1L2algebra

2.1

By [L4], the solution classes of the congruence are exactly the roots of $f$ in $Z / q$ . The bound [L3] therefore gives at most $d$ such classes.

step 1.1L3L4∎

Depends on

Used by

For primes p<q, nontrivial actions of Cₚ on C_q exist exactly when p∣(q-1) and are unique up to automorphisms Lemma

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 75 results over 20 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Peter Hackman, Elementary Number Theory, Chapter C (standard reference, not scraped)

For prime qq and d≥1d≥1, the congruence xd≡1(modq)xd≡1(modq) has at most dd residue-class solutions