LemmaStatement: 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.

Szegedy reflections and walk operators are unitary

Statement

For the projection $Π = T T^{*}$ onto $A = ran (T)$ , the operators $R_{A} = 2 Π - I$ and $S$ are self-adjoint involutions. Hence $U = S R_{A}$ and $W = U^{2}$ are unitary. On $A^{⊥}$ , $Π = 0$ and therefore $U = - S$ .

Facts & Assumptions

Given: The finite row-preparation isometry $T$ , its adjoint, the swap $S$ , and the definitions of $Π, R_{A}, U, W$ in Szegedy row-preparation map and discriminant and Szegedy reflection walk and its two-reflection square.

[F1]

The Szegedy discriminant is self-adjoint and contractive: $T^{*} T = I$ , so $T$ is an isometry.

[F2]

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

[F3]

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

[F4]

Linear isometries, and orthogonal or unitary operators on finite-dimensional inner product spaces: a unitary operator is an invertible linear isometry on a finite-dimensional complex inner-product space.

[F5]

Real and complex inner product spaces, with the inner product linear in the first argument: the inner product is positive definite and uses the root's linear-first convention.

[F6]

The adjoint $T^{*} : W \to V$ is characterised by $⟨ T v, w ⟩_{W} = ⟨ v, T^{*} w ⟩_{V}$ : $⟨ A u, v ⟩ = ⟨ u, A^{*} v ⟩$ for an adjoint.

[F7]

Szegedy row-preparation map and discriminant: $S ∣ x, y ⟩ = ∣ y, x ⟩$ on the orthonormal product basis.

Proof

1.1F1F2F3F6algebra

From [F1], $Π^{2} = T T^{*} T T^{*} = T (T^{*} T) T^{*} = T T^{*} = Π$ . For all $u, v$ , [F6] and conjugate symmetry give $⟨ Π u, v ⟩ = ⟨ T^{*} u, T^{*} v ⟩ = ⟨ u, Π v ⟩$ , so $Π^{*} = Π$ . By [F3], $Π$ is the orthogonal projection onto its image, which is $A = ran (T)$ because it fixes every $T v$ .

2.1F2F4F5F7step 1.1algebra

Since $Π^{2} = Π$ and $Π^{*} = Π$ , $R_{A}^{*} = 2 Π^{*} - I = R_{A}$ and $R_{A}^{2} = 4 Π^{2} - 4 Π + I = I$ . Thus $∥ R_{A} w ∥^{2} = ⟨ R_{A} w, R_{A} w ⟩ = ⟨ w, R_{A}^{*} R_{A} w ⟩ = ∥ w ∥^{2}$ for every $w$ . By [F7], $S$ permutes the orthonormal product basis by the transposition $(x, y) \mapsto (y, x)$ , so its permutation matrix is its own inverse and adjoint: $S^{2} = I$ and $S^{*} = S$ . It is therefore an invertible isometry and is unitary.

3.1F1F2F4F5F6F7step 2.1algebra∎

If $w \in A^{⊥}$ , then [F6] gives $⟨ v, T^{*} w ⟩ = ⟨ T v, w ⟩ = 0$ for every $v$ , so taking $v = T^{*} w$ and using positive definiteness [F5] gives $T^{*} w = 0$ and $Π w = 0$ ; hence $U w = S (2 Π - I) w = - S w$ . Both $S$ and $R_{A}$ are invertible norm-preserving maps by step 2.1, so $U = S R_{A}$ and $W = U^{2}$ are unitary.

Depends on

Used by

Cited to discharge well-definedness by Szegedy reflection walk and its two-reflection square.

Dependency tree · two levels

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