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

Zero-probability Pauli measurement branch

Statement

Let $H$ be a nonzero finite-dimensional complex inner-product space, let $ρ$ be a density operator on $H$ , and let $M$ be a Hermitian Pauli observable on $H$ with $M^{2} = I_{H}$ . For $b \in {0, 1}$ put $P_{b} = (I_{H} + (- 1)^{b} M) / 2$ and $p_{b} = Tr (ρ P_{b})$ . If $p_{b} = 0$ , then $P_{b} ρ P_{b} = 0$ . The outcome has probability zero and, under the conditional-state convention, has no normalized conditional state.

Facts & Assumptions

Given: The $H, ρ, M, b, P_{b}, p_{b}$ data of the Statement, with $p_{b} = 0$ .

[F1]

The setup defines $P_{b} = (I_{H} + (- 1)^{b} M) / 2$ and $p_{b} = Tr (ρ P_{b})$ .

[F2]

Pauli measurement projectors and total probability: $P_{b}^{*} = P_{b}$ and $P_{b}^{2} = P_{b}$ .

[A1]

Density operator: $ρ$ is a nonnegative endomorphism on a nonzero finite-dimensional complex inner-product space.

[F3]

For $A \in M_{m \times n} (F)$ and $B \in M_{n \times m} (F)$ , $tr (A B) = tr (B A)$ : trace is cyclic for compatible finite-dimensional endomorphisms.

[F4]

A non-negative operator is equivalently self-adjoint with nonnegative eigenvalues, a positive semidefinite matrix in an orthonormal basis, or an operator of the form S^*S: a nonnegative endomorphism has an orthonormal eigenbasis with nonnegative real eigenvalues.

[F5]

The basis-independent trace of an endomorphism of a finite-dimensional vector space: trace is basis-independent and equals the matrix trace in any ordered basis.

Proof

Given: The data in the Statement.

1.1givenF2A1algebra

Set $Q_{b} = P_{b} ρ P_{b}$ . For every $v$ , self-adjointness of $P_{b}$ in [F2] gives $⟨ Q_{b} v, v ⟩ = ⟨ ρ P_{b} v, P_{b} v ⟩ \geq 0$ by [A1]. Thus $Q_{b}$ is nonnegative.

1.2givenF1F2F3F4F5algebra

By [F1], [F2], and cyclicity [F3], $Tr (Q_{b}) = Tr (P_{b} ρ P_{b}) = Tr (ρ P_{b}^{2}) = p_{b} = 0$ . By [F4], choose an orthonormal eigenbasis of $Q_{b}$ whose eigenvalues are nonnegative; [F5] expresses its trace as their finite sum. A finite sum of nonnegative reals is zero only when each term is zero, so $Q_{b} = 0$ .

2.1givenstep 1.2algebra∎

The branch output is therefore zero. Normalization would require dividing it by $p_{b} = 0$ , which is undefined; the conditional-state convention assigns no state to this zero-probability outcome.

Sources

De Wolf §20.3, PDF pp. 187–188, separates deterministic outcomes from random outcomes; Watrous Lesson 14 §14.1, printed pp. 405–407 (PDF pp. 411–413), specifies the two projective branches. The zero-trace implication is proved locally using the finite spectral theorem.

Depends on

Used by

Dependency tree · two levels

30 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, §20.3 (standard reference, not scraped)
John Watrous, Understanding Quantum Information and Computation, Lesson 14 (standard reference, not scraped)