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.

Channels, Kraus, Choi, and Stinespring Representations — Examples

1 · Prerequisites

2 · Summary

The worked qubit phase-flip family uses Kraus operators $\sqrt{p} I$ and $\sqrt{1 - p} Z$ for $0 \leq p \leq 1$ . Its action multiplies off-diagonal entries by $2 p - 1$ , so $p = 1 / 2$ is complete dephasing. The Choi calculation uses the same input-first/output-second order as the A page and explicitly checks positivity and the output partial trace.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-adaptedjudge pass (gpt-6-luna)Open item page →

Qubit dephasing channel in Kraus and Choi forms

Example

Let $H = C^{2}$ with standard basis $e_{0}, e_{1}$ , let $0 \leq p \leq 1$ , and put $Z = (\begin{array}{cc} 1 & 0 \\ 0 & - 1 \end{array})$ , $K_{0} = \sqrt{p} I$ , and $K_{1} = \sqrt{1 - p} Z$ , using the nonnegative real square roots. For $Φ (X) = K_{0} X K_{0}^{†} + K_{1} X K_{1}^{†}$ , compute the Kraus normalization, the action on a density matrix, and the Choi matrix in the input-first/output-second convention. The map is a phase-flip family; at $p = 1 / 2$ it is the completely dephasing channel.

Facts & Assumptions

Given: $p \in [0, 1]$ , $H = C^{2}$ with its standard orthonormal basis, $Z = diag (1, - 1)$ , and the displayed finite Kraus family.

[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: $(e_{0}, e_{1})$ is orthonormal.

[F2]

Finite Kraus representation: $Φ (X) = \sum_{j = 0}^{1} K_{j} X K_{j}^{†}$ .

[F3]

Choi matrix with input factor first: $J (Φ) = \sum_{i, j = 0}^{1} E_{i j} \otimes Φ (E_{i j})$ , with input first.

[F4]

Finite channel, Kraus, Choi, and Stinespring equivalence: a map is a channel exactly when its Choi operator is non-negative and its output partial trace is the input identity; the finite Kraus and Stinespring conditions are equivalent as well.

[F5]

Trace preservation is Kraus normalization: the Kraus sum is trace-preserving when its adjoint-square sum is the identity.

[F6]

Non-negative and positive operators: non-negativity means self-adjointness and nonnegative quadratic form.

[F7]

In orthonormal bases, the matrix of the adjoint is the conjugate transpose of the matrix: in the standard orthonormal basis the adjoint matrix is the conjugate transpose.

[F8]

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

[F9]

Partial trace over a finite tensor factor and The partial trace is characterized by the trace pairing and is basis-independent: for the input-first/output-second basis, the output partial trace sums entries with the same output index.

[F10]

The product basis is orthonormal and tensor dimensions multiply: the ordered product basis of $H \otimes H$ is orthonormal and has dimension four.

[F11]

Density operator: a density operator is a non-negative endomorphism with trace one.

Verification

1.1givenF1F2F5F6F7F8F11algebra

The matrix $Z$ is real and diagonal, so [F7] gives $Z^{†} = Z$ and $Z^{2} = I$ by direct multiplication [F8]. Thus $K_{0}^{†} K_{0} + K_{1}^{†} K_{1} = p I + (1 - p) I = I$ , and [F5] makes $Φ$ trace-preserving on all operators. By [F11], a density operator $ρ$ is non-negative and has trace one. Self-adjointness gives the matrix form $ρ = (\begin{array}{cc} a & b \\ \overline{b} & d \end{array})$ with real $a, d$ ; non-negativity applied to $e_{0}, e_{1}$ gives $a, d \geq 0$ , and trace one gives $a + d = 1$ . Direct multiplication gives $Φ (ρ) = p ρ + (1 - p) Z ρ Z = (\begin{array}{cc} a & (2 p - 1) b \\ (2 p - 1) \overline{b} & d \end{array})$ . For every $x$ , its quadratic form is $⟨ Φ (ρ) x, x ⟩ = p ⟨ ρ x, x ⟩ + (1 - p) ⟨ ρ Z x, Z x ⟩ \geq 0$ ; the displayed matrix is self-adjoint, and its trace is $a + d = 1$ . Thus the output is a density operator. These formulas include $p = 0$ and $p = 1$ .

1.2givenF1F3F6F8F10algebra

Put $λ = 2 p - 1$ . Direct application of $Z$ to the four matrix units gives $Φ (E_{00}) = E_{00}$ , $Φ (E_{11}) = E_{11}$ , $Φ (E_{01}) = λ E_{01}$ , and $Φ (E_{10}) = λ E_{10}$ . By [F3], in the ordered basis $(e_{0} \otimes e_{0}, e_{0} \otimes e_{1}, e_{1} \otimes e_{0}, e_{1} \otimes e_{1})$ , $J (Φ) = (\begin{array}{cccc} 1 & 0 & 0 & λ \\ 0 & 0 & 0 & 0 \\ 0 & 0 & 0 & 0 \\ λ & 0 & 0 & 1 \end{array}) .$ The vectors $(e_{0} \otimes e_{0} \pm e_{1} \otimes e_{1}) / \sqrt{2}$ have eigenvalues $1 \pm λ = 2 p, 2 (1 - p)$ , and the other two product basis vectors have eigenvalue zero. Since $p \in [0, 1]$ , every eigenvalue is nonnegative; the matrix is self-adjoint, so [F6] makes $J (Φ)$ non-negative.

2.1givenF4F9F10step 1.1step 1.2algebra∎

In the product basis, the output partial-trace entry $(i, j)$ is $\sum_{α = 0}^{1} J (Φ)_{(i, α), (j, α)}$ by [F9]. The displayed matrix in step 1.2 therefore gives diagonal entries $1, 1$ and off-diagonal entries $0, 0$ , so ${Tr}_{K} J (Φ) = I_{H}$ . The Choi positivity from step 1.2 and this partial-trace identity imply by [F4] that $Φ$ is a channel; step 1.1 separately verifies the Kraus normalization and density matrix action required in the Example.