Qutrit APPT purity for n = 3
Abstract
Literal qutrit APPT density matrices satisfy the sharp purity bound for n = 3.
Theorem 1.1 (Sharp density-matrix purity estimate).
Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/AbsolutePPT/QutritN3PurityBound.purity_bound (✓ std3). ∎
Source. Repository-derived.
Commentary.
Every positive semidefinite trace-one complex matrix on Fin 3 × Fin 3 satisfying literal APPT has the stated real trace-square bound. APPT means that the partial transpose of U rho Uᴴ is positive semidefinite for every unitary U, as defined in QutritPerturbationAttainment. The proof applies QutritSpectralReduction.spectral_reduction to obtain ordered spectral certificate coordinates with both boundary LMIs and matching purity, then consumes the private rational gap certificate. All displayed quotients are real division.