LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generatedjudge pass (gpt-6-luna)

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.

Random residue gcd branch for factoring

Statement

Let $N \geq 2$ and choose $a$ uniformly from the integers $1, \dots, N - 1$ . If $\gcd (a, N) > 1$ , then $\gcd (a, N)$ is a proper factor of $N$ . Conditional on $\gcd (a, N) = 1$ , the residue class $[a]_{N}$ is uniformly distributed in the unit group $(Z / N)^{\times}$ .

Facts & Assumptions

Given: An integer $N \geq 2$ and the uniform finite sample space $Ω_{N} = {1, \dots, N - 1}$ .

[F1]

Each residue class modulo $N$ has a unique standard representative in ${0, \dots, N - 1}$ (For $n \geq 1$ , every class in $Z / n$ has one representative $r$ with $0 \leq r < n$ , so $∣ Z / n ∣ = n$ ; while $Z / 0$ is in bijection with $Z$ , The congruence class $[a]_{n}$ and the quotient set $Z / n$ ).

[F2]

A residue $[a]_{N}$ is a unit exactly when $\gcd (a, N) = 1$ (For $n \geq 1$ , $[a]_{n}$ is a unit if and only if $\gcd (a, n) = 1$ , The unit group $(Z / n)^{\times}$ and Euler's totient $φ (n) = ∣ (Z / n)^{\times} ∣$ for $n \geq 1$ ).

[F3]

In a finite uniform probability space, each outcome has equal weight; event probability is the sum of those weights (Finite probability spaces, outcome weights, events, and event probabilities), and $P (A ∣ B) = P (A \cap B) / P (B)$ when $P (B) > 0$ (Conditional probability $P (A ∣ B)$ for $P (B) > 0$ ).

[F4]

The gcd is a positive common divisor and is greatest in the usual order (Common divisor, and the greatest common divisor $\gcd (a, b)$ , with the convention $\gcd (0, 0) : = 0$ ); $\gcd (0, N) = N$ for $N \geq 1$ ( $\gcd$ is symmetric and unchanged by signs: $\gcd (a, b) = \gcd (b, a) = \gcd (∣ a ∣, ∣ b ∣)$ ; moreover $\gcd (a, 0) = ∣ a ∣$ , $\gcd (a, 1) = 1$ , $\gcd (a, a) = ∣ a ∣$ , and $\gcd (a, b) \geq 1$ unless $a = b = 0$ ).

[F5]

If $d ∣ a$ and $a \neq 0$ , then $∣ d ∣ \leq ∣ a ∣$ (If $d ∣ a$ and $a \neq 0$ then $d \neq 0$ and $∣ d ∣ \leq ∣ a ∣$ ; hence the set of divisors of a nonzero integer is bounded above by $∣ a ∣$ ).

Proof

1.1givenF4F5algebra

If $g = \gcd (a, N) > 1$ , then $g ∣ a$ and $g ∣ N$ by [F4]. Since $g$ is positive and divides the nonzero $a$ , [F5] gives $g \leq a < N$ ; hence $1 < g < N$ and $g$ is a proper factor.

1.2givenF1F2F4choose

The event $U = {a \in Ω_{N} : \gcd (a, N) = 1}$ is nonempty because $a = 1$ belongs to it. By [F1] and [F2], the map $a \mapsto [a]_{N}$ is a bijection from $U$ to $(Z / N)^{\times}$ : every unit has its unique standard representative, and the zero class is not a unit because [F2] and [F4] give $\gcd (0, N) = N \neq 1$ .

2.1step 1.2F3algebra

Every $a \in U$ has probability $1 / (N - 1)$ , so $P (U) = ∣ U ∣ / (N - 1) > 0$ . For any fixed unit representative $a \in U$ , its conditional probability is $(1 / (N - 1)) / P (U) = 1 / ∣ U ∣$ . By [F2], this is the uniform law on the unit group.

3.1step 1.1step 2.1∎

Step 1.1 proves the immediate proper-factor branch, and step 2.1 proves conditional uniformity of the unit branch.

Depends on

Used by

Shor factoring preprocessing and retry branches Example
Bounded-error success of Shor factoring Theorem
Order-to-factor output correctness Theorem

Dependency tree · two levels

41 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

Peter W. Shor, Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer (standard reference, not scraped)
Ronald de Wolf, Quantum Computing: Lecture Notes (standard reference, not scraped)