Unbiased full Choi snapshots

Open

QAlgorithms.Papers.Independent.Intakethird100.P66.unbiasedChoiSnapshots

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $\mathcal E$ be any CPTP map on $n\ge1$ qubits with normalized reference-first Choi state $\rho_{\Lambda}=2^{-n}\Lambda_{\mathcal E}$ . Fix an ideal Pauli-6, global Clifford, or fixed block-factorized measurement frame independently of $\mathcal E$ . Draw a fresh uniform basis $U$ and its computational Born outcome $b$ on $\rho_{\Lambda}$ . Using the actual linear inverse measurement channel, form

\widehat\Lambda=2^n\mathcal M^{-1}(U^\dagger|b\rangle\langle b|U).

Then

\mathbb E[\widehat\Lambda]=\Lambda_{\mathcal E}.

The global inverse acts in dimension $2^{2n}$ , while the external factor is $2^n$ . Individual snapshots may be indefinite and need not be CPTP or pure. This unbiased representation underlies linear prediction; no preservation of expectation by nonlinear postprocessing is asserted.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P66

Formal statement

noncomputable section

open MeasureTheory QAlgorithms ClassicalShadows

open scoped Matrix ComplexConjugate ENNReal

namespace QAlgorithms.Papers.Independent.Intakethird100.P66

attribute [local instance] Classical.propDecidable Classical.typeDecidableEq

/-- Section II, PDF p.2, Eq.(7), PDF p.4: one unbiased unnormalized Choi
snapshot for any CPTP process. A snapshot need not be positive, pure or CPTP. -/
theorem unbiasedChoiSnapshots (n : ℕ) (hn : 0 < n) (F : BasisChoiceFrame (n + n))
    (hF : PaperFrame F) (E : Superop (Qubits n) (Qubits n)) (hE : IsChannel E) :
    meanChoiSnapshot F E = processChoi E := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P66

end

Source

Classical Shadows for Quantum Process Tomography on Near-term Quantum Computers, arXiv:2110.02965v3, PDF p. 2, Section II; Eq.(7) on PDF p.4

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For every natural number $n>0$ , every basis-choice frame $F$ on $2n$ qubits satisfying the structural condition below, and every channel $\mathcal E$ on $n$ -qubit matrices, the weighted mean of the scaled frame snapshots equals the unnormalized Choi matrix:

\sum_{a\in A}\sum_{b\in\{0,1\}^{2n}} \frac{\operatorname{Re}\operatorname{Tr}(Q_{a,b}C_{\mathcal E})}{|A|} \,2^n T_F(Q_{a,b}) =J_{\mathcal E}, \qquad (J_{\mathcal E})_{(u,v),(u',v')} =\bigl[\mathcal E(|u\rangle\langle u'|)\bigr]_{v,v'}, \qquad C_{\mathcal E}=2^{-n}J_{\mathcal E}.

Here $A$ is the finite nonempty type of basis choices supplied by $F$ , $Q_{a,b}$ is its matrix for basis choice $a$ and outcome string $b$ , paired strings are identified with their concatenation, and real weights are used as complex scalar coefficients. The map $T_F$ is the inverse of the complex linear map

\mathcal M_F(X)=\frac1{|A|} \sum_{a\in A}\sum_{b\in\{0,1\}^{2n}} \operatorname{Tr}(Q_{a,b}X)\,Q_{a,b}

when that map is injective, and is defined to be the zero linear map otherwise. The channel hypothesis requires a finite Kraus representation $\mathcal E(X)=\sum_{j=0}^{r-1}K_jXK_j^\dagger$ for every matrix $X$ , for some $r\in\mathbb N$ , with $\sum_jK_j^\dagger K_j=I$ . The allowed structural condition on $F$ is that it is either the Pauli frame, or a frame obtained by finitely tensoring global Clifford frames and the zero-qubit Pauli frame. The Pauli frame on $m$ qubits has choices $a=(A_j,s_j)_{j<m}$ , $A_j\in\{X,Y,Z\}$ , $s_j\in\{-1,1\}$ , and $Q_{a,b}=\bigotimes_j(I+s_j(-1)^{b_j}A_j)/2$ . A global Clifford frame on $m$ qubits uses a supplied finite enumeration of the quotient of the unitary Pauli normalizer by equality of conjugation maps $X\mapsto UXU^\dagger$ , chooses a representative $U_a$ of each class, and uses $Q_{a,b}=U_a^\dagger|b\rangle\langle b|U_a$ ; the normalized subgroup is generated by all $m$ -qubit Pauli tensors with phases $1,i,-1,-i$ . Tensoring frames forms product basis-choice types and tensor products of their matrices, and the zero-qubit frame has one choice, one outcome, and matrix $1$ .

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph