LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-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.

Certified capped norm attempts succeed on prime residuals

Statement

Let $u$ be a grid candidate of least denominator exponent $k$ , and put $ξ = 1 - u^{†} u$ , $ξ^{∙} ξ = n / 2^{ℓ}$ in reduced form. Let $P (k) = 2^{200} (k + 1)^{20}$ be the calibrated prime-input binary-work bound of Efficient exact cyclotomic norm solving with a supplied integer factorization. The capped prime-attempt procedure in Cyclotomic scaled grid and norm-equation solver, with solver budget $2 ⌈ P (k) ⌉$ , has the following properties:

Every accepted output is an exact solution $t^{†} t = ξ$ .
On every input its work is polynomial in $k + 1$ , including the final exact verification, with no primality promise on $n$ .
When $n$ is prime, its success probability is at least $1 / 2$ . When $n \in {0, 1}$ , the explicitly complete zero/unit branches succeed.

For a candidate stream with exponent profile $k_{j}$ , suppose its arithmetic data are given an idealized stochastic model in which the indicators $I_{j}$ of prime or zero/unit norm numerators are independent, with $p_{j} = \Pr (I_{j} = 1) \geq c / (k_{j} + 1)$ . Draw fresh independent solver bits, independently of all arithmetic data. If $J$ is the first successful call, then $\Pr (J > j) \leq \prod_{i = 1}^{j} (1 - p_{i} / 2) \leq \prod_{i = 1}^{j} (1 - \frac{c}{2 (k_{i} + 1)}) .$ Thus these attempts have the same stopping-tail bound as independent events with probabilities $c / (2 (k_{j} + 1))$ . Independence of the actual successful-call events is not asserted or needed. This last assertion concerns the explicit stochastic model; the numerators of an actual fixed input have fixed primality, while the first three assertions above hold for each such input.

Facts & Assumptions

Given: The calibrated polynomial budget bound $P$ , the exact algebraic input, and independent random bits for each call. For the last assertion, let $D$ contain all modelled arithmetic data. The indicators $I_{j}$ are functions of $D$ and have the stated independent marginal model, but the remaining numerical data may have arbitrary correlations. Solver-bit streams are independent of $D$ and of one another; the enumerator ordering uses none of these solver bits. Conditioning on $D$ fixes primality, so no nondegenerate prime probabilities are asserted after that conditioning.

[F1]

Cyclotomic scaled grid and norm-equation solver defines the capped prospective single-factor execution and accepts only a verified exact norm certificate. An invalid or aborted computation only skips its candidate.

[F2]

Efficient exact cyclotomic norm solving with a supplied integer factorization proves that the construction terminates almost surely, is complete with a valid supplied factorization, and supplies the calibrated prime-input bound $P (k)$ , as well as expected polynomial bit cost on bounded grid inputs.

[F3]

Size and residue of the Rz candidate norm integer gives $n = 0$ or $n \equiv 1 (m o d 8)$ .

[F4]

Prime norm numerators congruent to one modulo eight are solvable gives solvability when $n = 1$ or $n$ is prime congruent to one modulo eight.

Proof

1.1F1givenalgebra

The exact certificate check in [F1] is a comparison of the four rational power-basis coefficients of $t^{†} t$ and $ξ$ . Equality of these coefficients is equality in the field, so acceptance always proves the required equation. On a composite input no field property of a proposed residue quotient and no NO_SOLUTION message is used as evidence: a failed operation, negative outcome, or work-cap interruption causes only a skip.

2.1F1F2step 1.1algebra

The construction is interrupted after $B = 2 ⌈ P (k) ⌉$ binary operations, regardless of whether its proposed prime factor was valid. Every generated bit string then has length bounded by the input length plus $B$ . The grid-input bound of [F2] makes its input length polynomial in $k + 1$ . A fixed-degree rational-coefficient multiplication and equality check therefore takes polynomial work in $k + 1 + B$ , by schoolbook integer multiplication and division. Since $B$ is a specified polynomial, total work including exact certification is polynomial on every input.

2.2F1F2F3F4step 1.1algebra

If $n$ is prime, the proposed one-factor factorization is valid, and [F3,F4] make its norm equation solvable. Let $T \geq 0$ be the binary work of the uncapped construction on this input. By the calibrated bound [F2], $E [T] \leq P (k)$ . The elementary inequality $T \geq B 1_{{T > B}}$ gives $\Pr (T > B) \leq E [T] / B \leq 1 / 2$ . Whenever $T \leq B$ , [F2] returns an exact solution and step 1.1 accepts it. Thus success probability is at least $1 / 2$ . The zero case is explicit in [F1], and [F4] plus the complete factored empty-list branch gives the numerator-one case.

3.1givenstep 2.2algebra∎

Condition first on all arithmetic data $D$ . Each call is then a deterministic function of its own input and its fresh solver bits, so its success events are independent under this conditional probability. By step 2.2 its conditional success probability is at least $I_{i} / 2$ ; this also holds for the immediate zero/unit branches. Consequently $\Pr (J > j ∣ D) \leq \prod_{i = 1}^{j} (1 - I_{i} / 2)$ . Average this inequality over $D$ . The indicators, rather than the successful-call events, are independent in the stated model; hence $E [\prod_{i = 1}^{j} (1 - I_{i} / 2)] = \prod_{i = 1}^{j} (1 - p_{i} / 2)$ . The lower bounds on $p_{i}$ give the displayed joint-failure estimate. Correlated numerical inputs can correlate the unconditional call successes, but cannot invalidate this estimate.

Depends on

Used by

T-count guarantees for Clifford+T Rz synthesis Theorem

Cited to discharge well-definedness by Cyclotomic scaled grid and norm-equation solver.

Dependency tree · two levels

23 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

Ross and Selinger, Optimal ancilla-free Clifford+T approximation of z-rotations, Algorithm 7.6 and Proposition 8.8 (standard reference, not scraped)