No $C^1$ retraction of the closed unit ball onto its boundary sphere

No smooth retraction of the ball onto its boundary (Milnor 1978, Section 2; Rogers 1980). Let $\overline{B}^n \subseteq \mathbb{R}^n$ be the closed unit ball and $S^{n-1}$ its boundary sphere. There is no $C^1$ map $g : \mathbb{R}^n \to \mathbb{R}^n$ such that

This is the analytic core of Milnor's proof of Brouwer's fixed-point theorem. Sketch of the classical argument: put $g_t(x) = x + t\,(g(x) - x)$. For small $t \ge 0$ the map $g_t$ is a bijection of the ball onto itself with positive Jacobian, so by the change-of-variables formula $\int_{\overline{B}^n} \det Dg_t = \operatorname{vol}(\overline{B}^n)$. The left-hand side is a polynomial in $t$, hence equals $\operatorname{vol}(\overline{B}^n)$ for all $t$, in particular for $t = 1$; but $g_1 = g$ takes values in the sphere, so $Dg$ is singular everywhere on the open ball and the integral vanishes, a contradiction. Together with the smoothing lemma AGT.exists_contDiff_retraction_unitBall it yields the no-retraction theorem AGT.no_retraction_unitBall, and hence Brouwer's theorem for the ball and Nash's theorem.

A note on the hypotheses. Only $C^1$ regularity is needed (continuity of the derivative gives the Lipschitz bound and the continuity of the Jacobian). For $n = 0$ the ball is a point and the sphere is empty, so the hypotheses are already contradictory.

Formalization Note. The ambient space is EuclideanSpace ℝ (Fin n); g is a total function with ContDiff ℝ 1 g, Set.MapsTo g (closedBall 0 1) (sphere 0 1), and the fixed-point condition on the sphere; the conclusion is False.