Appendix B: conversion from the R basis to permutation coefficients, Eq.(B5)

Proved

QAlgorithms.Papers.Independent.Extend50.P12.werner_permutation_coefficients_corrected

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

prove2quantum

Let $d\ge1$ and let $c_+,c_-,c_0,c_1,c_2,c_3$ be real. Using the six explicitly defined operators $R_+,R_-,R_0,R_1,R_2,R_3$ in Eq. (27), construct $\rho=\sum_j c_jR_j$ , and assume that $\rho$ is PSD with trace one. Then

\rho=\alpha_1I+\alpha_2V(12)+\alpha_3V(23)+\alpha_4V(31)+\alpha_5V(123)+\alpha_6V(321),

where the physical permutation action is the one in Eq. (2), and

\begin{aligned} \alpha_1&=c_+/6+c_-/6+2c_0/3,& \alpha_2&=c_+/6-c_-/6-c_1/3+c_2/\sqrt3,\\ \alpha_3&=c_+/6-c_-/6+2c_1/3,& \alpha_4&=c_+/6-c_-/6-c_1/3-c_2/\sqrt3,\\ \alpha_5&=c_+/6+c_-/6-c_0/3+i c_3/\sqrt3,& \alpha_6&=c_+/6+c_-/6-c_0/3-i c_3/\sqrt3. \end{aligned}

Here $i$ is the imaginary unit. This identity converts the two specified expansions of the same constructed Werner density matrix. It does not assert uniqueness of permutation coefficients at small $d$ .

Formalization Note The displayed $\alpha_2$ corrects the printed Eq. (B5), which omits $-c_1/3$ and has the wrong sign on $c_2/\sqrt3$ . Both changes are forced directly by the defining $R_1,R_2$ in Eq. (27), and require independent moderation.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Extend50_P12

Formal statement

noncomputable section

open scoped BigOperators Matrix ComplexOrder

namespace QAlgorithms.Papers.Independent.Extend50.P12

attribute [local instance] Classical.propDecidable

/-- Appendix B, PDF p.13, Eqs.(B3)-(B5), using the R definitions on p.5, Eq.(27).
SOURCE CORRECTION: the printed alpha_2=c_+/6-c_minus/6-c_2/sqrt(3) omits
-c_1/3 and has the wrong c_2 sign. Expanding Eq.(27) uniquely gives
alpha_2=c_+/6-c_minus/6-c_1/3+c_2/sqrt(3). The density is constructed from the
six real coefficients and is assumed PSD and trace one as in the section.
This is an equality of physical matrices, not an injectivity claim at small d. -/
theorem werner_permutation_coefficients_corrected
    (d : ℕ) (hd : 0 < d) (c : Fin 6 → ℝ)
    (hpositive : (wernerFromCoefficients d c).PosSemidef)
    (htrace : Matrix.trace (wernerFromCoefficients d c) = 1) :
    wernerFromCoefficients d c =
      ∑ j : Fin 6, correctedPermutationCoefficients c j • wernerPermutations d j := by sorry

end QAlgorithms.Papers.Independent.Extend50.P12

end

Source

Positive maps from the walled Brauer algebra, arXiv:2112.12738v3, PDF p. 13, Appendix B, Eqs.(B3)-(B5); corrected alpha_2 from Eq.(27)

Read-back

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

Let $d>0$ be a natural number and let $c_0,\ldots,c_5$ be arbitrary real numbers. For permutations of three register positions, define $V_\pi(x,y)=1$ if $x=y\circ\pi^{-1}$ , and $0$ otherwise, on words $x,y\in\{0,\ldots,d-1\}^{3}$ , and set

(V_0,V_1,V_2,V_3,V_4,V_5) =(I,V_{(01)},V_{(12)},V_{(02)},V_{(01)(12)},V_{(12)(01)}).

Define

\begin{aligned} B_0&=(V_0+V_1+V_2+V_3+V_4+V_5)/6,\\ B_1&=(V_0-V_1-V_2-V_3+V_4+V_5)/6,\\ B_2&=(2V_0-V_4-V_5)/3,\\ B_3&=(2V_2-V_3-V_1)/3,\\ B_4&=(V_1-V_3)/\sqrt3,\qquad B_5=\mathrm{i}(V_4-V_5)/\sqrt3, \end{aligned}

and $W=\sum_{j=0}^{5}c_jB_j$ . Assume $W$ is positive semidefinite and $\operatorname{tr}W=1$ . Then

W=\sum_{j=0}^{5}\gamma_jV_j,

where, writing $p=c_0,\ q=c_1,\ z=c_2,\ x=c_3,\ y=c_4,\ t=c_5$ and viewing these real numbers as complex scalars,

\begin{aligned} \gamma_0&=p/6+q/6+2z/3,\\ \gamma_1&=p/6-q/6-x/3+y/\sqrt3,\\ \gamma_2&=p/6-q/6+2x/3,\\ \gamma_3&=p/6-q/6-x/3-y/\sqrt3,\\ \gamma_4&=p/6+q/6-z/3+\mathrm{i}t/\sqrt3,\\ \gamma_5&=p/6+q/6-z/3-\mathrm{i}t/\sqrt3. \end{aligned}

The assertion includes $d=1$ and does not assert uniqueness of this expansion.

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