First explain the stated local conversion. The four equally weighted correlated local Pauli operations , , , and remove coherences in the Bell states basis, since those states have distinct joint parity eigenvalues. This leaves four Bell probabilities. One-party Pauli operations permute the Bell projectors, so the largest probability can be placed on the singlet . Call it ; necessarily .
The two common unitaries found above generate permutations of the three triplet projectors: exchanges and , and exchanges and . Averaging the six triplet permutations replaces their weights by their common mean, while collective-unitary covariance of the two-qubit singlet fixes the singlet projector. This is Bell twirling followed by triplet symmetrization, producing the specified two-qubit Werner state. Shared randomness coordinates the local choices, so the procedure is allowed by local operations and classical communication. Common unitaries alone would preserve the original singlet weight, which need not initially be at least ; the preceding one-party permutation is what ensures that range.
For the eigenvalue calculation, put , , and . Then . In the ordered computational basis , transposing the second subsystem gives
The block has eigenvalues and , while the other two basis vectors also have eigenvalue . Thus the partial transpose spectrum is
The last three are positive throughout the given range, so the partial transpose is not positive exactly when . A separable quantum state is a convex sum of product density operators, each still positive after transposing one factor. The negative eigenvalue therefore proves entanglement.
For completeness, separability on the other side can be proved explicitly rather than inferred solely from a theorem name. Let be the one-qubit Pauli eigenprojectors. At , the mixture of six antiparallel product states is
using . It is manifestly separable. For ,
with nonnegative coefficients summing to one; is also separable. Consequently
At the boundary the partial transpose has a zero eigenvalue and the explicit decomposition shows separability.