ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedprecheck passjudge 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.

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.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

60 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

John Watrous, The Theory of Quantum Information (2018), §2.3.2 (standard reference, not scraped)
John Preskill, Quantum Computation, Chapter 3: Foundations II: Measurement and Evolution, §3.1.1 (standard reference, not scraped)