Horn's conjecture on sums of Hermitian matrices

Let $\rho$, $\sigma$, and $\tau$ be weakly decreasing sequences of real numbers, and let $\rho\boxplus\sigma\sim_c\tau$ mean that there exist Hermitian matrices with spectra $\rho$, $\sigma$, and $\tau$ whose first two matrices sum to the third. The trace identity is

$$\tau_1+\cdots+\tau_n=\rho_1+\cdots+\rho_n+\sigma_1+\cdots+\sigma_n.$$

For an admissible triple $i=(i_1\geq\cdots\geq i_r)$, $j=(j_1\geq\cdots\geq j_r)$, and $k=(k_1\geq\cdots\geq k_r)$, with $1\leq r<n$ and all entries between $0$ and $n-r$, define the inequality

$$\rho_{i_1+r}+\cdots+\rho_{i_r+1}+\sigma_{j_1+r}+\cdots+\sigma_{j_r+1}\geq\tau_{k_1+r}+\cdots+\tau_{k_r+1}.$$

Horn's conjecture. The relation $\rho\boxplus\sigma\sim_c\tau$ holds if and only if the trace identity holds and the displayed inequality holds whenever $i$, $j$, and $k$ are admissible and $i\boxplus j\sim_c k$.

This conjecture gives a finite necessary-and-sufficient system of linear inequalities for the possible spectra of a sum of two Hermitian matrices. The source presents it as Horn's proposed resolution of Weyl's problem; no resolution status is supplied here.