Formal-immersion homotopies extend over a subcritical handle

The core lifting assertion is exactly [F1] with core dimension $k$, full column rank $m$, and target dimension $n$. The transverse columns are extended as frames in the normal quotient and with their tangential lift components; they are not differentiated parameter coordinates. The assumption $k<n$ supplies the positive normal direction in its covering-homotopy construction.

For the relative family, use its given genuine map on a source neighbourhood of $A$ as reference in the attaching collar. Restrict the formal data on the handle to the $k$-core, retaining all $m$ columns. Its attaching jet is the jet of that reference. By [F2] this family deforms through full-column formal core data to holonomic core data, with the attaching jet and the parameter neighbourhood of $Q$ fixed. Realize the holonomic data near the core by target local addition in the cocore directions. Pinch this realization to the given reference near the attaching core: identical full first jets make the difference $O(\mathrm{\mid }v{\mathrm{\mid }}^2)$ and the first derivative difference $O(\mathrm{\mid }v\mathrm{\mid })$, so the differentiated cutoff has size $O(\delta )$ on a cocore neighbourhood of radius $\delta$. Compactness gives one small radius preserving full rank for all parameters and homotopy times. These formulas match an actual open attaching germ, hence they glue to the unchanged immersion on $A$.

The resulting genuine map is defined near the union of the core and the attaching collar, and equals the original whole-handle immersion on a smaller parameter neighbourhood of $Q$. To obtain this, on a parameter transition strip inside the given holonomic neighbourhood blend the original immersion and the reconstructed map in local-addition coordinates near the core. Their identical full core jets give $O(\mathrm{\mid }v{\mathrm{\mid }}^2)$ value and $O(\mathrm{\mid }v\mathrm{\mid })$ derivative errors, so compactness and a sufficiently small common cocore radius preserve rank. On that smaller parameter neighbourhood keep the original map on the entire handle; the compression below is the identity there. Pull it back by the handle compression of [F2], with positive cocore scale $\lambda (p,x)$ equal to one near $Q$ and throughout a smaller attaching collar and transitioning inside the already prescribed reference region. This embeds the whole handle in that union, fixes $A$, and has triangular derivative blocks $I,\lambda I$. The associated formal homotopy starts from the original data: compress the original pair by this embedding isotopy, transport its full tangent columns to the core by the horizontal/vertical identity identifications, and reconstruct over a small cocore neighbourhood using the core homotopy. When the base map is not holonomic in the cocore directions, its vertical Taylor term can be interpolated to the supplied transverse formal columns freely; the base map has no immersion constraint during a formal homotopy. On the attaching region these terms already agree with the reference derivative. Transport target tangent fibres by local addition and interpolate the bundle columns after shrinking the cocore radius; their differences tend uniformly to zero from the common core monomorphism, so injectivity is preserved. This is fixed on the reference germ and on $Q$, and proves relative full-handle integration.

For the weak-equivalence preservation, take a sphere or disk parameter test with a formal family on $M$ and the prescribed genuine boundary family. An enlarged source collar $A^{+}$ inside the attaching region has the same derivative equivalence as $A$ by [F3]. The finite relative lifting in [F2] first holonomizes the family on $A^{+}$, keeping its prescribed genuine parameter data. Extend this deformation to the handle core using the formal first-jet lifting of [F1] on the cut attaching boundary. Reconstruct full formal handle data by the compression and target/bundle transport of step 2.1, using the varying $A^{+}$ family as attaching reference. This gives a global formal homotopy, then step 1.2–2.1 makes the whole handle genuine. All reconstructions are supported outside the fixed smaller $A$ collar where required; no all-boundary-jet extension of an arbitrary $A$ map is inferred from a bump function. Sphere tests give surjectivity and disk tests with their genuine boundary fixed give injectivity on each homotopy group and on components. Thus $D_M$ is a weak equivalence.