Two-qudit reconstruction coefficients and endpoint maps

Open

QAlgorithms.Papers.Independent.Intakethird100.P71.twoQudit_reconstruction

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

prove2quantum

Let $N=2$ , $d\ge2$ , and let a locally scrambled projective experiment have second features $(1,w,w,1)$ in region order $\varnothing,\{1\},\{2\},\{1,2\}$ , with $2d/(d^2+1)\le w\le1$ . Its unique coefficient solution is

\begin{aligned}r_\varnothing&=\frac{d^3w-3d^2+3dw-2w^2+1}{(dw-1)(d^2-2dw+1)},\\r_{\{1\}}=r_{\{2\}}&=\frac{-d^4w+2d^3-2d+w}{d(dw-1)(d^2-2dw+1)},\\r_{\{1,2\}}&=\frac{(d^2-1)^2}{d^2(d^2-2dw+1)}.\end{aligned}

The constructed map $\mathcal R_w(X)=d^2\sum_A r_A X_A$ is a two-sided inverse of the measurement channel. At the endpoints,

\mathcal R_1=\mathcal L_d\otimes\mathcal L_d,\qquad \mathcal L_d(X)=(d+1)X-\operatorname{Tr}(X)I,\qquad \mathcal R_{2d/(d^2+1)}(X)=(d^2+1)X-\operatorname{Tr}(X)I.

For product inputs the local endpoint is $\mathcal L_d(X)\otimes\mathcal L_d(Y)$ . The tensor-of-maps formulation covers correlated inputs without factoring their marginals.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P71

Formal statement

noncomputable section

open MeasureTheory

open scoped Matrix ComplexConjugate ENNReal Matrix.Norms.Elementwise

namespace QAlgorithms.Papers.Independent.Intakethird100.P71

attribute [local instance] Classical.propDecidable

local notation "Config" n:max d:max =>
  QAlgorithms.Papers.Independent.Information100.P21.Config (P := Fin n) (fun _ => d)

local notation "Op" n:max d:max =>
  QAlgorithms.Papers.Independent.Information100.P21.Op (Config n d)

attribute [local instance] QAlgorithms.Papers.Independent.Intakethird100.P71.matrixContinuousENorm

local notation "Unitary" n:max d:max => Matrix.unitaryGroup (Config n d) ℂ

local notation "Local" n:max d:max => Fin n → Matrix.unitaryGroup (Fin d) ℂ

open QAlgorithms.Papers.Independent.Information100.P63 (tensorPower)

/-- PDF pp.5–6 Eqs.(24)–(28): exact toy-model coefficients and the local/global
endpoint superoperators. Eq.(27) is a tensor of maps on general inputs, with a
product-input specialization; Eq.(28) contains Tr(X) I on arbitrary X. -/
theorem twoQudit_reconstruction {d : ℕ} (hd : 2 ≤ d) (E : ProjectiveEnsemble 2 d)
    (hls : LocallyScrambled (prior E)) (w : ℝ)
    (hw : 2*(d : ℝ)/((d : ℝ)^2+1) ≤ w ∧ w ≤ 1) (hf : ToyFeature (prior E) w) :
    CoefficientSystem (prior E) (toyCoefficients d w) ∧
    (∀ r, CoefficientSystem (prior E) r → r = toyCoefficients d w) ∧
    (∀ X : Op 2 d,
      efReconstruct (toyCoefficients d w) (snapshotMeasurementMap (prior E) X) = X ∧
      snapshotMeasurementMap (prior E) (efReconstruct (toyCoefficients d w) X) = X) ∧
    (∀ X : Op 2 d, efReconstruct (toyCoefficients d 1) X =
      QAlgorithms.piSuperop (fun _ : Fin 2 => oneSiteInverse d) X) ∧
    (∀ X Y : Matrix (Fin d) (Fin d) ℂ,
      efReconstruct (toyCoefficients d 1) (twoSiteProduct X Y) =
        twoSiteProduct (oneSiteInverse d X) (oneSiteInverse d Y)) ∧
    (∀ X : Op 2 d,
      efReconstruct (toyCoefficients d (2*(d : ℝ)/((d : ℝ)^2+1))) X =
        ((d : ℂ)^2+1) • X - X.trace • 1) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P71

