Qutrit APPT purity for n = 7
Abstract
Literal qutrit APPT density matrices satisfy the sharp purity bound for n = 7.
Theorem 1.1 (The reusable length-21 spectral certificate).
Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/AbsolutePPT/QutritN7PurityBound.certificate_bound (✓ std3). ∎
Source. Repository-derived.
Commentary.
Every antitone real 21-coordinate vector of mass one with nonnegative last coordinate and both qutrit boundary matrices positive semidefinite has square sum at most 29/529. The rational gap certificate applies directly to spectral data. Boundary-preserving insertion and deletion use this endpoint after positive mass normalization; no literal APPT sufficiency is asserted for arbitrary boundary-feasible spectra.
Theorem 1.2 (Sharp density-matrix purity estimate).
Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/AbsolutePPT/QutritN7PurityBound.purity_bound (✓ std3). ∎
Source. Repository-derived.
Commentary.
Every positive semidefinite trace-one complex matrix on Fin 3 × Fin 7 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 reusable rational gap certificate. All displayed quotients are real division.