Injectivity 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 injective.

With two disks glued along their boundaries by $\varphi$, twistedGlueToSphere maps the left copy onto the upper hemisphere and the right copy onto the lower one. Injectivity is the statement that no two distinct points of the quotient are identified by that map.

Where the content is. On each copy separately the map is a composition of homeomorphisms, so it is injective there, and the two open hemispheres are disjoint. The whole difficulty is the equator. A point of the left disk's boundary and a point of the right disk's boundary have the same image exactly when they were already identified by the gluing relation GlueRel, and checking that requires unwinding: a boundary point $u$ of the left disk maps to the equatorial point determined by $u$, while a boundary point $w$ of the right disk maps through alexanderExt φ.symm, which on the boundary sphere is $\varphi^{-1}$ itself (alexanderExt_sphereToDisk), and then through the reflected chart. Equality of the two images forces $w = \varphi(u)$ as points of the boundary sphere, which is precisely the relation GlueRel.glue u.

So the statement is the injectivity half of the gluing; combined with surjectivity and continuity it gives the homeomorphism, since the twisted sphere is compact and the target is Hausdorff.