(70): the second dimension-two braid solution

Proved

PermPartialTranspose.CommonSolutions.eq_70

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

braid-relationeight-vertex-modelp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1partial-transpose

In dimension two, the coefficient choice $a=b=-u$ gives $\check R(u)=a(\mathbf1-P+P_*)$ . For every nonzero complex $a$ , this matrix satisfies the braid relation:

\check R_i\check R_{i+1}\check R_i =\check R_{i+1}\check R_i\check R_{i+1}.

This is the second branch of Theorem 1's braid classification. Equation (70) displays the matrix at $a=1$ ; the statement includes its nonzero scalar multiples because the braid equation is homogeneous.

Preamble

import Mathlib
import Definitions.Def_PermPartialTranspose_CommonSolutions_Ops

Formal statement

namespace PermPartialTranspose.CommonSolutions

/-- The nonzero scalar multiples of the braid solution (70), p. 22. -/
theorem eq_70 (a : ℂ) (ha : a ≠ 0) : BraidRel (Rcheck 2 a (-a) a) := by sorry

end PermPartialTranspose.CommonSolutions

Source

Zhang, Kauffman & Werner, Permutation and Its Partial Transpose, arXiv:quant-ph/0606005v1, p. 22, Theorem 1 and (70)

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