Alphabeta Math
CorollaryStatement: 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.

A coprime exponent gives a unique nonzero k-th root modulo a prime

Statement

Let p be prime, let k1, and let aZ satisfy pa and gcd(k,p1)=1. Then xka(modp) has a unique nonzero solution class. If 0 and

k1(modp1),

then that class is [a]p; the formula is independent of the chosen nonnegative representative of the inverse class.

Facts & Assumptions

Given: A prime p, an integer k1, and aZ with pa and gcd(k,p1)=1.

[L1]

If n1 admits a primitive root, gcd(a,n)=1, m1, and d=gcd(m,φ(n)), then xma(modn) is solvable if and only if aφ(n)/d1(modn) (Euler's criterion: if n has a primitive root, gcd(a,n)=1, and m1, then xma(modn) is solvable if and only if aφ(n)/gcd(φ(n),m)1(modn)).

[L2]

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

[L3]

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

[L4]

Under the hypotheses of [L1], a soluble congruence xma(modn) has exactly gcd(φ(n),m) solution classes (If n has a primitive root, gcd(a,n)=1, m1, and xma(modn) is solvable, then it has exactly gcd(φ(n),m) solution classes modulo n).

[L5]

For u,vZ and n1, the congruence uyv(modn) is soluble exactly when gcd(u,n) divides v, and then it has exactly gcd(u,n) solution classes (For n1, axb(modn) is solvable exactly when gcd(a,n)b, and then has exactly gcd(a,n) solution classes modulo n).

Proof

technique · direct
1.1

By [L7], gcd(a,p)=1. Facts [L2] and [L3] specialise [L1] to modulus p, while gcd(k,p1)=1 reduces its test to ap11(modp), which holds by [L6]. Thus the root congruence is soluble.

L1L2L3L6L7given
2.1

Applying [L4] with n=p and m=k gives exactly gcd(p1,k)=1 solution class, so the root is unique. It is nonzero because a zero root would give xk0(modp), contrary to pa.

L2L3L4step 1.1given
3.1

By [L5], the congruence k1(modp1) has one solution class and has nonnegative representatives. If p=2, every such a is odd, so it represents the sole unit class and hence the unique root from step 2.1. Suppose p is odd. For a nonnegative representative , the congruence forces >0, so k=1+t(p1) with t0; then [L6] gives (a)k=a1+t(p1)a(modp). Two nonnegative representatives differ by a multiple of p1; ordering them and applying [L6] to the nonnegative difference shows that their powers of a represent the same class.

L5L6L7step 2.1algebra

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 98 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