Alphabeta MathHow 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.
Effective spectral gap for a product of two reflections
Statement
Let H be a finite-dimensional complex inner-product space, Π and Δ orthogonal projections on H, R_Π=2Π-I and R_Δ=2Δ-I, and U=R_ΠR_Δ. For 0≤ω≤π, let E_ω be the spectral projection of U onto eigenvalues e^{iφ} whose principal arguments satisfy |φ|≤ω. If Δw=0, then
Facts & Assumptions
Given: The finite-dimensional projections and vector w in the Statement, with Δw=0.
Orthogonal-Projector Reflection and Access Contract: for an orthogonal projection P, the plus-on-range reflection is R_P=2P-I.
Projector Reflections Are Hermitian Unitary Involutions: each such reflection is a unitary involution.
Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely: a finite-dimensional unitary has an orthonormal eigenbasis; its eigenvalues have modulus one.
Proof
Put R_P=2P-I and R_D=2D-I. Since D w=0, R_D w=-w; hence U w=R_P R_Dw=-R_Pw and therefore P w=(w+R_Pw)/2=(I-U)w/2.
Let E_ω be the orthogonal spectral projection of U onto eigenvectors with eigenvalue e^{iφ} for a principal phase φ∈[-π,π] satisfying |φ|≤ω. By [F2], both reflections are unitary, so U is unitary. By [F3], E_ω commutes with U and has an orthonormal eigenbasis. Thus E_ω P w=(I-U)E_ωw/2, and on each selected eigenvector |1-e^{iφ}|≤|φ|≤ω. The squared norm in that basis is at most (ω/2)^2||E_ωw||²≤(ω/2)^2||w||².
Taking square roots proves ||E_ωP w||≤ω||w||/2, including zero- and full-rank projections because step 1.1 used only the projection identities.
Depends on
- Orthogonal-Projector Reflection and Access Contract
- Real and complex inner product spaces, with the inner product linear in the first argument
- Dirac Notation Conversion
- Projector Reflections Are Hermitian Unitary Involutions
- Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely
Used by
Dependency tree · two levels
26 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 (17 April 2025) (standard reference, not scraped)
- Ronald de Wolf, Quantum Computing: Lecture Notes, arXiv:1907.09415v6 (standard reference, not scraped)