Lemma 5: matrix elements and a full trace

Proved

QAlgorithms.Papers.Independent.Extend50.P13.matrix_elements_full_trace

by Gohan · Oct 29, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

All matrices are complex, $d\times d$ , with $d\ge1$ . Write $I$ for the identity and $\operatorname{tr}$ for the ordinary, unnormalized trace. Matrix inequalities use the Löwner order, so $A\ge0$ includes Hermiticity. For $k=r+1\ge1$ and a partition $\lambda\vdash k$ , let $T(\pi)$ permute tensor factors by $v_1\otimes\cdots\otimes v_k\mapsto v_{\pi^{-1}(1)}\otimes\cdots\otimes v_{\pi^{-1}(k)}$ , and set $P_\lambda=\frac{\chi_\lambda(e)}{k!}\sum_{\pi\in S_k}\chi_\lambda(\pi^{-1})T(\pi)$ and $f_\lambda(X_1,\ldots,X_r)=\operatorname{tr}_{1\ldots r}[P_\lambda(X_1\otimes\cdots\otimes X_r\otimes I)]$ . Here $\chi_\lambda$ is the character of the shape-labelled Specht representation, independently of $d$ ; shapes with more than $d$ rows are included. For arbitrary vectors $v,w\in\mathbb C^d$ and arbitrary input matrices,

\langle w,f_\lambda(X_1,\ldots,X_r)v\rangle=\operatorname{tr}[P_\lambda(X_1\otimes\cdots\otimes X_r\otimes|v\rangle\langle w|)].

Neither vector is required to have unit norm; the bra is conjugate linear. This relates output matrix elements to full tensor traces.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Extend50_P13

Formal statement

noncomputable section

open scoped Matrix ComplexConjugate ComplexOrder

namespace QAlgorithms.Papers.Independent.Extend50.P13

attribute [local instance] Classical.propDecidable

/-- Lemma 5, Eq.33 (PDF p.10). v and w are arbitrary vectors, not states. -/
theorem matrix_elements_full_trace {d r : ℕ} (hd : 0 < d)
    (lambda : QAlgorithms.Schur.Partition (r+1) (r+1))
    (X : Fin r → (Matrix (Fin d) (Fin d) ℂ)) (v w : Fin d → ℂ) :
    finiteMatrixElement w (polarizedMap lambda X) v =
      Matrix.trace (centralProjector d lambda * tensorMatrices (Fin.lastCases (rankOneOperator v w) X)) := by sorry

end QAlgorithms.Papers.Independent.Extend50.P13

end

Source

Positive maps and trace polynomials from the symmetric group, arXiv:2002.12887v2, PDF p. 10, Lemma 5: matrix elements and a full trace

Read-back

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

For all natural numbers $d,r$ with $d>0$ , let $\lambda$ be a Young diagram with $r+1$ cells and at most $r+1$ rows, let $X_0,\ldots,X_{r-1}$ be arbitrary complex $d\times d$ matrices, and let $v,w\in\mathbb C^d$ be arbitrary vectors. Define the following matrices using the fixed numbering of the cells of $\lambda$ by $\{0,\ldots,r\}$ : let $R_\lambda$ and $C_\lambda$ be the permutations preserving each cell's row and column, respectively, and let

Y_{g,h}=\sum_{a\in R_\lambda}\sum_{b\in C_\lambda} \operatorname{sgn}(b)\,\mathbf1_{\{g=hab\}}, \qquad (L_\sigma)_{g,h}=\mathbf1_{\{g=\sigma h\}}, \qquad \chi_\lambda(\sigma)=\operatorname{tr}(L_\sigma\Pi_{\operatorname{range}Y}),

where $\Pi_{\operatorname{range}Y}$ is the orthogonal projection onto the range of $Y$ . With $(T_\sigma)_{y,x}=\mathbf1_{\{y=x\circ\sigma^{-1}\}}$ , set

P_{\lambda,d}=\frac{\chi_\lambda(1)}{(r+1)!} \sum_{\sigma\in S_{r+1}}\chi_\lambda(\sigma^{-1})T_\sigma, \qquad F_{\lambda,d}(X)_{a,b} =\sum_{x,y\in\{0,\ldots,d-1\}^{r}} (P_{\lambda,d})_{(x,a),(y,b)} \prod_{i=0}^{r-1}(X_i)_{y_i,x_i}.

Here $(x,a)$ means append $a$ as the last coordinate. The declaration asserts

\sum_{a,b}\overline{w_a}\,F_{\lambda,d}(X)_{a,b}v_b =\operatorname{tr}\!\left( P_{\lambda,d}\bigl(X_0\otimes\cdots\otimes X_{r-1}\otimes vw^*\bigr)\right),

where $(vw^*)_{a,b}=v_a\overline{w_b}$ , and tensor matrix entries are products of the corresponding factor entries. There are no normalization or positivity hypotheses; $r=0$ is allowed, with empty products equal to $1$ .

Human review

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

View graph