Gongyo's Mukai-type conjecture for smooth Fano varieties

Let $X$ be a smooth Fano variety, let $\rho_X$ be its Picard number, and let $\mathbb{K}\in\{\mathbb{Z},\mathbb{Q}\}$. Define the $\mathbb{K}$-total index $\tau_X(\mathbb{K})$ by

$$\tau_X(\mathbb{K})=\sup\left\{\sum_{i=1}^k a_i\mathrel{}\middle|\mathrel{}\sum_{i=1}^k a_iS_i=-K_X,\ S_i>0\text{ is a nef }\mathbb{Z}\text{-divisor},\ a_i\in\mathbb{K}_{>0}\right\}.$$

Gongyo's Mukai-type conjecture.

$$\dim X+\rho_X-\tau_X(\mathbb{K})\geq 0,$$

with equality if and only if

$$X\cong\mathbb{P}^{n_1}\times\dots\times\mathbb{P}^{n_{\rho_X}}.$$

The conjecture was posed by Gongyo as a characterisation of products of projective spaces whose factors need not have the same dimension. The source reports that it was very recently proved in full generality, so the conjectural statement is solved.