ExampleConstruction: Literature-sourcedVerification: 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.

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.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

62 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.2.3 (standard reference, not scraped)
John Preskill, Quantum Computation, Chapter 3, §3.4.2 (standard reference, not scraped)