Four-by-four APPT spectral reduction
Abstract
Literal four-by-four APPT density matrices satisfy the two qutrit corner constraints on their largest three and smallest six spectral values.
Definition 1.1 (The nine boundary values in dimension sixteen).
Formalization. D5/S3/Quantum/Entanglement/AbsolutePPT/QuadbitSpectralReduction.boundaryValues16 (✓ std3).
Source. Repository-derived.
Commentary.
Indices are zero-based. The boundary selector retains spectrum entries 0, 1, 2, 10, 11, 12, 13, 14, 15, and omits the seven middle values. The packing equivalence uses all sixteen coordinates; it does not change the physical local tensor factors.
Theorem 1.2 (Four-by-four density-to-spectrum reduction).
Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/AbsolutePPT/QuadbitSpectralReduction.spectral_reduction (✓ std3). ∎
Source. Repository-derived.
Commentary.
Every positive semidefinite trace-one matrix on Fin 4 × Fin 4 that remains positive under partial transpose after every global unitary conjugation has an antitone nonnegative sixteen-coordinate spectrum of mass one. Its selected largest three and smallest six values satisfy both real qutrit boundary LMIs, and its real trace-square equals the sum of spectral squares. The proof reuses the existing ordered spectral diagonalization and the existing Bell calculation. It embeds that calculation into the genuine local Fin 3 × Fin 3 corner, extends each unitary by the identity on the seven complementary product positions, and compresses partial transpose only along product coordinates. An arbitrary global coordinate equivalence is used as a unitary packing, never as an asserted symmetry of partial transpose. These two constraints are necessary; this theorem does not assert that they characterize four-by-four APPT states. No statement about physical preparation or experimental observability is included. The bridge is consumed by the exact dimension-sixteen purity bound.