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

Projector Reflections Are Hermitian Unitary Involutions

Statement

Let $H$ be a finite-dimensional complex-inner-product space and let $Π$ be an orthogonal projection. The operators $R_{Π} = 2 Π - I$ and $S_{Π} = I - 2 Π$ are self-adjoint unitary involutions, with $R_{Π} = - S_{Π}$ . On $ran Π$ they act as $+ I$ and $- I$ , respectively; on $\ker Π$ they act as $- I$ and $+ I$ . In control-first order,

$C (S_{Π}) = (Z_{C}) C (R_{Π}), Z_{C} : = diag (I_{H}, - I_{H}) = Z \otimes I_{H} .$

Facts & Assumptions

Given: The finite-dimensional complex-inner-product space and orthogonal projection in the Statement.

[L1]

Orthogonal-Projector Reflection and Access Contract fixes $R_{Π} = 2 Π - I$ and $S_{Π} = I - 2 Π = - R_{Π}$ , and requires explicit control access. Its carrier is present in this batch.

[L2]

Controlled Unitary Access defines the control-first block operator $C (U) = diag (I_{H}, U)$ . Its carrier is present in this batch.

[L3]

The Pauli matrices defines the exact control- $Z$ matrix. Its current draft definition body was read; its item is now present in the QC07 manifest and page; the page remains draft.

[F1]

An endomorphism is an orthogonal projection exactly when it is idempotent and self-adjoint: an orthogonal projection satisfies $Π^{*} = Π$ and $Π^{2} = Π$ , and its range is orthogonal to its kernel.

[F2]

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

[F3]

Adjoints satisfy $(S + T)^{*} = S^{*} + T^{*}$ , $(λ T)^{*} = \overline{λ} T^{*}$ , $(S T)^{*} = T^{*} S^{*}$ , and $T^{* *} = T$ : adjoints are conjugate-linear in scalars, preserve sums, and reverse products.

[F4]

For an endomorphism in finite dimension, preserving lengths, preserving inner products, carrying orthonormal bases to orthonormal bases, and $T^{*} T = I$ are equivalent: for an endomorphism of a finite-dimensional inner-product space, $T^{*} T = I$ implies that $T$ is an invertible isometry and $T T^{*} = I$ .

Proof

1.1givenF1F2F3

By [F1], $Π^{*} = Π$ and $Π^{2} = Π$ . The adjoint rules [F2] and [F3] give $R_{Π}^{*} = 2 Π - I = R_{Π}$ and $S_{Π}^{*} = I - 2 Π = S_{Π}$ .

2.1step 1.1F1F4algebra

Expanding with $Π^{2} = Π$ gives $R_{Π}^{2} = 4 Π^{2} - 4 Π + I = I$ and $S_{Π}^{2} = I - 4 Π + 4 Π^{2} = I$ , and the definitions give $R_{Π} = - S_{Π}$ . Hence $R_{Π}^{*} R_{Π} = S_{Π}^{*} S_{Π} = I$ , so both are unitary by [F4].

3.1givenF1step 2.1algebra

If $x = Π y \in ran Π$ , then $Π x = Π^{2} y = x$ , so $R_{Π} x = x$ and $S_{Π} x = - x$ . If $x \in \ker Π$ , then $Π x = 0$ , so $R_{Π} x = - x$ and $S_{Π} x = x$ . Every $v$ splits as $Π v + (I - Π) v$ with the first term in the range and the second in the kernel; [F1] says these subspaces are orthogonal.

4.1L1L2L3step 2.1step 3.1algebra∎

By [L2], $C (S_{Π}) = diag (I_{H}, S_{Π}) = diag (I_{H}, - R_{Π})$ . In the declared control-first order, $Z_{C} = diag (I_{H}, - I_{H})$ , so $Z_{C} C (R_{Π}) = diag (I_{H}, - I_{H}) diag (I_{H}, R_{Π}) = diag (I_{H}, - R_{Π}) = C (S_{Π})$ .

Depends on

Used by

Amplitude amplification with a fixed integer iteration count Algorithm
BBHT search when the marked count is unknown Algorithm
Bounded-error evaluation from a dual adversary certificate Algorithm
Controlled input-consistency reflection from a bit query Algorithm
Known-count Grover search by exact integer maximization Algorithm
Known-count search by randomized Grover iteration Algorithm
One Grover iterate in the standard bit-query model Algorithm
QFT-based amplitude estimation Algorithm
Quantum singular-value transformation circuit Algorithm
A preserved unknown state cannot program its own reflection Counterexample
Amplitude estimation and counting input/output contract Definition
Oblivious ancilla reflection Definition
Prepared unitary and success subspace for amplitude amplification Definition
Amplitude-amplification invariant plane Lemma
Capped randomized amplitude amplification preserves a flagged output Lemma
Effective spectral gap for a product of two reflections Lemma
Robust one-step OAA including ancilla leakage Lemma
Amplitude-amplification access and resource accounting Proposition
Gate and reflection accounting for randomized known-count search Proposition
Amplitude-estimation additive error and success probability Theorem
Dual reflection evaluator has bounded-error correctness Theorem
Exact success probability after amplitude amplification Theorem
Oblivious-amplification block identity Theorem
Projector phase operations from controlled reflections Theorem
QSVT action on singular subspaces Theorem
Qubitization lifts scalar QSP Theorem
Qubitized simulation correctness Theorem
Rank-One Reflection Is Ray-Invariant and Its Signs Differ Under Control Theorem
The controlled input-consistency circuit realizes the exact reflection Theorem

Cited to discharge well-definedness by Orthogonal-Projector Reflection and Access Contract.

Dependency tree · two levels

27 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, arXiv:1907.09415v6 (standard reference, not scraped)
John Preskill, Quantum Computation, Chapter 6: Quantum Algorithms (standard reference, not scraped)