Smooth four-dimensional Poincaré conjecture — sphere form

Let $S^4=\{x\in\mathbb R^5:\|x\|=1\}$, with its subspace topology and standard stereographic smooth structure modeled on $\mathbb R^4$. For every type $M$ in the base universe equipped with a topology making it compact and Hausdorff, every specified charted-space structure on $M$ modeled on $\mathbb R^4$ with $C^\infty$-compatible chart transitions, if there exists a homeomorphism $M\to S^4$, then there exists a diffeomorphism $M\to S^4$, meaning a bijection for which both the forward map and the inverse are $C^\infty$ in the specified manifold charts. The assertion is universal over the topology and chart structure as well as $M$; it asserts existence of a diffeomorphism, without uniqueness or any requirement that a particular homeomorphism supply its underlying map. An empty $M$ is allowed among the quantified spaces, but cannot satisfy the homeomorphism premise.