Equality of one-shot reconstruction expectations

Open

QAlgorithms.Papers.Independent.Intakethird100.P66.twoSidedFactorizedAncilla

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

prove2quantum

Let $\mathcal E$ be any CPTP channel on $n\ge1$ qubits. Use the same named uniform frame on reference and output: global Clifford, product single-qubit Clifford, Pauli-6, or a fixed partition into smaller Clifford blocks. Choices on the two registers are independent. Write $Q_{u,b}=U_u^\dagger|b\rangle\langle b|U_u$ and let $\mathcal M^{-1}$ be the actual complex-linear inverse measurement channel. With $\rho_{\Lambda}=2^{-n}\Lambda_{\mathcal E}$ , define

\rho_a=\mathbb E_{u,v}\sum_{b,c}\operatorname{Tr}[\rho_{\Lambda}(Q_{u,b}\otimes Q_{v,c})] \mathcal M^{-1}(Q_{u,b})\otimes\mathcal M^{-1}(Q_{v,c}),

\rho_t=\mathbb E_{u,v}\sum_c\operatorname{Tr}[\mathcal E(Q_{u,0})Q_{v,c}] \mathcal M^{-1}(Q_{u,0}^{T})\otimes\mathcal M^{-1}(Q_{v,c}).

For Pauli-6, the preparation-frame relabeling bit lets fixed outcome zero prepare each of the six eigenstates uniformly. Then

\rho_t=\rho_a.

This equality concerns reconstruction expectations for one fresh repetition per choice. It does not identify individual random snapshots, empirical matrices, or repeated-circuit experiments. Pauli- $Y$ transposition is an ensemble permutation exchanging the two eigenprojectors.

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

/-- Appendix B, PDF pp.14-15, B1-B4: equality of expectation matrices for
one fresh repetition with independent choices on the two registers. The
printed Pauli-Y pointwise transpose equality is replaced by an ensemble
outcome permutation. No empirical-data equality is asserted. -/
theorem twoSidedFactorizedAncilla (n : ℕ) (hn : 0 < n) (F : BasisChoiceFrame n)
    (hF : PaperFrame F) (E : Superop (Qubits n) (Qubits n)) (hE : IsChannel E) :
    twoSidedReconstruction F E = ancillaReconstruction F 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. 15, Appendix B, B1-B4

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 $n$ qubits satisfying the structural condition described below, and every channel $\mathcal E$ from $n$ -qubit matrices to $n$ -qubit matrices, the following two matrices on $2n$ qubits are equal. A basis-choice frame supplies a finite nonempty type $A$ of basis choices and a matrix $Q_{a,b}$ for each $a\in A$ , $b\in\{0,1\}^n$ . Define

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

and let $T_F=\mathcal M_F^{-1}$ if $\mathcal M_F$ is injective, using its inverse complex linear map in that case, and let $T_F$ be the zero linear map otherwise. With

(C_{\mathcal E})_{(u,v),(u',v')}= 2^{-n}\bigl[\mathcal E(|u\rangle\langle u'|)\bigr]_{v,v'},

the asserted equality is

\frac1{|A|^2} \sum_{a,c\in A}\sum_{d\in\{0,1\}^n} \operatorname{Re}\operatorname{Tr}\!\left( Q_{c,d}\,\mathcal E(Q_{a,0^n})\right) \,T_F(Q_{a,0^n}^{\mathsf T})\otimes T_F(Q_{c,d}) = \frac1{|A|^2} \sum_{a,c\in A}\sum_{b,d\in\{0,1\}^n} \operatorname{Re}\operatorname{Tr}\!\left( (Q_{a,b}\otimes Q_{c,d})C_{\mathcal E}\right) \,T_F(Q_{a,b})\otimes T_F(Q_{c,d}),

where real coefficients act as complex scalars and tensor products are indexed by concatenated bit strings. The channel hypothesis means that there exist a natural number $r$ and matrices $K_0,\ldots,K_{r-1}$ with $\sum_jK_j^\dagger K_j=I$ and $\mathcal E(X)=\sum_jK_jXK_j^\dagger$ for every matrix $X$ . The structural condition on $F$ allows either the Pauli frame, or a frame built by finitely tensoring global Clifford frames and the zero-qubit Pauli frame. In the Pauli frame, $a=(A_j,s_j)_{j<n}$ with $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, chooses a representative $U_a$ of each class, and sets $Q_{a,b}=U_a^\dagger|b\rangle\langle b|U_a$ ; the Pauli subgroup is the subgroup generated by all Pauli tensors with phases $1,i,-1,-i$ . Tensoring frames takes the product of their basis-choice types and the tensor product of their matrices. The zero-qubit frame has one basis choice, one outcome, and matrix $1$ . The left-hand sum specifically uses only the all-false outcome $0^n$ for its first frame factor.

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