ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck 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 a primitive root modulo $13$ by testing the prime divisors of $12$

Example

The class of $2$ is a primitive root modulo $13$ .

Facts & Assumptions

Given: The prime modulus $13$ and the unit class of $2$ .

[L1]

A unit is a primitive root modulo $n$ when its order is $φ (n)$ (Primitive roots modulo $n$ ).

[L2]

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

[L3]

If an element has finite order $r$ , its powers equal the identity exactly at exponents divisible by $r$ (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$ ).

Verification

technique · direct

1.1algebra

Direct calculation gives $2^{4} \equiv 3 \equiv̸ 1$ and $2^{6} \equiv - 1 \equiv̸ 1 (m o d 13)$ ; in particular $2^{12} \equiv 1 (m o d 13)$ .

2.1step 1.1L1L2L3∎

By step 1.1 and [L3], the order divides $12$ . Every proper divisor of $12$ divides either $12 / 2 = 6$ or $12 / 3 = 4$ , so step 1.1 and [L3] exclude every proper divisor. The order is therefore $12 = φ (13)$ by [L2], and [L1] makes $2$ primitive.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

30 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

William Stein, Elementary Number Theory, Example 2.5.9 (standard reference, not scraped)

22 is a primitive root modulo 1313 by testing the prime divisors of 1212