On the product of nontrivial cross-intersecting families

Let $n\geq2\ell\geq2k\geq6$ and $n>k+\ell$. We determine the maximum of $|\mathcal A||\mathcal B|$ over all nonempty, nontrivial cross-intersecting families $\mathcal A\subseteq\binom{[n]}k$ and $\mathcal B\subseteq\binom{[n]}\ell$. The exact bound is $|\mathcal A||\mathcal B|\leq\max\{M_1,M_2\}$, where \[ \begin{aligned} M_1 &=\left(\binom{n-1}{k-1}-\binom{n-\ell-1}{k-1}+1\right) \left(\binom{n-1}{\ell-1}-\binom{n-k-1}{\ell-1}+1\right),\\ M_2 &=\left(\binom{n-2}{\ell-2}+1\right) \sum_{i=1}^{2} \left(\binom{n-i}{k-1}-\binom{n-\ell-i}{k-1}\right). \end{aligned} \] Both terms are attained by explicit constructions: a Hilton--Milner-type pair and a two-point construction, respectively. We classify all equality cases, including the additional cross-triangle pairs when $k=\ell=3$. Two structural results underlie the proof. First, we establish a restricted-lex comparison theorem showing that restricted lexicographic initial segments minimize disjointness neighborhoods, and characterize equality at the first nontrivial threshold. Second, a decomposition of critically shifted families into two parts with disjoint cores leads to a sharp product theorem, with equality characterized, for all cross-intersecting pairs admitting this decomposition, without additional nontriviality assumptions. Endpoint comparisons and reverse shifting complete the proof for unequal as well as equal uniformities.