Prove2Me

Proof of Proposition 3.1: equivariance of the family

Proved
EquivPosMaps.TwoPositive.phi_equivariant

by mikedeng1 · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

k-positivityp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1positive-mapsquantum-information

Let n≥3n\geq3, let α,β∈R\alpha,\beta\in\mathbb R, and let U∈Mn(C)U\in M_n(\mathbb C) be unitary. Set V=U‾⊗UV=\overline U\otimes U. For every X∈Mn(C)X\in M_n(\mathbb C),

Φα,β,n(UXU∗)=VΦα,β,n(X)V∗.\Phi_{\alpha,\beta,n}(UXU^*)=V\Phi_{\alpha,\beta,n}(X)V^*.

This is the displayed equivariance computation in the proof of Proposition 3.1. It supplies the structural condition used in the positivity and 2-positivity criteria. The conjugation on the first tensor factor is essential.

Preamble
import Mathlib
import Definitions.Def_EquivPosMaps_TwoPositive_Basic
open scoped Matrix Kronecker ComplexOrder
noncomputable section
Formal statement
namespace EquivPosMaps.TwoPositive
/-- The equivariance display in the proof of Proposition 3.1, pp. 6–7. -/
theorem phi_equivariant (n : ℕ) (hn : 3 ≤ n) (α β : ℝ)
    (U : Matrix.unitaryGroup (Fin n) ℂ) (X : Matrix (Fin n) (Fin n) ℂ) :
    phi n α β ((U : Matrix (Fin n) (Fin n) ℂ) * X * star (U : Matrix (Fin n) (Fin n) ℂ)) =
      (((U : Matrix (Fin n) (Fin n) ℂ).map star) ⊗ₖ
        (U : Matrix (Fin n) (Fin n) ℂ)) * phi n α β X *
          ((((U : Matrix (Fin n) (Fin n) ℂ).map star) ⊗ₖ
            (U : Matrix (Fin n) (Fin n) ℂ))ᴴ) := by sorry

end EquivPosMaps.TwoPositive
Source
Collins, Osaka & Sapra, On a family of a linear maps from Mn(C) to Mn2(C), arXiv:1802.07553v1, pp. 6–7, proof of Proposition 3.1, “Choose V = Ū ⊗ U …”
Human review

  • Endorsed by Shuze Chen · Oct 21, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 21, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph