Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Ahiable–Kothakonda–Winter Eq. (31) and absolute separability

Abstract

The linear spectral condition in Eq. (31) implies absolute separability.

Definition 1.1 (The spectral condition).

Formalization. D5/S3/Quantum/Entanglement/AbsoluteSeparability/AhiableKothakondaWinterEq31.claim (✓ std3).

Citation. Jennifer Ahiable; Naga Bhavya Teja Kothakonda; Andreas Winter (2026). The geometry of absolute separability and other convex matrix properties from spectrum. DOI: 10.48550/arXiv.2608.03390. URL: https://arxiv.org/abs/2608.03390v2.

Commentary.

Theorem 6.2, Eq. (31), assumes a decreasingly ordered spectrum λ₁ ≥ ⋯ ≥ λ_mn ≥ 0 and requires 2λ_mn + Σ_{k=1}^{m−1} λ_{mn−k} ≥ Σ_{k=1}^{m−1} λ_k. Section 7 asks whether this condition implies absolute separability. The definition in Section 1 requires every global unitary conjugate UρU† to remain separable. The statement quantifies all 2 ≤ m ≤ n, every positive semidefinite trace-one state, and every global unitary, using separableCone, the cone of finite sums of Kronecker products of positive semidefinite factors. In the displayed formula lambda(i) is the decreasing eigenvalues₀ of rho at zero-based index i; lambda(0) ≥ ⋯ ≥ lambda(mn−1) ≥ 0.

Theorem 1.2 (Absolute separability follows).

Proof. Machine-checked in Lean as D5/S3/Quantum/Entanglement/AbsoluteSeparability/AhiableKothakondaWinterEq31.result (✓ std3). ∎

Resolves. Problems/ahiable-kothakonda-winter-2026-eq31-absolute-separability (proved) by D5/S3/Quantum/Entanglement/AbsoluteSeparability/AhiableKothakondaWinterEq31.result.

Source. Repository-derived.

Acknowledgement. Jennifer Ahiable; Naga Bhavya Teja Kothakonda; Andreas Winter (2026). The geometry of absolute separability and other convex matrix properties from spectrum. DOI: 10.48550/arXiv.2608.03390. URL: https://arxiv.org/abs/2608.03390v2.

Commentary.

The spectral theorem orders an eigenbasis and telescopes the spectrum into the identity, the codimension-one projection ray, and the rays a_k I + 2P_k with a_k = min(k,m−1,mn−k−1). The three existing ray constructions prove separability of each summand; Eq. (31) makes the identity coefficient nonnegative. Finite sums and nonnegative scalings preserve separability.

References