Regular homotopy classes of immersions are formal homotopy classes

By [L1], derivative induces a bijection on ${\pi }_0$. By [L2], the genuine components are the regular homotopy classes; the formal components are exactly homotopy classes of formal data. This gives the displayed bijection and both directions of the stated regular-homotopy criterion.

For a finite CW pair and a genuine restriction $u:Q\to \mathrm{Imm}(M,N)$, [L3] deforms every formal extension $v:P\to \mathrm{FImm}(M,N)$ to the derivative of a genuine extension, fixing $Q$. Hence the relative family comparison is surjective. If two genuine extensions have formally homotopic derivatives rel $Q$, apply [L3] to the finite CW pair $(P\times I,P\times \{0,1\}\cup Q\times I)$ with the prescribed genuine end families and constant $Q$ tracks. The resulting genuine family on $P\times I$ is a relative homotopy between the two extensions. This proves injectivity. Time remains a parameter of maps with source $M$, so this argument does not require an immersion of $P\times M$.

For the compact smooth parameter class, apply the separate relative assertion of [L1] to the family itself or to its supplied family homotopy with the full prescribed relative region. Its hypothesis concerns the original data on an open neighbourhood, so it gives exactly the stated relative holonomization and smooth version. For ordinary paths the endpoint flattening and smoothing in [L2] produce regular homotopies. No arbitrary-compact relative conclusion is inferred from weak equivalence alone.

If the source or the parameter is empty, the corresponding mapping spaces or families have their unique vacuous data; degree-zero source manifolds are finite and the same component argument applies. Both directions of every classification follow from the bijections proved above. The finite-relative comparison uses no extra choice by [L3]; the countable-choice premise is inherited from [L1] and [L2]. Thus all asserted conclusions are proved.