ExampleConstruction: AI-adaptedVerification: 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.

$2$ is primitive modulo every power of $5$

Example

For every $k \geq 1$ , the class of $2$ is a primitive root modulo $5^{k}$ .

Facts & Assumptions

Given: The integer $2$ and powers of the odd prime $5$ .

[L1]

For an odd prime $p$ , an integer $u$ with $p ∤ u$ , and $k \geq 1$ , the class of $1 + p u$ has order $p^{k - 1}$ modulo $p^{k}$ (For odd prime $p$ , $p ∤ u$ , and $k \geq 1$ , the class of $1 + p u$ has order $p^{k - 1}$ modulo $p^{k}$ ).

[L2]

If an element has order $r$ , then its fourth power has order $r / \gcd (r, 4)$ (In a cyclic group of order $m$ , $g^{a}$ has order $m / \gcd (a, m)$ ).

[L3]

An element of order $r$ has its $t$ th power equal to the identity exactly when $r ∣ t$ (If $ord (g) = n$ then $g^{k} = e$ iff $k$ is an integer multiple of $n$ , the powers $g^{0}, \dots, g^{n - 1}$ are distinct, and $⟨ g ⟩$ has exactly $n$ elements; if $g$ has infinite order then $g^{j} = g^{k}$ only for $j = k$ ).

[L4]

$φ (5^{k}) = 4 \cdot 5^{k - 1}$ (For a prime $p$ and $k \geq 1$ , $φ (p^{k}) = p^{k} - p^{k - 1}$ ).

[L5]

A class modulo $n$ is a unit exactly when its representative is coprime to $n$ , and a primitive root is a unit of order $φ (n)$ (For $n \geq 1$ , $[a]_{n}$ is a unit if and only if $\gcd (a, n) = 1$ , Primitive roots modulo $n$ ).

Verification

technique · direct

1.1

Modulo $5$ , $2^{1}, 2^{2}, 2^{3}, 2^{4}$ are $2, 4, 3, 1$ , so $2$ has order $4$ . This settles $k = 1$ .

L3L4L5algebra

1.2

Let $k \geq 2$ and let $r$ be the order of $2$ modulo $5^{k}$ . Since $2^{4} = 1 + 5 \cdot 3$ , [L1] says that $2^{4}$ has order $5^{k - 1}$ . Hence [L2] gives $r / \gcd (r, 4) = 5^{k - 1}$ .

L1L2

2.1

Reduction modulo $5$ and step 1.1 show that $4 ∣ r$ by [L3]. Therefore $\gcd (r, 4) = 4$ , and step 1.2 yields $r = 4 \cdot 5^{k - 1} = φ (5^{k})$ by [L4]. Since $2$ is a unit by [L5], it is primitive by the definition in [L5].

step 1.1step 1.2L3L4L5∎

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: 115 results over 25 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

William Stein, Elementary Number Theory, Theorem 2.5.11 (standard reference, not scraped)

22 is primitive modulo every power of 55