The inclusion of the explicit closed disk is differentiable to every order

For every natural number $m$, including $m=0$, let $E=\mathbb R^{m+1}$ with its Euclidean norm, $D=\{x\in E:\|x\|\leq1\}$, and $S^m=\{u\in E:\|u\|=1\}$, with their subspace topologies. The specified charted structure on $D$ has model half-space $H=\{y\in E:y_0\geq0\}$ and atlas consisting of the chart $x\mapsto x+2e_0$ on $\|x\|<1$ and, for each $p\in S^m$, the chart $x\mapsto(1-\|x\|,\sigma_{-p}(x/\|x\|))$ on $x\neq0$ and $x\neq-\|x\|p$, with target $\{y\in H:y_0<1\}$; $\sigma_{-p}$ is stereographic projection from $-p$, followed by the linear isometry to $\mathbb R^m$ chosen in the imported sphere construction. The preferred chart at $a$ is the first chart if $\|a\|<1$, and the boundary chart with $p=a$ if $\|a\|=1$. For every regularity order $k\in\mathbb N\cup\{\infty,\omega\}$, the inclusion $D\to E$, $x\mapsto x$, is $C^k$ in the manifold sense from this half-space model to the identity model on $E$. This means continuity and $C^k$ regularity in the specified preferred charts, within the model half-space at boundary points. The quantifier includes $k=0$, every positive finite order, infinite differentiability at $k=\infty$, and analytic chart regularity at $k=\omega$; no separate manifold-compatibility hypothesis on $D$ is assumed in the statement.