Stable normal data supplies framings of the surgery spheres below the middle dimension

The representation lemma proves that $g^{\ast }{\nu }_M$ is stably trivial, with the stable trivialization determined by $b$ and the pulled-back target bundle over the nullhomotopy disk. The tangent-normal identity along $g$ is $g^{\ast }TM=T{S}^p\oplus {\nu }_g$. The standard radial normal line of $S^p\subset {\mathbb{R}}^{p+1}$ gives $T{S}^p\oplus {\epsilon }^1\cong {\epsilon }^{p+1}$. Adding the stable normal splitting of $TM$ shows that ${\nu }_g$ is stably trivial. Equivalently the normal bundle of the Euclidean composite splits as ${\nu }_g\oplus g^{\ast }{\nu }_M$ and is stably trivial; neither summand is declared actually trivial merely because it is a complement.

Since $p<q$, the sphere-bundle cancellation lemma gives an actual normal frame. For the stable-framing comparison below take $p\ge 1$; the zero-sphere determinant comparison is treated separately below. We also check compatibility with the prescribed stable framing: in its construction the images of the added trivial directions form a map $T:S^p\to V_k({\mathbb{R}}^{q+k})$. The nullhomotopy of $T$ over the ball and the full complementary frame constructed there give a full orthogonal completion on the boundary which itself extends over the ball. Therefore the difference between the resulting stabilized actual frame and the supplied stable frame is nullhomotopic. Smoothing its normal sections preserves this homotopy class. Thus the actual framing realizes the supplied stable normal data, not merely the abstract isomorphism type of the bundle.

The tubular neighbourhood theorem turns this frame into a product embedding of a neighbourhood of the zero section. Compactness of $S^p$ supplies one uniform sufficiently small normal radius, which can be rescaled to $D^q$. It is the required framed embedded surgery sphere. The compatible stable framing together with the chosen nullhomotopy is precisely the normal-map extension data consumed by the surgery bordism supplier. For $p=0$, choose endpoint bases compatible with the incoming orientations and the handle radial-line convention. The determinant-transport hypothesis puts their comparison matrices in the same component of the general linear group, so an interval interpolation extends them; finite bases alone would not ensure this compatibility. All other cases use the stated rank inequality.

Construct the extension of the normal datum explicitly. The target nullhomotopy trivializes its pulled-back stable bundle over the core disk by the finite continuous projection construction. The trace handle has trivial tangent bundle, so its stable normal bundle has a fixed trivialization. Along the attaching sphere the comparison of these two stable trivializations with the incoming datum $b$ is precisely the stabilized difference checked nullhomotopic in step 2.1 for $p\ge 1$, or interpolated with compatible determinant signs in step 3.1 for $p=0$; this is the framing compatibility, including the radial tangent line of the sphere. Use that nullhomotopy to extend the comparison matrix over the core disk, constant on a short attaching collar, and extend it over the normal $D^q$ factor by its contraction. It agrees with $b$ on the handle attaching region after collar interpolation, so pastes to a stable bundle isomorphism $B$ over the trace. The map itself extends by the supplied core nullhomotopy and contraction of the $D^q$ factor; no smoothing into the CW target is asserted. Restricting to the outgoing face gives $(f^{\mathrm{\prime }},b^{\mathrm{\prime }})$. The oriented trace has boundary $M^{\mathrm{\prime }}\bigsqcup (-M)$, and pushing its boundary fundamental class to $X$ gives zero, so $f_{\ast }^{\mathrm{\prime }}[M^{\mathrm{\prime }}]=f_{\ast }[M]=[X]$. Thus the endpoint is degree one and $(F,B)$ is a normal bordism over the same target datum. This proves the finite-CW-target extension directly, rather than invoking the source13 proposition whose statement currently assumes a smooth target and already-supplied $B$.