Prove2Me

(3.20) — partial transpose preserves the trace pairing

Proved
BraneBrauer.Orthogonal.eq_3_20

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

brauer-algebrap2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1partial-transposetrace

For two operators X,YX,Y on the mixed tensor space, the partial transpose Σ\Sigma preserves their trace pairing:

tr⁡m,n(XY)=tr⁡m,n(Σ(X)Σ(Y)).\operatorname{tr}_{m,n}(XY) =\operatorname{tr}_{m,n}(\Sigma(X)\Sigma(Y)).

This is the bilinear-form identity used to pass from the third to the fourth line of (7.13).

Formalization Note The paper writes this on a complete Brauer basis. Matrix bilinearity extends it to all operators, the domain used here.

Preamble
import Mathlib
import Definitions.Def_BraneBrauer_Orthogonal_Setting

noncomputable section
Formal statement
namespace BraneBrauer.Orthogonal

/-- (3.20), p. 12: the partial transpose preserves the trace
bilinear form, extended from Brauer basis elements to all operators. -/
theorem eq_3_20 {N m n : ℕ} (X Y : Op N m n) :
    (X * Y).trace = (sigma X * sigma Y).trace := by sorry

end BraneBrauer.Orthogonal
Source
Kimura & Ramgoolam, Branes, Anti-Branes and Brauer Algebras in Gauge-Gravity duality, arXiv:0709.2158v2, p. 12, (3.20)
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