spectral_norm_dual_attainment

spectralNorm dual ATTAINMENT. For every real matrix $X$ (viewed as the Euclidean linear map $\mathrm{toEuclideanLin}\,X$), there exist unit vectors $x,y$ ($\lVert x\rVert\le 1$, $\lVert y\rVert\le 1$) with $\langle Xx,\,y\rangle = \lVert X\rVert_{\mathrm{op}} = \mathrm{spectralNorm}\,X$. The operator norm of a finite-dimensional matrix is ATTAINED by a unit pair (extreme-value theorem: the unit ball of $\mathbb{R}^{n_2}$ is compact and $x\mapsto\lVert Xx\rVert$ is continuous, so the supremum defining the operator norm is achieved; the norming functional is then $y = Xx/\lVert Xx\rVert$). This is the ATTAINMENT companion to the previously-proved dual UPPER bound spectral_norm_inner_pairing_bound (d3228e1d, $\langle Xx,y\rangle\le\lVert X\rVert\,\lVert x\rVert\,\lVert y\rVert$); together they characterise the spectral norm by its dual pairing. This is the matrix→scalar norming-functional reduction used in de la Peña–Montgomery-Smith 1995 (arXiv:math/9309211) Proposition 1 / Lemma 2 to drop a Banach-valued tail to a scalar one.