ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 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.

Fourth and eighth powers modulo $17$

Example

The nonzero fourth powers modulo $17$ are $1, 4, 13, 16$ , and the nonzero eighth powers are $1, 16$ . Each fourth-power target has four fourth roots, and each eighth-power target has eight eighth roots.

Facts & Assumptions

Given: The prime modulus $17$ and nonzero target classes.

[L1]

If $n \geq 1$ admits a primitive root, $\gcd (a, n) = 1$ , $m \geq 1$ , and $d = \gcd (m, φ (n))$ , then $x^{m} \equiv a (m o d n)$ is soluble exactly when $a^{φ (n) / d} \equiv 1 (m o d n)$ (Euler's criterion: if $n$ has a primitive root, $\gcd (a, n) = 1$ , and $m \geq 1$ , then $x^{m} \equiv a (m o d n)$ is solvable if and only if $a^{φ (n) / \gcd (φ (n), m)} \equiv 1 (m o d n)$ ).

[L2]

Every prime admits a primitive root modulo that prime (Every prime modulus admits a primitive root).

[L3]

For every prime $p$ , $φ (p) = p - 1$ ( $φ (1) = 1$ , and $φ (p) = p - 1$ for every prime $p$ ).

[L4]

Under the hypotheses of [L1], a soluble congruence $x^{m} \equiv a (m o d n)$ has exactly $\gcd (φ (n), m)$ solution classes (If $n$ has a primitive root, $\gcd (a, n) = 1$ , $m \geq 1$ , and $x^{m} \equiv a (m o d n)$ is solvable, then it has exactly $\gcd (φ (n), m)$ solution classes modulo $n$ ).

[L5]

If $p ∤ a$ , then $p$ and $a$ are coprime (For a prime $p$ and any integer $a$ , $\gcd (p, a)$ is $p$ when $p ∣ a$ and $1$ otherwise; so $p ∤ a$ makes $p$ and $a$ coprime).

Verification

technique · direct

1.1

By [L2], $17$ admits a primitive root, [L3] gives $φ (17) = 16$ , and [L5] supplies the coprimality of every nonzero target. Thus [L1] says that a target is a fourth power exactly when its fourth power is $1$ , and an eighth power exactly when its square is $1$ .

L1L2L3L5given

2.1

Direct reduction gives the fourth-power values $1^{4} = 4^{4} = 13^{4} = 16^{4} \equiv 1$ , $2^{4} = 8^{4} = 9^{4} = 15^{4} \equiv 16$ , $3^{4} = 5^{4} = 12^{4} = 14^{4} \equiv 13$ , and $6^{4} = 7^{4} = 10^{4} = 11^{4} \equiv 4$ . Squaring the unit classes shows that the targets satisfying $a^{2} \equiv 1$ are exactly $1, 16$ . These lists agree with both directions of the tests in [L1].

L1step 1.1algebra

3.1

Fact [L4] gives $\gcd (16, 4) = 4$ roots for each fourth-power target and $\gcd (16, 8) = 8$ roots for each eighth-power target.

L3L4step 2.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 85 results over 22 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

A. Gorodnik, Number Theory, Lecture 9, Example 1.3 (standard reference, not scraped)

Fourth and eighth powers modulo 1717