p. 9 (with eq. (11), p. 4) — V′(n−1, n) = Φ⁺_{n−1,n}, the unnormalized maximally entangled projector on the last two systems
ProvedPTCommutant.OperatorBasis.ptLast_swapLastLet be the transposition of the last two of systems of and the partial transpose, on the last system, of its permutation operator. Then
the identity on the first systems tensored with the unnormalized projector onto the maximally entangled vector of systems . Entrywise: the matrix element between basis strings and is if for all , and , and otherwise.
This identifies the only generator of on which the partial transposition acts non-trivially, and it is the operator through which every is built.
Formalization Note. , systems are 0-based, so systems are the indices and and the first systems are the images of Fin.castLE from Fin m. On p. 9 denotes the unnormalized projector (eq. (11) calls "unnormalized"); the statement is the unnormalized form, which is for the normalized of Remark 3.
import Mathlib import Definitions.Def_PTCommutant_OperatorBasis_Model
namespace PTCommutant.OperatorBasis
open QAlgorithms.Schur
theorem ptLast_swapLast {m d : ℕ} (x y : Site d (m + 2)) :
ptLast (tensorPermutation d (m + 2) (swapLast m)) x y =
if (∀ i : Fin m, x (Fin.castLE (by omega) i) = y (Fin.castLE (by omega) i)) ∧
x ⟨m, by omega⟩ = x (Fin.last (m + 1)) ∧ y ⟨m, by omega⟩ = y (Fin.last (m + 1))
then 1 else 0 := by sorry
end PTCommutant.OperatorBasis
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.