LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge 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.

Spectral bound for a symmetric lazy walk killed on a marked set

Statement

Let $X$ be a finite set of size $n \geq 2$ , and let $P = (I + Q) / 2$ where $Q$ is a symmetric row-stochastic matrix. Let $u = n^{- 1 / 2} 1_{X}$ . Assume the second-largest eigenvalue of $P$ is at most $1 - δ$ , where $0 < δ \leq 1$ . For $M \subseteq X$ , put $ε = ∣ M ∣ / n$ , $U = X ∖ M$ , and let $Π_{U}$ be the coordinate orthogonal projection defined by $Π_{U} e_{x} = e_{x}$ for $x \in U$ and $Π_{U} e_{x} = 0$ for $x \notin U$ . Let $P_{U} = Π_{U} P Π_{U}$ restricted to vectors supported on $U$ . Then $P$ has spectrum in $[0, 1]$ and

$∥ P_{U} ∥ \leq 1 - δ ε .$

The empty compression has norm $0$ by convention.

Facts & Assumptions

Given: The finite symmetric lazy transition matrix $P = (I + Q) / 2$ , its uniform unit vector $u$ , the marked set $M$ , and the second-eigenvalue bound.

[F1]

Finite row-stochastic kernel: $Q_{x y} \geq 0$ and $\sum_{y} Q_{x y} = 1$ for every row.

[F2]

Marked sets, stationary mass, and walk-search tasks: in the uniform case $ε = ∣ M ∣ / n$ .

[F3]

Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely: a finite-dimensional self-adjoint endomorphism has an orthonormal eigenbasis.

[F4]

Self-adjoint and normal endomorphisms of a finite-dimensional real or complex inner product space: a self-adjoint endomorphism equals its adjoint.

[F5]

The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv||: on a nonzero domain, $∥ T ∥ = \max_{∥ z ∥ = 1} ∥ T z ∥$ ; the zero-domain norm is $0$ .

[F6]

Cauchy–Schwarz: $∣ ⟨ u, v ⟩ ∣ \leq ∥ u ∥ ∥ v ∥$ , with equality exactly for linearly dependent vectors: $∣ ⟨ v, w ⟩ ∣ \leq ∥ v ∥ ∥ w ∥$ in a real or complex inner-product space.

Proof

1.1F1F3F4F6algebra

For any vector $z \in C^{X}$ , weighted Cauchy–Schwarz, obtained by applying [F6] to $(\sqrt{Q_{x y}})_{y}$ and $(\sqrt{Q_{x y}} z_{y})_{y}$ , gives $∣ (Q z)_{x} ∣^{2} \leq \sum_{y} Q_{x y} ∣ z_{y} ∣^{2}$ . Summing over $x$ and using symmetry, so that every column sum is also $1$ , yields $∥ Q z ∥^{2} \leq ∥ z ∥^{2}$ . Since $Q$ is self-adjoint by its real symmetric matrix and [F4], [F3] gives a real orthonormal eigenbasis; the contraction inequality forces every eigenvalue of $Q$ into $[- 1, 1]$ . Thus $P = (I + Q) / 2$ is self-adjoint with spectrum in $[0, 1]$ . Its row sums are $1$ , so $P u = u$ .

1.2F2F6givenalgebra

If $U = \emptyset$ , then $P_{U} = 0$ and the conclusion follows from [F5]. Otherwise choose a unit vector $z$ supported on $U$ and write $z = α u + v$ with $v ⊥ u$ . [F6] applied to $⟨ z, u ⟩ = ⟨ z, Π_{U} u ⟩$ gives $∣ α ∣^{2} \leq ∥ Π_{U} u ∥^{2} = ∣ U ∣ / n = 1 - ε$ , so $∥ v ∥^{2} = 1 - ∣ α ∣^{2}$ .

2.1F3givenstep 1.2algebra

The orthogonal complement $u^{⊥}$ is invariant under $P$ by self-adjointness and $P u = u$ . Its eigenvalues are at most $1 - δ$ by the stated second-eigenvalue hypothesis. Therefore $⟨ z, P z ⟩ = ∣ α ∣^{2} + ⟨ v, P v ⟩ \leq ∣ α ∣^{2} + (1 - δ) ∥ v ∥^{2} \leq 1 - δ ε$ .

3.1F3F4F5step 1.1step 2.1∎

The compression $P_{U}$ is positive semidefinite because $⟨ z, P_{U} z ⟩ = ⟨ z, P z ⟩ \geq 0$ for every vector supported on $U$ , by the nonnegative spectrum in step 1.1. It is self-adjoint, so its operator norm is its largest eigenvalue; equivalently it is the maximum of its unit-vector Rayleigh quotients. Step 2.1 bounds each such quotient by $1 - δ ε$ , proving the result.

Depends on

Used by

Szegedy-walk marked-set detection Algorithm
Classical marked-set hitting bound from a spectral gap Theorem
Walk detection correctness and cost Theorem

Dependency tree · two levels

21 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

Andrew M. Childs, Lecture Notes on Quantum Algorithms, Chapter 18, §18.4, Lemma 18.2 (standard reference, not scraped)
Ronald de Wolf, Quantum Computing: Lecture Notes, Chapter 8, §8.1 (standard reference, not scraped)
Frédéric Magniez, Ashwin Nayak, Jérémie Roland, and Miklos Santha, Search via Quantum Walk, Proposition 1 and §3 (standard reference, not scraped)