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.

Low-target amplification has a controlled multiplicative loss

Statement

Let $n \geq 1$ be an integer. Let a coherent sampler have success weight $q > 0$ , and suppose an estimate $\hat{q} > 0$ satisfies $∣ \hat{q} - q ∣ \leq q / 100$ and $\hat{q} \leq 1 / (9 n)$ . Choose the least integer $k \geq 0$ such that $(2 k + 1)^{2} \hat{q} \geq 1 / (9 n)$ , and put $d = 2 k + 1$ , $x = d^{2} \hat{q}$ , $y = d^{2} q$ . Applying $k$ standard iterates of Amplitude amplification with a fixed integer iteration count gives success weight $r$ satisfying $\frac{1}{9 n} \leq x \leq \frac{1}{n}, \frac{100}{101} x \leq y \leq \frac{100}{99} x, y (1 - \frac{2}{5 n}) \leq r \leq y .$ In particular $1 / (16 n) \leq r \leq \min {1, 100 / (99 n)}$ , and the positive-probability conditional good state is unchanged. The total number of sampler/inverse calls in this fixed amplification is exactly $d$ , charging reflections separately.

For any $s \leq n$ such amplifications, indexed by $i$ , with the same parameter $n$ , their multiplicative losses obey $\prod_{i = 1}^{s} \frac{r_{i}}{d_{i}^{2} q_{i}} \geq \frac{3}{5}, \prod_{i = 1}^{s} d_{i} \leq \sqrt{\frac{5}{3}} \prod_{i = 1}^{s} \sqrt{\frac{r_{i}}{q_{i}}} .$

Facts & Assumptions

Given: The coherent sampler, relative estimate, integer $n$ and least crossing index $k$ in the Statement; all sampler inverse and reflection operations required by the fixed amplification are supplied.

[F1]

Exact success probability after amplitude amplification gives $r = \sin^{2} (d θ)$ for $θ = \arcsin \sqrt{q}$ ; Amplitude-amplification invariant plane keeps the good component collinear with the original good component.

[F2]

