spectral_norm_eq_singular_value_zero

For any real matrix $Y$, its spectral (operator) norm equals its largest singular value, i.e. $\|Y\|_{op} = \sigma_1(Y) = (\mathrm{toEuclideanLin}\,Y).\mathrm{singularValues}\,0$. This is the standard identity (Horn & Johnson, Matrix Analysis 2nd ed., §5.6, and §7.3 on singular values) that the $\ell^2\to\ell^2$ operator norm of a matrix is its top singular value. Here spectralNorm is the operator norm of Matrix.toEuclideanLin Y and singularValues 0 is the (sorted-descending) largest singular value. The equality combines the two inequality directions, both already proved on the platform (spectral_norm_le_singular_value_zero and singular_value_zero_le_spectral_norm), via antisymmetry. It is a reusable rewrite bridge between the operator-norm world and the singular-value world.