Uniform qutrit APPT spectral bound
Abstract
The first qutrit spectral LMI yields the purity bound 3/(8n) for every n at least 11.
Theorem 1.1 (K1-only uniform purity estimate).
Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/AbsolutePPT/UniformSpectralBound.uniform_spectral_bound (✓ std3). ∎
Source. Repository-derived.
Commentary.
Here n=3+k with k at least 8. An antitone nonnegative real spectrum of mass one is bounded using K1 alone. The argument extracts two boundary inequalities, reconstructs the spectrum from gaps, transfers a 33-ray cone certificate, and bounds every middle-coordinate mixture. The sum 3+k is formed in the natural numbers before its coercion to the reals; the quotient is real division.
The norm, step-synthesis, gap reconstruction and convex mixture lemmas have their unique source and typed descriptions in HalfspaceConeTransfer. This original qutrit proof and the three-row scalar proof both consume that common dependency; the original declaration names are preserved.