(66)–(67): two flat braid representations in dimension two

Proved

PermPartialTranspose.CommonSolutions.eq_66_67

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

braid-relationp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1partial-transposevirtual-braid-group

In dimension two, let $P$ be permutation and $P^*=\mathbf1-\Theta_2(P)$ . Write $P_i,P_{i+1}$ and $P_i^*,P_{i+1}^*$ for their actions on adjacent pairs in $V^{\otimes3}$ . Both $P$ and $P^*$ satisfy the braid relation, both square to the identity, and

\begin{aligned} P_iP^*_{i+1}P_i&=P_{i+1}P_i^*P_{i+1},\\ P_iP^*_{i+1}P_i^*&=P^*_{i+1}P_i^*P_{i+1},\\ P_i^*P^*_{i+1}P_i&=P_{i+1}P_i^*P^*_{i+1}. \end{aligned}

These are the paper's flat unrestricted braid relations with $P^*$ as the flat crossing and $P$ as the virtual crossing.

Preamble

import Mathlib
import Definitions.Def_PermPartialTranspose_CommonSolutions_Ops

Formal statement

namespace PermPartialTranspose.CommonSolutions

/-- Equations (66)–(67), p. 22. -/
theorem eq_66_67 :
    BraidRel (swapOp 2) ∧
    BraidRel (pBar 2) ∧
    swapOp 2 * swapOp 2 = 1 ∧
    pBar 2 * pBar 2 = 1 ∧
    onFirst (swapOp 2) * onLast (pBar 2) * onFirst (swapOp 2) =
      onLast (swapOp 2) * onFirst (pBar 2) * onLast (swapOp 2) ∧
    onFirst (swapOp 2) * onLast (pBar 2) * onFirst (pBar 2) =
      onLast (pBar 2) * onFirst (pBar 2) * onLast (swapOp 2) ∧
    onFirst (pBar 2) * onLast (pBar 2) * onFirst (swapOp 2) =
      onLast (swapOp 2) * onFirst (pBar 2) * onLast (pBar 2) := by sorry

end PermPartialTranspose.CommonSolutions

Source

Zhang, Kauffman & Werner, Permutation and Its Partial Transpose, arXiv:quant-ph/0606005v1, p. 22, (66)–(67)

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