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

Shor factoring preprocessing and retry branches

Example

The following exact inputs exercise the early return and retry branches of Shor factoring with verified output and bounded outer retries: the even input $14$ , the perfect power $81 = 3^{4}$ , the nonunit choice $a = 5$ for $N = 15$ , and the unit samples $(N, a) = (35, 11)$ and $(15, 14)$ . For these two retry executions, take the order-finding subroutine to return candidate $q = 3$ for $(35, 11)$ and candidate $q = 2$ for $(15, 14)$ .

Facts & Assumptions

Given: The stated Shor algorithm, the displayed residue samples, and the chosen order-finding candidate outputs $q = 3$ for $(N, a) = (35, 11)$ and $q = 2$ for $(N, a) = (15, 14)$ .

[F1]

The even precheck returns $2$ for even composite $N \geq 4$ . When the root-search branch is reached on a perfect-power input, it detects an exact representation $N = c^{e}$ with $c \geq 2$ and $e \geq 2$ , and returns that representation's base $c$ as a proper factor (Shor factoring with verified output and bounded outer retries, Even and perfect-power preprocessing returns a proper factor).

[F2]

A nonunit sample in ${1, \dots, N - 1}$ gives a proper gcd factor; conditional on gcd one, it is a unit (Random residue gcd branch for factoring, For $n \geq 1$ , $[a]_{n}$ is a unit if and only if $\gcd (a, n) = 1$ ).

[F3]

A period candidate is continued only when it is even, between $2$ and $N$ , and passes $a^{q} \equiv 1 (m o d N)$ ; the half-power gcds are returned only after the strict divisor checks (Shor factoring with verified output and bounded outer retries, Order-to-factor output correctness).

[F4]

Modular powers and gcds here are computed by integer multiplication, congruence and common-divisor calculations (The congruence class $[a]_{n}$ and the quotient set $Z / n$ , For every natural $n$ , $(Z / n, +)$ is an abelian group, multiplication is a commutative monoid operation, and both distributive laws hold, Powers $g^{n}$ : natural exponents in a monoid and integer exponents in a group, with $g^{0} = e$ , Common divisor, and the greatest common divisor $\gcd (a, b)$ , with the convention $\gcd (0, 0) : = 0$ , Divisibility in $Z$ : $d ∣ a$ when $a = d q$ for some integer $q$ ).

Verification

1.1givenF1algebra

For $N = 14$ , the even branch checks $1 < 2 < 14$ and $14 m o d 2 = 0$ , so it returns the proper factor $2$ before sampling. For $N = 81$ , the root search starts at $e = 2$ and finds $9^{2} = 81$ ; since $1 < 9 < 81$ , that branch returns $9$ . The alternative representation $81 = 3^{4}$ is not reached after this earlier return.

1.2givenF2F4algebra

For $N = 15$ and sample $a = 5$ , $\gcd (5, 15) = 5$ , which is strictly between $1$ and $15$ and divides $15$ ; the nonunit branch returns $5$ without order finding.

1.3givenF3F4algebra

For $N = 35$ and $a = 11$ , $\gcd (11, 35) = 1$ . The powers satisfy $11^{1} \equiv 11$ , $11^{2} \equiv 16$ , and $11^{3} \equiv 1 (m o d 35)$ , so the true order is $3$ , agreeing with the chosen candidate $q = 3$ . This candidate is odd and therefore fails the algorithm's even-period check; this attempt continues.

2.1givenF3F4algebra∎

For $N = 15$ and $a = 14$ , $\gcd (14, 15) = 1$ and $14^{2} \equiv 1 (m o d 15)$ while $14 \equiv̸ 1$ , so the true order is $2$ , agreeing with the chosen candidate $q = 2$ . The half-power is $z = 14 \equiv - 1 (m o d 15)$ , giving $\gcd (z - 1, 15) = \gcd (13, 15) = 1$ and $\gcd (z + 1, 15) = \gcd (15, 15) = 15$ . Neither passes the strict check, so the algorithm continues.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

53 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)