Sitewise factorization of the fusion tensor

Open

QAlgorithms.Papers.Independent.Intakethird100.P71.fusion_siteFactorization

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

prove2quantum

Let $N\ge0$ , $d\ge2$ , and let $A,B,C$ be arbitrary regions. Define

f_{A,B,C}=\left(\frac{d^3}{d^2-1}\right)^N\sum_D\delta_{B,A\cap D}\,d^{-|D|}\left(-\frac1d\right)^{|C\triangle D|}.

For $a_i=\mathbf1_{i\in A}$ , $b_i=\mathbf1_{i\in B}$ , and $c_i=\mathbf1_{i\in C}$ ,

f_{A,B,C}=\prod_i f_{a_i,b_i,c_i}.

The local tensor has pairs indexed by $c=0,1$ : $f_{0,0,:}=(d,0)$ , $f_{0,1,:}=(0,0)$ , $f_{1,0,:}=(d^3,-d^2)/(d^2-1)$ , and $f_{1,1,:}=(-d,d^2)/(d^2-1)$ . At $N=0$ both expressions equal one. This factorizes the fusion tensor; it supplies no bound on the bond dimension of the reconstruction-coefficient solution.

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 p.22 Eqs.(C9)–(C10): the regional fusion coefficient equals the
product of its site tensors. At N=0 both sides are one. This gives no
bond-dimension bound or convergence guarantee for the solution r. -/
theorem fusion_siteFactorization {n d : ℕ} (hd : 2 ≤ d) (A B C : Finset (Fin n)) :
    fusion n d A B C =
      ∏ i : Fin n, fusionSite d (decide (i ∈ A)) (decide (i ∈ B)) (decide (i ∈ C)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P71

end

Source

Classical Shadow Tomography with Locally Scrambled Quantum Dynamics, arXiv:2107.04817v4, PDF p. 22, Appendix C.3, Eqs.(C9)–(C10): sitewise fusion tensor

Read-back

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

For every pair of natural numbers $n,d$ with $d\ge 2$ , and every three subsets $A,B,C$ of $I_n=\{0,\ldots,n-1\}$ , the following identity holds:

\left(\frac{d^3}{d^2-1}\right)^n \sum_{\substack{D\subseteq I_n\\ B=A\cap D}} d^{-|D|} \left(-\frac1d\right)^{|C\triangle D|} = \prod_{i\in I_n} F_d\bigl(\mathbf1_A(i),\mathbf1_B(i),\mathbf1_C(i)\bigr),

where $\triangle$ denotes symmetric difference, $\mathbf1_A(i)$ is $1$ when $i\in A$ and $0$ otherwise, and the factor $F_d$ is given by

F_d(a,b,c)= \begin{cases} \dfrac{d^2}{d^2-1}, &(a,b,c)=(1,1,1),\\[2pt] -\dfrac{d}{d^2-1}, &(a,b,c)=(1,1,0),\\[2pt] -\dfrac{d^2}{d^2-1}, &(a,b,c)=(1,0,1),\\[2pt] \dfrac{d^3}{d^2-1}, &(a,b,c)=(1,0,0),\\[2pt] d, &(a,b,c)=(0,0,0),\\ 0, &\text{otherwise}. \end{cases}

All arithmetic in this identity is real. The sets may be empty, and an empty sum is $0$ . The case $n=0$ is included: then $A=B=C=\varnothing$ , the sum has its single term $D=\varnothing$ , and both sides equal $1$ , with the product interpreted as an empty product.

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