TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck pass

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.

Correctness and cost of the linear-combination sampler

Statement

Run Finite rejection sampler for a linear combination with $k \geq 1$ , $x = \sum_{j = 1}^{k} w_{j} v_{j} \neq 0$ , and positive integer cap $R$ . Put $C : = \sum_{j} ∥ w_{j} v_{j} ∥_{2}^{2} / ∥ x ∥_{2}^{2}$ , and suppose a proof-side bound $C_{0} \geq C$ and $0 < δ < 1$ satisfy $R \geq k C_{0} \ln (1 / δ)$ . The routine itself receives $R$ but does not test or require a certificate for $C_{0}$ ; these are hypotheses for this theorem's guarantee. A proposal is accepted with probability $1 / (k C)$ , and conditional on acceptance its index has law $D_{x}$ . The probability of returning FAIL is at most $δ$ . The worst-case entry-query count is at most $k R$ , with at most $R$ mixture draws and $R$ vector-sample calls in addition. If an entry query, a mixture draw, and a vector-sample call have uniform cost upper bounds $Q$ , $B_{m i x}$ , and $B_{s a m p}$ in the declared model, their total access cost is at most $B_{s e t u p} + R (k Q + B_{m i x} + B_{s a m p})$ , where $B_{s e t u p}$ charges the initial norm queries and mixture setup. Arithmetic, acceptance randomness, and output writing are charged separately; no unit-cost sampling or bit-time bound is assumed. As $R \to \infty$ , the capped expected number of trials tends to $k C$ .

Facts & Assumptions

Given: The access and coefficient hypotheses of the Statement, with $x \neq 0$ .

[F1]

Finite rejection sampler for a linear combination: with $S = \sum_{j} ∥ w_{j} v_{j} ∥_{2}^{2} > 0$ , the proposal chooses term $j$ proportionally to $∥ w_{j} v_{j} ∥_{2}^{2}$ and then samples from $D_{v_{j}}$ ; its acceptance probability is the displayed ratio. The routine's finite cap does not depend on detecting the truth of $C \leq C_{0}$ .

[F2]

ℓ2 sample/query access to vectors and matrices: each nonzero term sampler has law $D_{v_{j}}$ with fresh conditional randomness; entry queries, norm queries, and sample calls have separately declared costs.

[F3]

Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation: $∣ \sum_{j} a_{j} b_{j} ∣^{2} \leq k \sum_{j} ∣ a_{j} b_{j} ∣^{2}$ .

[F4]

$1 + x \leq \exp (x)$ for every real $x$ , hence $(1 - p)^{m} \leq \exp (- m p)$ : for $0 \leq p \leq 1$ , $(1 - p)^{R} \leq e^{- R p}$ .

[F5]

Adaptive conditional failure budgets compose by a union bound: for independent trials of success probability $p > 0$ , the expected capped number of trials tends to $1 / p$ as the cap tends to infinity.

Proof

1.1givenF1F2algebra

Put $S = \sum_{j} ∥ w_{j} v_{j} ∥_{2}^{2} > 0$ . The proposal probability of coordinate $i$ is $P (i) = \sum_{j} (w_{j} v_{j, i})^{2} / S$ , because choosing $j$ has weight $∥ w_{j} v_{j} ∥_{2}^{2} / S$ and the conditional coordinate law is $v_{j, i}^{2} / ∥ v_{j} ∥_{2}^{2}$ . Its target probability is $Q (i) = x_{i}^{2} / ∥ x ∥_{2}^{2}$ .

2.1step 1.1F3algebra

When $\sum_{j} (w_{j} v_{j, i})^{2} > 0$ , [F3] shows the acceptance ratio $Q (i) / (k C P (i)) = x_{i}^{2} / [k \sum_{j} (w_{j} v_{j, i})^{2}]$ lies in $[0, 1]$ . If the denominator is zero, then every $w_{j} v_{j, i} = 0$ , so $x_{i} = 0$ and the prescribed acceptance is $0$ .

3.1step 1.1step 2.1F3algebra

Multiplying proposal and acceptance probabilities gives $P (i) a_{i} = Q (i) / (k C)$ . Summing over $i$ shows total acceptance probability is $1 / (k C)$ , and conditioning on acceptance yields $Q (i)$ . Also $k C \geq 1$ by [F3] applied to each coordinate and summed.

4.1givenF1F2F4F5algebra∎

Independent trials miss with probability $(1 - 1 / (k C))^{R}$ . Since $C \leq C_{0}$ , this is at most $e^{- R / (k C_{0})} \leq δ$ by [F4] and the cap hypothesis. Each executed trial queries the $k$ entries at its sampled coordinate, makes one mixture draw, and calls one vector sampler. At most $R$ trials therefore use at most $k R$ entry queries and $R$ calls of each other type. Initial norms and mixture setup contribute $B_{s e t u p}$ ; multiplying the call counts by the declared uniform upper bounds gives $B_{s e t u p} + R (k Q + B_{m i x} + B_{s a m p})$ . This count excludes arithmetic, acceptance randomness, and output writing, which retain their separate charges. With per-trial success probability $1 / (k C)$ , [F5] shows the capped expected trial count tends to $k C$ as $R \to \infty$ .

Depends on

Used by

Tang's conditional recommendation sampler Theorem

Cited to discharge well-definedness by Finite rejection sampler for a linear combination.

Dependency tree · two levels

36 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

Ewin Tang, A quantum-inspired classical algorithm for recommendation systems, version 3 (standard reference, not scraped)