DefinitionDefinition: AI-adaptedProof: AI-generatedPipeline-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.

Expected query cost from finite execution prefixes

Definition

Fix a promised input $z$ and a sequential procedure whose elementary steps are deterministic transitions, finite random transitions, finite-outcome measurements, or a single oracle call. At every live history, the next transition has a specified probability law on a finite outcome set; a query step has one successor and issues one call. A halted history is extended by deterministic idle steps that issue no calls.

For $M \in N$ , let $Ω_{M}$ be the finite set of length- $M$ histories with the recursively assigned transition weights. Let $C_{M} : Ω_{M} \to {0, \dots, M}$ count the oracle calls actually executed in those $M$ steps. Define the expected query cost on input $z$ by

E_{q u e r y} (z) : = \sup_{M \in N} E [C_{M}] \in [0, \infty],

where each expectation is taken on the finite probability space of the corresponding prefix. Define the pathwise total query count on an infinite history $ω$ by $C (ω) : = \sup_{M} C_{M} (ω)$ . No probability measure or expectation of $C$ on an infinite history space is presumed by this definition.

If a procedure is organized into rounds of at most $K$ elementary steps for some fixed integer $K \geq 1$ , each containing at most one query, pad each round with deterministic idle steps to exactly $K$ steps. In this padded procedure, its first $R$ rounds are the prefix of length $K R$ . Hence the supremum of its finite-round expected query counts equals the displayed finite-step supremum. In particular, query-indexed rounds are valid when each round contains exactly one query, as in Simon sampling.

Facts & Assumptions

Given: A fixed promised input and a sequential procedure satisfying the finite-outcome transition and one-query-per-step conditions in the Definition.

[A1]

At each live finite history $h$ , the next-step probabilities $p_{h} (o)$ are nonnegative and sum to one over the finite next-outcome set; after halting, the unique idle successor has probability one.

[A2]

$[0, \infty]$ denotes the extended nonnegative reals with the usual least-upper-bound convention, so every subset has a supremum in that interval.

[F1]

Finite probability spaces, outcome weights, events, and event probabilities: a finite probability space has nonnegative outcome weights summing to one, and events are subsets of its finite outcome set.

[F2]

Real random variables on finite probability spaces and their finite distributions: a real random variable on a finite probability space is a function on its finite outcome set and therefore has finite range.

[F3]

Expectation of a real random variable on a finite probability space: the expectation is the finite sum of outcome values multiplied by their probability weights.

[F4]

Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule: finite sums can be reindexed by bijections and a sum over a finite Cartesian product equals either iterated finite sum.

[F5]

The principle of mathematical induction: a property holding at zero and preserved from $M$ to $M + 1$ holds for every natural number $M$ .

Verification

1.1givenF1base

For $M = 0$ , the only history is the empty history with weight one, so $Ω_{0}$ is a finite probability space by [F1].

2.1givenA1F1F4step 1.1ihalgebra

Assume the length- $M$ histories form a finite probability space. Each has finitely many successors, so their length- $(M + 1)$ extensions form a finite set. For each parent history $h$ , the total weight of its children is $w (h) \sum_{o} p_{h} (o) = w (h)$ by [A1]. Summing over the finite parent set by [F4] shows that the extended weights again sum to one. Thus $Ω_{M + 1}$ is a finite probability space.

3.1step 1.1step 2.1F5discharge-induction

Steps 1.1 and 2.1 establish the base and successor cases; induction [F5] proves that every $Ω_{M}$ is a finite probability space.

3.2A1F4step 2.1algebra

For any length- $M$ history $h$ , the sum of the weights of its length- $(M + 1)$ extensions is $w (h) \sum_{o} p_{h} (o) = w (h)$ by [A1]. Therefore projection to length- $M$ prefixes preserves every prefix's probability weight.

4.1givenF2step 3.2algebra

The count $C_{M}$ is a function on the finite set $Ω_{M}$ , so it is a finite real random variable by [F2]. Every additional step either adds one query or is a nonquery or idle step; consequently, under the prefix projection, $C_{M} \leq C_{M + 1}$ pathwise.

5.1F1F3step 3.2step 4.1algebra

By [F3] and the prefix-marginal identity in step 3.2, the expectation of $C_{M}$ computed on the length- $(M + 1)$ tree equals its length- $M$ expectation. The pointwise inequality in step 4.1 and nonnegative transition weights then give $E [C_{M}] \leq E [C_{M + 1}]$ . Each expectation is finite because $0 \leq C_{M} \leq M$ .

5.2A2F1F3step 3.1step 4.1

Each $C_{M}$ is bounded between $0$ and $M$ , so its finite-space expectation is a finite nonnegative real by [F1] and [F3]. Step 3.1 supplies a normalized prefix space for every $M$ , and [A2] therefore makes the displayed supremum well-defined in $[0, \infty]$ .

6.1givenA2F3step 5.1choosealgebradischarge-induction: step 3.1∎

For round length bounded by $K \geq 1$ , pad every round by idle steps so its end is a length- $K R$ prefix after $R$ rounds. These round-end indices are cofinal in $N$ : for every $M$ choose $R$ with $K R \geq M$ . By step 5.1 the expected counts are nondecreasing, so $\sup_{R} E [C_{K R}] = \sup_{M} E [C_{M}]$ . This proves the finite-round claim without applying a finite-space theorem to an unbounded total count.

Depends on

Used by

Unknown-amplitude randomized search Algorithm
Classical query complexity Definition
Quantum query complexity Definition
Simon independent-sample rank process Definition
Expected bit-query cost of unknown-count BBHT search Theorem
Expected cost of unknown-amplitude search Theorem
Simon recovery succeeds with probability at least 1-delta Theorem
Unknown-amplitude search has no false positives and halts almost surely Theorem

Dependency tree · two levels

18 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

Ronald de Wolf, Quantum Computing: Lecture Notes (standard reference, not scraped)
Andrew M. Childs, Lecture Notes on Quantum Algorithms (standard reference, not scraped)
John Preskill, Quantum Information, Chapter 6: Quantum Algorithms (standard reference, not scraped)