Principal inverse sine and inverse cosine and For $- 1 < y < 1$ , $(\arcsin y)^{'} = 1 / \sqrt{1 - y^{2}}$ and $(\arccos y)^{'} = - 1 / \sqrt{1 - y^{2}}$ give $\arcsin 0 = 0$ and $(\arcsin u)^{'} = (1 - u^{2})^{- 1 / 2}$ for $∣ u ∣ < 1$ .

[F3]

The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ and Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ give the mean value theorem and derivative rules. The derivatives of sine and cosine are cosine and minus sine gives $\sin^{'} = \cos$ , $\cos^{'} = - \sin$ , $\sin 0 = 0$ and $\cos 0 = 1$ .

[F4]

The addition formulas for sine and cosine and Parity and the Pythagorean identity for sine and cosine give sine addition and $∣ \sin u ∣, ∣ \cos u ∣ \leq 1$ for real $u$ .

[F5]

Amplitude-amplification access and resource accounting counts $k + 1$ forward calls, $k$ inverse calls and $k$ calls to each reflection.

[F6]

Bernoulli's inequality $(1 + x)^{n} \geq 1 + n x$ gives $(1 - a)^{n} \geq 1 - n a$ for $0 \leq a \leq 1$ and integer $n \geq 1$ .

Proof

1.1givenalgebra

Since $\hat{q} > 0$ , some finite $k$ crosses the target. If the least index is $k = 0$ , the crossing and $\hat{q} \leq 1 / (9 n)$ force $x = 1 / (9 n)$ . If $k \geq 1$ , minimality gives $(d - 2)^{2} \hat{q} < 1 / (9 n)$ , so $d \sqrt{\hat{q}} < 1 / (3 \sqrt{n}) + 2 \sqrt{\hat{q}} \leq 1 / \sqrt{n}$ and $x < 1 / n$ . The relative estimate gives $99 q / 100 \leq \hat{q} \leq 101 q / 100$ , hence $100 / 101 \leq q / \hat{q} \leq 100 / 99$ . Multiplying by $x$ proves the bounds on $y$ , and also $q \leq 100 / (891 n) < 1$ .

2.1givenF2F3step 1.1algebra

Put $u = \sqrt{q}$ . For $0 \leq v \leq u$ , [F2] gives $1 \leq (\arcsin v)^{'} \leq (1 - q)^{- 1 / 2}$ . Applying [F3] to $\arcsin$ on $[0, u]$ yields $\sqrt{q} \leq θ \leq \sqrt{q} / \sqrt{1 - q}$ . Therefore $z = d θ$ satisfies $y \leq z^{2} \leq y / (1 - q) \leq (100 / (99 n)) / (1 - 100 / 891) = 900 / (791 n)$ .

3.1givenF3F4step 2.1algebra

For $v \geq 0$ define $f (v) = \sin v - v + v^{3} / 6$ . By [F3] and [F4], $f^{'''} (v) = 1 - \cos v \geq 0$ and $f^{''} (0) = f^{'} (0) = f (0) = 0$ . Three applications of the mean value theorem imply successively $f^{''} (v) \geq 0$ , $f^{'} (v) \geq 0$ and $f (v) \geq 0$ . Thus $\sin z \geq z - z^{3} / 6$ . Step 2.1 gives $z^{2} \leq 900 / 791 < 6$ , so this lower bound is positive and may be squared: $\sin^{2} z \geq z^{2} (1 - z^{2} / 6)^{2} \geq z^{2} (1 - z^{2} / 3) \geq y (1 - 300 / (791 n)) \geq y (1 - 2 / (5 n))$ . The factor $1 - 300 / (791 n)$ is positive because $n \geq 1$ , which justifies replacing $z^{2}$ by its lower bound $y$ .

4.1givenF1F4step 1.1step 3.1inductionalgebra

Sine addition and [F4] give $∣ \sin ((h + 1) θ) ∣ \leq ∣ \sin (h θ) ∣ + \sin θ$ for integer $h \geq 1$ . Finite induction yields $∣ \sin (d θ) ∣ \leq d \sin θ$ , so [F1] gives $r \leq d^{2} q = y$ . Together with step 3.1 this proves the multiplicative loss bound. Since $y \geq 100 / (909 n)$ , it also gives $r \geq (100 / (909 n)) (3 / 5) = 20 / (303 n) > 1 / (16 n)$ ; the upper bounds $r \leq 100 / (99 n)$ and $r \leq 1$ follow from step 1.1 and [F4]. In particular $r > 0$ , and the collinearity in [F1] shows that conditioning on success preserves the original good state.

5.1givenF5F6step 4.1algebra∎

By [F5], this fixed amplification makes $k + 1 + k = 2 k + 1 = d$ sampler/inverse calls and $k$ calls to each reflection. For $s \leq n$ instances, the preceding bounds give $\prod_{i = 1}^{s} r_{i} / (d_{i}^{2} q_{i}) \geq (1 - 2 / (5 n))^{s} \geq (1 - 2 / (5 n))^{n} \geq 3 / 5$ by [F6]. All factors are positive, so rearranging this product inequality and taking nonnegative square roots gives $\prod_{i = 1}^{s} d_{i} \leq \sqrt{5 / 3} \prod_{i = 1}^{s} \sqrt{r_{i} / q_{i}}$ , as claimed.

Remarks

The upper bound $x \leq 1 / n$ concerns the estimated quadratic weight. A one-percent estimate allows the actual amplified weight $r$ to exceed $1 / n$ ; the proved bound $r \leq 100 / (99 n)$ retains this distinction. No estimate is treated as an exact amplitude input to the known-amplitude maximization procedure.

Depends on

Used by

Finite CKS sparse QLSP with variable-time inverse estimation Algorithm
CKS stopping-time and success-mass instantiation Lemma
CKS nearly-linear condition-number guarantee Theorem
Variable-time amplitude-amplification theorem Theorem

Dependency tree · two levels

67 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

Gilles Brassard, Peter Høyer, Michele Mosca, and Alain Tapp, Quantum Amplitude Amplification and Estimation (standard reference, not scraped)
Andris Ambainis, Variable time amplitude amplification and a faster quantum algorithm for solving systems of linear equations (standard reference, not scraped)