end

Source

Classical Shadow Tomography with Locally Scrambled Quantum Dynamics, arXiv:2107.04817v4, PDF p. 5, §II C, Eqs.(24)–(28): two-qudit reconstruction coefficients

Read-back

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

Let $d\ge2$ be a natural number, let $\mathcal X=\{0,\ldots,d-1\}^2$ , and let $E$ supply a probability law $\lambda$ on unitary matrices on $\mathbb C^{\mathcal X}$ . Put $\nu=d^{-2}\sum_b(U\mapsto U^\dagger|b\rangle\langle b|U)_*\lambda$ , and assume that $\nu$ is invariant under $S\mapsto(V_0\otimes V_1)^\dagger S(V_0\otimes V_1)$ for all local unitary matrices $V_0,V_1$ . For $A\subseteq\{0,1\}$ , let $\operatorname{Tr}_{A^c}X$ be the partial trace obtained by summing matching complementary row and column indices, let $R_A(X)$ have entries $d^{-(2-|A|)}(\operatorname{Tr}_{A^c}X)_{x|_A,y|_A}$ when $x,y$ agree outside $A$ and $0$ otherwise, and define $f(A)=\int\operatorname{Re}\operatorname{tr}((\operatorname{Tr}_{A^c}S)^2)\,d\nu(S)$ . Let $w\in\mathbb R$ satisfy $2d/(d^2+1)\le w\le1$ , and assume $f(A)=w$ for every singleton $A$ and $f(A)=1$ for the empty and full subsets. Define

r_w(A)= \begin{cases} \dfrac{d^3w-3d^2+3dw-2w^2+1}{(dw-1)(d^2-2dw+1)},&|A|=0,\\[4pt] \dfrac{-d^4w+2d^3-2d+w}{d(dw-1)(d^2-2dw+1)},&|A|=1,\\[4pt] \dfrac{(d^2-1)^2}{d^2(d^2-2dw+1)},&|A|=2, \end{cases} \qquad \mathcal E_r(X)=d^2\sum_A r(A)R_A(X),

and $\mathcal M(X)_{ij}=\sum_{k,l}(\int d^2S_{ij}S_{lk}\,d\nu(S))X_{kl}$ . The theorem states that $r_w$ satisfies the equations

\sum_{A,C}r(A) \left(\frac{d^3}{d^2-1}\right)^2 \left(\sum_{\substack{D\subseteq\{0,1\}\\B=A\cap D}} d^{-|D|}(-1/d)^{|C\triangle D|}\right)f(C) =\mathbf1_{\{B=\{0,1\}\}}

for every $B$ , and that every real function $r$ satisfying these equations equals $r_w$ . For every complex matrix $X$ , $\mathcal E_{r_w}(\mathcal M(X))=X$ and $\mathcal M(\mathcal E_{r_w}(X))=X$ . In addition, putting $\ell_d(X)=(d+1)X-\operatorname{tr}(X)I$ , the map $\mathcal E_{r_1}$ equals the linear map $\ell_d\otimes\ell_d$ , meaning that it sends each matrix unit $E_{ab}\otimes E_{cd}$ to $\ell_d(E_{ab})\otimes\ell_d(E_{cd})$ ; in particular $\mathcal E_{r_1}(X\otimes Y)=\ell_d(X)\otimes\ell_d(Y)$ for all $d\times d$ complex matrices $X,Y$ . Finally, for every $X$ ,

\mathcal E_{r_{\,2d/(d^2+1)}}(X)=(d^2+1)X-\operatorname{tr}(X)I.

These last identities use the indicated endpoint coefficients regardless of the value of the given $w$ .

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