(74): coloured Yang–Baxter identity for the dimension-two family

Proved

PermPartialTranspose.CommonSolutions.eq_74

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

braid-relationp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1partial-transposeyang-baxter-equation

In dimension two put $P^*=\mathbf1-\Theta_2(P)$ and $\check R(t)=aP^*+tP$ , where $a,x,y,z\in\mathbb C$ . On three factors, the paper's coloured identity is

\check R_i(x)\check R_{i+1}(z)\check R_i(y) =\check R_{i+1}(y)\check R_i(z)\check R_{i+1}(x).

This common identity supplies both Yang–Baxter parameter laws in the dimension-two branch.

Preamble

import Mathlib
import Definitions.Def_PermPartialTranspose_CommonSolutions_Ops

Formal statement

namespace PermPartialTranspose.CommonSolutions

/-- Equation (74), p. 24, with the operator (71). -/
theorem eq_74 (a x y z : ℂ) :
    onFirst (a • pBar 2 + x • swapOp 2) *
        onLast (a • pBar 2 + z • swapOp 2) *
        onFirst (a • pBar 2 + y • swapOp 2) =
      onLast (a • pBar 2 + y • swapOp 2) *
        onFirst (a • pBar 2 + z • swapOp 2) *
        onLast (a • pBar 2 + x • swapOp 2) := by sorry

end PermPartialTranspose.CommonSolutions

Source

Zhang, Kauffman & Werner, Permutation and Its Partial Transpose, arXiv:quant-ph/0606005v1, pp. 23–24, (71) and (74)

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