A compact smooth knot has a choice-free normal tube

For each $p\in K$, [F2] supplies a local inverse neighborhood for $E$. Form the set of all tuples consisting of a local trivialization, an open base set $O$ containing its center, and a radius $r>0$ such that $O\times \{v:\mathrm{\parallel }v\mathrm{\parallel }<r\}$ lies in that injectivity neighborhood. These base sets cover $K$. Compactness gives finitely many such tuples whose base sets $O_i$ cover $K$; their recorded radii have a positive finite minimum $r_0$. The tuples are collected as a set of all witnesses and only a finite subfamily is extracted, so no point-indexed choice is used.

Apply [F3] to the finite cover $\{O_i\}$ of the metric space $K$, obtaining $\delta >0$. Choose $0<\epsilon <\min \{r_0,\delta \mathrm{/}3\}$. If $E(p,v)=E(q,w)$ with $\mathrm{\parallel }v\mathrm{\parallel },\mathrm{\parallel }w\mathrm{\parallel }<\epsilon$, then $\mathrm{\parallel }p-q\mathrm{\parallel }=\mathrm{\parallel }w-v\mathrm{\parallel }<2\epsilon <\delta$. Thus $\{p,q\}$ lies in one $O_i$, and both $(p,v)$ and $(q,w)$ lie in the same recorded neighborhood where $E$ is injective; hence $(p,v)=(q,w)$. Every point of the radius-$\epsilon$ tube also lies in one of those local-diffeomorphism neighborhoods, so the restriction is an injective local diffeomorphism.

An injective local diffeomorphism is open and has smooth local inverses that agree on overlaps. Therefore $E$ is a diffeomorphism onto its open image $N_{\epsilon }$, which contains $K$ by [F1].

For $x=E(p,v)\in N_{\epsilon }\setminus K$, define $H_t(x)=E\text{\hspace{0.17em}⁣}(p,\frac{(1-t)\mathrm{\parallel }v\mathrm{\parallel }+t\epsilon }{\mathrm{\parallel }v\mathrm{\parallel }}v),0\le t\le 1,$ and set $H_t(x)=x$ for $x\mathrm{\notin }{N}_{\epsilon }$. The normal coordinates are unique by step 3.1, and the formula approaches the identity at $\mathrm{\parallel }v\mathrm{\parallel }=\epsilon$, so these clauses paste continuously. It fixes the exterior pointwise and at $t=1$ sends every point in the punctured tube to its radius-$\epsilon$ boundary. Thus it is a deformation retraction of ${\mathbb{R}}^3\setminus K$ onto ${\mathbb{R}}^3\setminus N_{\epsilon }$. Only finitely many local neighborhoods and a finite minimum were used.