Sphere and homotopy formulations under an explicit topological hypothesis

Let $S^4=\{x\in\mathbb R^5:\|x\|=1\}$, with its subspace topology and standard stereographic smooth structure modeled on $\mathbb R^4$. Assume the following universal hypothesis: for every type $M$ in the base universe, every compact Hausdorff topology on $M$, and every specified charted-space structure on $M$ modeled on $\mathbb R^4$, existence of a continuous homotopy equivalence between $M$ and $S^4$ implies existence of a homeomorphism $M\to S^4$; this hypothesis does not require smooth compatibility of the chart transitions. Under that hypothesis, two assertions are equivalent: for every $M$ among the compact Hausdorff topological spaces equipped with a specified charted-space structure modeled on $\mathbb R^4$ whose chart transitions are $C^\infty$ for the identity model on $\mathbb R^4$ with underlying type in the base universe, existence of a homeomorphism $M\to S^4$ implies existence of a diffeomorphism $M\to S^4$; and for every $M$ with those same space and smoothness assumptions, existence of a continuous homotopy equivalence between $M$ and $S^4$ implies existence of a diffeomorphism $M\to S^4$. Here a continuous homotopy equivalence consists of a pair of continuous maps in opposite directions whose two composites are continuously homotopic to the corresponding identity maps, and a diffeomorphism is a bijection for which both the forward map and the inverse are $C^\infty$ in the specified manifold charts. All conclusions are existence assertions, without uniqueness or a requirement to realize a particular given map. Empty spaces are permitted by the universal space assumptions, but cannot meet the homeomorphism or homotopy-equivalence premises involving $S^4$.