TheoremStatement: Literature-sourcedProof: 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.

Exact row-preparation access count for one and two walk steps

Statement

For a nonempty chain in the row-preparation implementation of Finite row-preparation access model for a Szegedy walk, the full-workspace word $S V_{P} R_{0} V_{P}^{*}$ restricts on the clean-work subspace to the logical one-reflection step $U = S (2 T T^{*} - I)$ . One such uncontrolled step uses exactly one call each to $V_{P}^{*}$ and $V_{P}$ , one clean-state reflection $R_{0}$ , and one swap $S$ . The factorwise controlled implementation controls each constituent, including both row-preparation calls, $R_{0}$ , and $S$ ; this count describes that implementation. A $W = U^{2}$ step uses exactly two such $U$ implementations. Query calls, gate counts, description bits, uniform-generation time, and precision are recorded as separate cost coordinates.

Facts & Assumptions

Given: A nonempty finite row-stochastic kernel, the row-preparation unitary and its specified clean work state, the explicitly listed inverse and controlled capabilities, the clean-state reflection, and the swap implementation.

[F1]

Finite row-preparation access model for a Szegedy walk: $V_{P}$ is unitary and sends each clean input $∣ x, 0, 0_{W} ⟩$ to $T ∣ x ⟩ \otimes ∣ 0_{W} ⟩$ ; $R_{0} = 2 (I_{X} \otimes ∣ 0, 0_{W} ⟩ ⟨ 0, 0_{W} ∣) - I$ ; the swap is $S$ on the first two registers and identity on work.

[F2]

Szegedy reflection walk and its two-reflection square: the logical operators are $R_{A} = 2 T T^{*} - I$ , $U = S R_{A}$ , and $W = U^{2}$ .

[F3]

The Szegedy discriminant is self-adjoint and contractive: $T^{*} T = I$ , so $T$ is an isometry and its row vectors form an orthonormal list.

[F4]

Controlled Unitary Access: on a control-first register, $C (A) = diag (I, A)$ ; products of such blocks implement the controlled product word.

[F5]

Inverse Unitary Access: inverse access is the explicitly granted $V_{P}^{*} = V_{P}^{- 1}$ operation, with its cost declared separately.

[F6]

Circuit-family and computation cost model: circuit-description, gate, depth, width, generator, oracle-query and precision costs are distinct coordinates, with inapplicable coordinates recorded as such.

[F7]

Ordered tensor registers, their inner product, and wire permutations: the ordered product basis is orthonormal and factor permutations act on that basis in the specified order.

[F8]

Adjoints satisfy $(S + T)^{*} = S^{*} + T^{*}$ , $(λ T)^{*} = \overline{λ} T^{*}$ , $(S T)^{*} = T^{*} S^{*}$ , and $T^{* *} = T$ : adjoints reverse products, so $(T T^{*})^{*} = T T^{*}$ .

[F9]

An endomorphism is an orthogonal projection exactly when it is idempotent and self-adjoint: a self-adjoint idempotent is the orthogonal projection onto its range.

Proof

1.1F1F2F3F5F7F8F9algebra

By [F3], $T^{*} T = I$ , so $Π : = T T^{*}$ is idempotent; [F8] gives $Π^{*} = Π$ , and [F9] identifies it as the orthogonal projection onto $ran T$ (it maps into $ran T$ and fixes every $T v$ ). Let $J : C^{X} \to C^{X} \otimes C^{X} \otimes W$ send $∣ x ⟩$ to $∣ x, 0, 0_{W} ⟩$ . The orthonormal product basis [F7] makes $J$ an isometry and gives $J J^{*} = I_{X} \otimes ∣ 0, 0_{W} ⟩ ⟨ 0, 0_{W} ∣$ . By [F1], $V_{P} J = T \otimes ∣ 0_{W} ⟩$ . Hence, using [F5] and unitarity of $V_{P}$ , $V_{P} R_{0} V_{P}^{*} = 2 (V_{P} J) (V_{P} J)^{*} - I = 2 (T T^{*} \otimes ∣ 0_{W} ⟩ ⟨ 0_{W} ∣) - I .$ For any logical state $h \in C^{X \times X}$ , this operator sends $h \otimes ∣ 0_{W} ⟩$ to $(2 T T^{*} - I) h \otimes ∣ 0_{W} ⟩ = R_{A} h \otimes ∣ 0_{W} ⟩$ . The extended swap sends $h \otimes ∣ 0_{W} ⟩$ to $S h \otimes ∣ 0_{W} ⟩$ . Thus the word $S V_{P} R_{0} V_{P}^{*}$ restricts to $S R_{A} = U$ and returns the work register to its clean state.

2.1F1F2F5step 1.1algebra

Reading $S V_{P} R_{0} V_{P}^{*}$ from right to left applies one $V_{P}^{*}$ call, one $R_{0}$ , one $V_{P}$ call, and one swap. The inverse and forward preparation, reflection and swap costs are therefore each charged once in this implementation.

3.1F1F4step 2.1given

In the factorwise controlled implementation, replace each factor in step 2.1 by its control-first block. By [F4], their product is the controlled full word: the control-zero block is identity and the control-one block is $S V_{P} R_{0} V_{P}^{*}$ . It uses controlled $V_{P}^{*}$ , $R_{0}$ , $V_{P}$ , and $S$ , with each declared cost charged separately; without one of these capabilities this particular construction is unavailable.

4.1F2F6step 1.1step 2.1algebra∎

By [F2], $W = U^{2}$ is two successive $U$ steps, and step 1.1 shows the work state is clean again after each step. Thus exactly two copies of the step counts in step 2.1 implement $W$ . The resource coordinates remain separate by [F6].

Depends on

Used by

MNRS finite reversible-walk finding Algorithm
Szegedy-walk marked-set detection Algorithm
Coherent Johnson row access with stored values Lemma
Walk detection correctness and cost Theorem

Cited to discharge well-definedness by Finite row-preparation access model for a Szegedy walk.

Dependency tree · two levels

53 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, §18.2 (standard reference, not scraped)
Ronald de Wolf, Quantum Computing: Lecture Notes, §8.2 (standard reference, not scraped)