Pipeline-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.

✓ 1 result · all verified · 1 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs; all 1 also cleared it.

Measurements, POVMs, and Instruments — Examples

1 · Prerequisites

2 · Summary

This example computes a two-outcome projective measurement and its Lüders instrument on a qubit state. One branch has probability zero and zero output, so the conditional value is the explicit no-state symbol $⊥$ .

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

A projective measurement branch with probability zero

Example

On $H = C^{2}$ with its standard inner product, consider

$P_{0} = (\begin{array}{cc} 1 & 0 \\ 0 & 0 \end{array}), P_{1} = (\begin{array}{cc} 0 & 0 \\ 0 & 1 \end{array}), ρ = P_{0} .$

For the two-outcome projective measurement $(P_{0}, P_{1})$ , the outcome probabilities are $1$ and $0$ . Its Lüders instrument has a zero output on outcome $1$ , so that branch has no conditioned density operator.

Facts & Assumptions

Given: The standard complex inner product on $H = C^{2}$ , the displayed matrices, and the definitions and results cited below.

[F1]

The standard formulas $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ and $\sum_{k < n} x_{k} \overline{y_{k}}$ on $C^{n}$ are inner products: on $C^{2}$ , $⟨ x, y ⟩ = x_{0} \overline{y_{0}} + x_{1} \overline{y_{1}}$ , linear in the first argument.

[F2]

Finite-dimensional vector space, and its dimension $\dim_{F} V$ ; infinite-dimensional means having no finite basis: $C^{2}$ is a nonzero finite-dimensional space of dimension two.

[F3]

Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes: matrix products use row-by-column sums and the identity matrix acts as the identity.

[F4]

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

[F5]

Non-negative and positive operators: a nonnegative operator is self-adjoint and has nonnegative quadratic form on every vector.

[F6]

Density operator: on nonzero finite-dimensional $H$ , a density operator is nonnegative and has trace one.

[F7]

Finite projective measurements: a projective measurement is a finite family of pairwise orthogonal self-adjoint projections summing to the identity.

[F8]

Finite POVMs and their outcome law: a finite POVM is a family of nonnegative operators summing to the identity, with weights $tr (ρ E_{a})$ .

[F9]

Projective measurement outcome weights are probabilities: the projective outcome weights $tr (ρ P_{a})$ form a probability distribution.

[F10]

The square-root Lüders maps form an instrument: the maps $X \mapsto E_{a}^{1 / 2} X E_{a}^{1 / 2}$ form an instrument for a finite POVM.

[F11]

Finite instruments and conditional states: the conditional value is the normalized branch output for positive weight and $⊥$ at zero weight.

[F12]

A zero-probability instrument branch has no conditioned state: a zero-weight instrument branch has zero output and no conditioned density operator.

[F13]

The basis-independent trace of an endomorphism of a finite-dimensional vector space: the trace is the sum of the diagonal entries of an endomorphism matrix.

[F14]

A non-negative operator has a unique non-negative square root: every nonnegative operator has a unique nonnegative square root.

Verification

1.1givenF1F3F4F5

For $x = (x_{0}, x_{1})$ and $y = (y_{0}, y_{1})$ , [F1] gives $⟨ P_{0} x, y ⟩ = x_{0} \overline{y_{0}} = ⟨ x, P_{0} y ⟩$ and $⟨ P_{1} x, y ⟩ = x_{1} \overline{y_{1}} = ⟨ x, P_{1} y ⟩$ . By [F4], both matrices are self-adjoint. Direct multiplication [F3] gives $P_{0}^{2} = P_{0}$ , $P_{1}^{2} = P_{1}$ , $P_{0} P_{1} = P_{1} P_{0} = 0$ , and $P_{0} + P_{1} = I$ . Their quadratic forms are $∣ x_{0} ∣^{2}$ and $∣ x_{1} ∣^{2}$ , which are nonnegative by [F1]; hence both are nonnegative by [F5].

2.1givenF2F6F13step 1.1

The matrix $ρ = P_{0}$ is nonnegative by step 1.1 and has trace $1$ by [F13]. Since $H$ is nonzero and finite-dimensional by [F2], [F6] makes $ρ$ a density operator.

2.2givenF5F7F8step 1.1

The identities in step 1.1 show that $(P_{0}, P_{1})$ is a projective measurement by [F7]. Each $P_{a}$ is nonnegative and the pair sums to $I$ , so $E_{a} = P_{a}$ is also a finite POVM by [F8].

3.1givenF3F9F13step 2.1

The outcome weights are $p_{0} = tr (ρ P_{0}) = tr (P_{0}^{2}) = 1$ and $p_{1} = tr (ρ P_{1}) = tr (P_{0} P_{1}) = 0$ , using [F3] and [F13]. They are probabilities by [F9].

3.2givenF8F10F14step 1.1step 2.2

Since each $P_{a}$ is nonnegative and satisfies $P_{a}^{2} = P_{a}$ by step 1.1, uniqueness of the nonnegative square root [F14] gives $P_{a}^{1 / 2} = P_{a}$ . Applying [F10] to $E_{a} = P_{a}$ therefore gives the Lüders branch maps $I_{a} (X) = P_{a} X P_{a}$ and proves that they form an instrument.

4.1givenF3F11F12step 2.1step 3.1step 3.2∎

Matrix multiplication [F3] gives $I_{0} (ρ) = P_{0}$ and $I_{1} (ρ) = P_{1} P_{0} P_{1} = 0$ . Thus $I_{0} (ρ) / p_{0} = P_{0}$ is a density operator by steps 2.1 and 3.1, whereas [F11] assigns $⊥$ to the outcome- $1$ conditional value because $p_{1} = 0$ . The zero-branch theorem [F12] confirms that no conditional density operator is assigned there.