LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generated

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.

Conditional stopping bounds for prime-tested Rz candidates

Statement

For the candidate sequence and exponents of Exponent growth of the Rz scaled grid, let $E_{j}$ be success events and $J = \min {j \geq 1 : E_{j}}$ . Suppose there are numbers $p_{j} \in [0, 1]$ with $p_{j} \geq c / (k_{j} + 1)$ , for a constant $0 < c \leq 1$ independent of the input, such that $\Pr (J > j) \leq \prod_{i = 1}^{j} (1 - p_{i}) (j \geq 1) .$ Independent success events of probabilities $p_{j}$ are a sufficient special case; independence of the events is not otherwise required. Then $J < \infty$ almost surely and, for every fixed positive integer $r$ , $E [J^{r}] = O ((k_{2} + 1)^{r}) = O ((1 + \log (1 / ε))^{r}) .$ In particular $E [J] = O (\log (1 / ε))$ and $E [\log_{2} J] = O (1 + \log \log (1 / ε))$ . The implied constants can depend on $c$ and $r$ , but not on $θ$ or $ε$ . For every fixed nonnegative integer $d$ , $E [J (1 + k_{2} + \log J)^{d}]$ is polynomially bounded in $1 + k_{2}$ .

This is the explicit quantitative probabilistic assumption needed when Ross–Selinger Hypothesis 8.3 is used for a complexity claim. It is a conditional model, not an assertion of independence for a deterministic input sequence.

Facts & Assumptions

Given: The success events, joint-failure product bound, constant $c$ , and random index $J$ in the statement.

[F1]

Exponent growth of the Rz scaled grid gives $k_{j} \leq k_{2} + 2 ⌈ \log_{2} j ⌉$ and $k_{2} = O (1 + \log (1 / ε))$ .

Proof

1.1F1givenalgebra

By [F1], choose constants $a \geq 1$ and $b > 0$ , with $a = O (k_{2} + 1)$ , so that $p_{j} \geq 1 / (a + b \ln j)$ for all $j \geq 1$ . The assumed joint-failure bound and $1 - x \leq e^{- x}$ imply $\Pr (J > j) \leq \prod_{h = 1}^{j} (1 - p_{h}) \leq \exp (- j / (a + b \ln j))$ . This upper bound tends to zero, which proves almost sure finiteness.

2.1step 1.1algebra

For $j \geq a$ , put $x = j / a \geq 1$ . Since $\ln a \leq a$ and $\ln x \leq 2 \sqrt{x}$ , one has $a + b \ln j \leq (1 + 3 b) a \sqrt{x}$ . Hence $\Pr (J > j) \leq \exp (- \sqrt{j / a} / (1 + 3 b))$ for $j \geq a$ . For an integer-valued positive random variable, summing the identity $J^{r} = \sum_{j = 0}^{J - 1} ((j + 1)^{r} - j^{r})$ and using nonnegative sums gives $E [J^{r}] = \sum_{j \geq 0} ((j + 1)^{r} - j^{r}) \Pr (J > j)$ . The part $j < a$ is $O (a^{r})$ . The remaining part is bounded by a constant times $\sum_{j \geq a} (j + 1)^{r - 1} e^{- \sqrt{j / a} / (1 + 3 b)} = O (a^{r})$ : comparison with the integral and substitution $y = \sqrt{t / a}$ reduce it to $a^{r} \int_{1}^{\infty} y^{2 r - 1} e^{- y / (1 + 3 b)} d y$ , which is finite by repeated integration by parts. This proves all the moment bounds.

3.1F1step 2.1algebra∎

The elementary tangent bound $\ln x \leq \ln μ + (x - μ) / μ$ for $x, μ > 0$ , with $μ = E [J]$ , gives $E [\log_{2} J] \leq \log_{2} E [J] = O (1 + \log (k_{2} + 1))$ . Finally $\log J \leq J$ , and expansion of $J (1 + k_{2} + J)^{d}$ reduces its expectation to the finitely many moments in step 2.1; these are polynomial in $k_{2} + 1$ . The stated bounds in $ε$ follow from [F1].

Depends on

Exponent growth of the Rz scaled grid

Used by

T-count guarantees for Clifford+T Rz synthesis Theorem

Dependency tree · two levels

6 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, Hypothesis 8.3 and Proposition 8.8 (standard reference, not scraped)