Continuity of the twisted gluing map $D^{m+1}\cup_\varphi D^{m+1}\to S^{m+1}$

The glue map from the twisted sphere to the sphere is continuous.

Two copies of the closed disk $D^{m+1}$ are glued along their boundary spheres by a homeomorphism $\varphi$, and twistedGlueToSphere sends the resulting quotient to $S^{m+1}$: the left copy goes to the upper hemisphere by the chart upperHemisphereHomeoDisk, the right copy to the lower hemisphere by lowerHemisphereHomeoDiskRefl after applying the Alexander extension of $\varphi^{-1}$. The map is already constructed in the definition bundle, with its well-definedness on the quotient discharged; what is claimed here is continuity.

Why it is not free. A map out of a Quot is continuous exactly when its composite with the quotient projection is, and that composite is Sum.elim of the two branch maps. The first branch is a composition of homeomorphisms and is continuous outright. The second is not: it factors through alexanderExt φ.symm, defined by

which is a quotient by $\|w\|$ and so has no continuity at the centre of the disk for formal reasons. Continuity there holds because $\bigl\|\,\|w\|\cdot\varphi^{-1}(w/\|w\|)\bigr\| = \|w\|$ exactly — the radial factor annihilates the discontinuity of the direction $w/\|w\|$ — so the map is squeezed to $0$ as $w\to0$. Away from the centre the direction map unitOr is continuous on $\{w \ne 0\}$, which is open, and the rest is composition.

Mathlib has neither the Alexander trick nor any radial-extension API, so this has to be built from continuousOn_unitOr in the mission's own chart bundle together with a squeeze at the origin.