Appendix B (corrected): exclusion above dimension two

Proved

PermPartialTranspose.CommonSolutions.appendix_b_high_dim

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

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

Let $d>2$ , $a\ne0$ , and $\check R(u)=a\mathbf1+uP+bP_*$ . Then:

For every $u\ne0$ , $\check R(u)$ fails the braid relation.
With $u$ as the spectral parameter, this family fails the multiplicative Yang–Baxter equation (14).
If $b\ne0$ , it fails the additive Yang–Baxter equation (15).

These are the higher-dimensional exclusions needed for the corrected classification.

Formalization Note The paper's unqualified braid and additive claims have counterexamples at $u=0$ and $b=0$ , respectively. The first is its own $\mathbf1+vP_*$ solution in §6.1; the second is the rational family $a\mathbf1+uP$ in §3.2. The corrected guards are explicit here.

Preamble

import Mathlib
import Definitions.Def_PermPartialTranspose_CommonSolutions_Ops

Formal statement

namespace PermPartialTranspose.CommonSolutions

/-- The corrected higher-dimensional exclusions in Appendix B, p. 37. -/
theorem appendix_b_high_dim (d : ℕ) (hd : 3 ≤ d) (a b : ℂ) (ha : a ≠ 0) :
    (∀ u : ℂ, u ≠ 0 → ¬ BraidRel (Rcheck d a u b)) ∧
    ¬ MultiplicativeYBE d a b ∧
    (b ≠ 0 → ¬ AdditiveYBE d a b) := by sorry

end PermPartialTranspose.CommonSolutions

Source

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

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