(127): necessary coefficient equations above dimension two

Proved

PermPartialTranspose.CommonSolutions.eq_127

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

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

Let $d>2$ , and let $\check R(t)=a\mathbf1+tP+bP_*$ with complex $a,b,u,v$ . If the additive Yang–Baxter equality holds at this particular pair $(u,v)$ , then

\begin{aligned} abu&=ab(u+v)+b^2v,\\ abv&=ab(u+v)+b^2u,\\ a^2b&=ab(u+v)+b^2(u+v)+b^3+2a^2b+ab^2d. \end{aligned}

These are the coefficient constraints extracted in Appendix B. The statement gives the necessary direction asserted by the paper; it makes no uniqueness claim at fixed $(u,v)$ .

Formalization Note The hypothesis $3\le d$ is the natural-number form of the paper's $d>2$ .

Preamble

import Mathlib
import Definitions.Def_PermPartialTranspose_CommonSolutions_Ops

Formal statement

namespace PermPartialTranspose.CommonSolutions

/-- The necessary coefficient equations (127), Appendix B, p. 38. -/
theorem eq_127 (d : ℕ) (hd : 3 ≤ d) (a b u v : ℂ)
    (h : onFirst (Rcheck d a u b) * onLast (Rcheck d a (u + v) b) *
          onFirst (Rcheck d a v b) =
        onLast (Rcheck d a v b) * onFirst (Rcheck d a (u + v) b) *
          onLast (Rcheck d a u b)) :
    a * b * u = a * b * (u + v) + b ^ 2 * v ∧
    a * b * v = a * b * (u + v) + b ^ 2 * u ∧
    a ^ 2 * b = a * b * (u + v) + b ^ 2 * (u + v) + b ^ 3 +
      2 * a ^ 2 * b + a * b ^ 2 * (d : ℂ) := by sorry

end PermPartialTranspose.CommonSolutions

Source

Zhang, Kauffman & Werner, Permutation and Its Partial Transpose, arXiv:quant-ph/0606005v1, p. 38, Appendix B, (127)

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