The quaternion double cover generates the third homotopy group of SO(3)

Conjugation is an anti-automorphism and the norm is multiplicative. Comparing the four coordinates of the product formula of [F1] with those of the product of the conjugates gives $\overline{xy}=\bar{y}\bar{x}$ for all $x,y\in \mathbb{H}$; since $\widehat{N(y)}$ is central by [F1], this gives $xy\cdot \overline{xy}=x(y\bar{y})\bar{x}=x\widehat{N(y)}\bar{x}=\widehat{N(y)}x\bar{x}$, whose left side is $\widehat{N(xy)}$ and whose right side is $\widehat{N(y)N(x)}$ by [F1], so $N(xy)=N(x)N(y)$. With [F2] this gives $\parallel x{\parallel }_2^2=N(x)$, and for a unit $q$ it gives $q^{-1}=\bar{q}$; in particular $S^3$ is closed under multiplication and inversion.

Quaternion multiplication and conjugation are continuous. Each coordinate of the product formula of [F1] is a polynomial in the eight coordinates of its two arguments; on the metric space $\mathbb{H}\times \mathbb{H}$ the coordinate functions are continuous by [F8], the product of two continuous real-valued functions is continuous because $2xy=⟨(x,y),(y,x)⟩$ is an inner product of two continuous vector-valued functions and scalar multiples are continuous, and finite sums of continuous functions are continuous, all by [F8]; so multiplication is continuous by the componentwise criterion of [F8]. Conjugation negates three coordinates and is continuous by the same criterion, and composites and restrictions of continuous maps are continuous by [F8], so $(q,v)\mapsto qv\bar{q}$ is continuous on $\mathbb{H}\times \mathrm{Im}\mathbb{H}$.

A nonidentity element of $\mathrm{SO}(3)$ fixes a unit vector. Let $R\in \mathrm{SO}(3)$. By [F6], $\det (R-I)=\det ((R-I{)}^{\mathsf{T}})=\det (R^{\mathsf{T}}-I)=\det (R^{-1}-I)=\det (R^{-1})\det (I-R)$, where $\det (R^{-1})=1$ and $\det (I-R)=-\det (R-I)$; hence $\det (R-I)=-\det (R-I)$, so $\det (R-I)=0$. By [F6] again $R-I$ is not invertible, so by [F17] its kernel is nonzero; choosing a nonzero $v$ with $Rv=v$ and setting $u=v\mathrm{/}\parallel v{\parallel }_2$ gives a unit vector with $Ru=u$.

The boundary of the cube is connected in dimensions at least two. For $n\ge 2$, $\epsilon \in \{0,1\}$ and $i<n$ let $F_i^{\epsilon }=\{s\in I^n:s_i=\epsilon \}$, so that $\mathrm{\partial }{I}^n$ is the union of the $2n$ faces $F_i^{\epsilon }$; each face is the image of $I^{n-1}$ under the continuous map inserting the constant coordinate $\epsilon$ in position $i$, hence connected by [F8] and [F10]. The set $A=F_0^0\cup F_1^0$ is connected by the first clause of [F10], both faces containing the point all of whose coordinates are $0$. Every face meets $A$: for $i\mathrm{\ne }0$ the faces $F_i^{\epsilon }$ and $F_0^0$ meet, and $F_0^1$ meets $F_1^0$, in each case because $n\ge 2$ leaves a coordinate free. The second clause of [F10] with core $A$ therefore makes $\mathrm{\partial }{I}^n$ connected.

The cube satisfies the hypotheses of the lifting criterion. The cube $I^n$ is convex by [F15] and nonempty, hence path-connected by [F15], and its fundamental group is trivial by [F15]. It is locally path-connected: given $x\in I^n$ and an open $U\ni x$ in the subspace topology, there is a ball $B(x,\delta )$ with $I^n\cap B(x,\delta )\subseteq U$ by [F8], the ball is convex by the triangle inequality of [F3], so $V=I^n\cap B(x,\delta )$ is convex as an intersection of convex sets and is nonempty and open in $I^n$, and $V$ is path-connected by [F15].

The third homotopy group of the sphere. By [F14] degree is an isomorphism ${\pi }_3(S^3,1)\to \mathbb{Z}$ carrying the class of the identity self-map to $1$, so transporting that self-map to the cubical model through the correspondence of [F13] gives a class $[\mathrm{id}]\in {\pi }_3(S^3,1)$ that generates the infinite cyclic group, and the constant class is the group identity by [F13] and therefore has degree $0$ by [F14].

A constant clutching map gives the trivial bundle. Let $c:S^3\to \mathrm{SO}(3)$ be constant and let $E_c$ be its clutched bundle, the quotient of the two cones times ${\mathbb{R}}^3$ by the identifications $(a,v{)}_{+}\sim (a,cv{)}_{-}$ of [F16]. Over the lower cone the map $(a,w{)}_{-}\mapsto (a,c^{-1}w{)}_{-}$ is a fibrewise-linear homeomorphism, and it is compatible with the identifications: the class of $(a,cv{)}_{-}$ is sent to the class of $(a,c^{-1}cv{)}_{-}=(a,v{)}_{-}$, which is identified with $(a,v{)}_{+}$ in the quotient by $(a,v{)}_{+}\sim (a,v{)}_{-}$. So the universal property of the quotient from [F11] produces a bundle isomorphism from $E_c$ to the bundle clutched by the identity map, whose two charts have identity transition and which is therefore the product of the suspension with ${\mathbb{R}}^3$, the trivial rank-three bundle. Hence every constant clutching map has trivial clutched bundle.

The induced map on ${\pi }_n$ is injective for $n\ge 2$. Let $p:E\to B$ be a covering with $b_0=p(e_0)$, and let $a,a^{\mathrm{\prime }}:(I^n,\mathrm{\partial }{I}^n)\to (E,e_0)$ be based cubes with $p_{\ast }[a]=p_{\ast }[a^{\mathrm{\prime }}]$. Then there is a homotopy $H:I^n\times I\to B$ with $H_0=p\circ a$, $H_1=p\circ a^{\mathrm{\prime }}$ and $H_t(\mathrm{\partial }{I}^n)=\{b_0\}$ for all $t$; lifting it through $p$ with initial lift $a$, which lifts $H_0=p\circ a$, gives $\tilde{H}$ with ${\tilde{H}}_0=a$ and $p\circ \tilde{H}=H$ by [F12]. For fixed $s\in \mathrm{\partial }{I}^n$, the path $t\mapsto \tilde{H}(s,t)$ and the constant path at $e_0$ are both lifts of the constant path at $b_0$ through $p$ and agree at $t=0$, because $\tilde{H}(s,0)=a(s)=e_0$; since $I$ is connected by [F10] they are equal by [F12], so ${\tilde{H}}_t(\mathrm{\partial }{I}^n)=\{e_0\}$ for all $t$. Thus $\tilde{H}$ is a boundary-fixed homotopy from $a$ to the based cube ${\tilde{H}}_1$, with $p\circ {\tilde{H}}_1=H_1=p\circ a^{\mathrm{\prime }}$. The two lifts ${\tilde{H}}_1$ and $a^{\mathrm{\prime }}$ of the same map $H_1$ agree at the boundary basepoint $0\in I^n$, where both equal $e_0$; since $I^n$ is connected, uniqueness of lifts [F12] gives ${\tilde{H}}_1=a^{\mathrm{\prime }}$. Hence $\tilde{H}$ is a based homotopy from $a$ to $a^{\mathrm{\prime }}$, so $[a]=[a^{\mathrm{\prime }}]$ and $p_{\ast }$ is injective.

Imaginary elements and orthogonality. An element is imaginary when its real coordinate is $0$, and $\mathrm{Im}\mathbb{H}$ is a three-dimensional real inner product space under the restriction of [F2]. For imaginary $x,y$ the real coordinate of $xy$ in the formula of [F1] is $-⟨x,y⟩$ and that of $yx$ is the same, so $xy+yx=-2⟨x,y⟩1$; hence orthogonal imaginary $x,y$ satisfy $xy=-yx$, a unit imaginary $u$ satisfies $u^2=-1$ by the case $x=y=u$, and for $w\in \mathrm{Im}\mathbb{H}$ orthogonal to such a $u$ associativity gives $uwu=(uw)u=(-wu)u=-w{u}^2=w$ and $u(uw)=u^{2}w=-w$. The product $uw$ is imaginary: step 1.1 gives $\overline{uw}=\bar{w}\bar{u}=wu=-uw$. Also $u(uw)+(uw)u=-w+w=0$ and $w(uw)+(uw)w=-u(w^2)+u(w^2)=0$; the displayed anticommutator identity therefore gives $u\perp uw$ and $w\perp uw$. Norm multiplicativity in step 1.1 gives $\parallel uw{\parallel }_2=\parallel w{\parallel }_2$. A unit $w\perp u$ exists by taking the first vector $e$ in $(i,j,k)$ not parallel to $u$ and normalizing $e-⟨e,u⟩u$. For this $w$, let $M$ have columns $u,w,uw$ in $(i,j,k)$. Their orthonormality gives $M^{\mathsf{T}}M=I$, hence $Mx=0$ implies $x=0$. By [F17] $M$ is invertible, so its columns form a basis. This finite matrix argument uses no basis-extension principle.

The matrix entries of conjugation vary continuously. For unit $q$ and imaginary $v$, step 1.1 gives $\overline{qv\stackrel{ˉ}{q}}=q\bar{v}\bar{q}=-qv\bar{q}$, so conjugation preserves the imaginary subspace; the coordinate product formula makes it real-linear. Write $(e_1,e_2,e_3)=(i,j,k)$. Its nine matrix entries are $⟨e_r,q{e}_s\bar{q}⟩$, $1\le r,s\le 3$, since this basis is orthonormal. Each is continuous in $q$ by step 1.2 and [F8], and the componentwise criterion gives a continuous map $S^3\to {\mathbb{R}}^9$.

The action of $\{\pm 1\}$ is a covering-space action. The two-element group $\{\pm 1\}$ acts on $S^3$ by left multiplication, which is an action by the group structure of the unit quaternions from step 1.1, and for $q\in S^3$ the set $U=\{p\in S^3:\parallel p-q{\parallel }_2<1\}$ is open in $S^3$ by [F2] and [F8] and contains $q$. If some $p$ lay in both $U$ and $-U$, then $\parallel p-q{\parallel }_2<1$ and $\parallel p+q{\parallel }_2<1$, so the parallelogram identity of [F3] would give $4=2\parallel p{\parallel }_2^2+2\parallel q{\parallel }_2^2=\parallel p-q{\parallel }_2^2+\parallel p+q{\parallel }_2^2<2$, which is impossible. Each of the maps $x\mapsto x$ and $x\mapsto -x$ is a homeomorphism of $S^3$, being the restriction of a linear isometry of $\mathbb{H}$ with continuous inverse by [F8]. Hence the action is a covering-space action, and the orbit map $\pi :S^3\to S^3\mathrm{/}\{\pm 1\}$ onto the orbit space with the quotient topology is a covering by [F12].

The induced map on ${\pi }_n$ is surjective for $n\ge 2$. Let $b:(I^n,\mathrm{\partial }{I}^n)\to (B,b_0)$ be a based cube and view it as a based map of $(I^n,0)$ into $(B,b_0)$, with $0\in \mathrm{\partial }{I}^n$. By step 1.5 the cube is path-connected and locally path-connected with trivial fundamental group at $0$, so $b_{\ast }{\pi }_1(I^n,0)=0\subseteq p_{\ast }{\pi }_1(E,e_0)$ vacuously, and the lifting criterion of [F12] gives a based lift $\tilde{b}:(I^n,0)\to (E,e_0)$ with $p\circ \tilde{b}=b$. On $\mathrm{\partial }{I}^n$ this lift takes values in the fibre $p^{-1}(b_0)$, which is discrete by [F12], and $\mathrm{\partial }{I}^n$ is connected by step 1.4, so $\tilde{b}(\mathrm{\partial }{I}^n)$ is a single point, namely $\tilde{b}(0)=e_0$. Hence $\tilde{b}$ is a based cube with $p_{\ast }[\tilde{b}]=[p\circ \tilde{b}]=[b]$ by [F13], and $p_{\ast }$ is surjective.

The conjugation formula. Let $q=a+r$ be a unit quaternion, with real $a$ and imaginary $r$; put $s=\parallel r{\parallel }_2$ and, when $s>0$, $u=r\mathrm{/}s$. For imaginary $w$ orthogonal to $u$, expanding $(a+su)w(a-su)$ by distributivity and using $uw=-wu$ and $uwu=w$ from step 2.2 gives $qw\bar{q}=(a^2-s^2)w+2asuw$, while expanding $(a+su)(uw)(a-su)$ and using $u(uw)=-w$ gives $q(uw)\bar{q}=(a^2-s^2)uw-2asw$; also $qu\bar{q}=(a^2+s^2)u=u$, because $u^2=-1$ and $a^2+s^2=N(q)=1$. The same expansions apply to any real $a,s$ and unit imaginary $u$ with $a^2+s^2=1$, without a sign restriction on $s$. Writing $C=a^2-s^2$ and $S=2as$, the identity $C^2+S^2=(a^2+s^2{)}^2=1$ holds and will be used below; conjugation by $q$ is linear in its argument and preserves the imaginary subspace, so $\rho (q)$ is a well-defined endomorphism of $\mathrm{Im}\mathbb{H}$, and for $s=0$, that is for $q=\pm 1$, it is the identity.

The action of $R$ on the plane orthogonal to its axis. Keep $R\mathrm{\ne }I$ and the unit fixed vector $u$ of step 1.3, and choose a unit $w$ orthogonal to $u$; by step 2.2 the list $(u,w,uw)$ is an orthonormal basis of $\mathrm{Im}\mathbb{H}$. By [F4] the map $R$ preserves inner products, so $Ru=u$, the vector $Rw$ is a unit vector orthogonal to $u$, and $R(uw)$ is a unit vector orthogonal to both $u$ and $Rw$. In the orthonormal basis $(w,uw)$ of the plane orthogonal to $u$ we may therefore write $Rw=(\cos \theta )w+(\sin \theta )uw$ for exactly one $\theta \in [0,2\pi )$ by [F7], while $R(uw)=\epsilon (-(\sin \theta )w+(\cos \theta )uw)$ for a sign $\epsilon \in \{1,-1\}$, those being the two unit vectors orthogonal to $(\cos \theta ,\sin \theta )$. The matrix of $R$ in the ordered basis $(u,w,uw)$ therefore has columns $(1,0,0)$, $(0,\cos \theta ,\sin \theta )$ and $(0,-\epsilon \sin \theta ,\epsilon \cos \theta )$, and the Leibniz formula of [F5] gives its determinant as $\epsilon ({\cos }^2\theta +{\sin }^2\theta )=\epsilon$; since determinants are basis-independent by [F5] and $\det R=1$, we conclude $\epsilon =1$.

The map $\rho (q)$ preserves norms. For $v\in \mathrm{Im}\mathbb{H}$ write $v=cu+w$ with $c=⟨v,u⟩$ real and $w$ orthogonal to $u$, so that $\parallel v{\parallel }_2^2=c^2+\parallel w{\parallel }_2^2$ by [F3]; by linearity of conjugation by $q$ and the identities of step 3.1, $qv\bar{q}=cu+Cw+Suw$. The three summands are pairwise orthogonal, and $\parallel uw{\parallel }_2=\parallel w{\parallel }_2$ by step 2.2, so the squared norm is $c^2+C^2\parallel w{\parallel }_2^2+S^2\parallel w{\parallel }_2^2=c^2+\parallel w{\parallel }_2^2$ by [F3] and $C^2+S^2=1$. Hence $\parallel qv\bar{q}{\parallel }_2=\parallel v{\parallel }_2$ for all $v$, and the same holds for $q=\pm 1$.

The map $\rho$ is surjective. For $R=I$ we have $R=\rho (1)$. For $R\mathrm{\ne }I$ keep $u$, $w$, $\theta$ from step 3.2 and put $q_0=\cos (\theta \mathrm{/}2)+\sin (\theta \mathrm{/}2)u$, a unit quaternion by [F7]. The addition formulas of [F7] with equal arguments give $\cos \theta ={\cos }^2(\theta \mathrm{/}2)-{\sin }^2(\theta \mathrm{/}2)$ and $\sin \theta =2\sin (\theta \mathrm{/}2)\cos (\theta \mathrm{/}2)$, so step 3.1 applied with $a=\cos (\theta \mathrm{/}2)$ and $s=\sin (\theta \mathrm{/}2)$ gives $\rho (q_0)(u)=u$, $\rho (q_0)(w)=(\cos \theta )w+(\sin \theta )uw$ and $\rho (q_0)(uw)=(\cos \theta )uw-(\sin \theta )w$. By step 3.2 these values agree with those of $R$ on the basis $(u,w,uw)$, and two linear maps with equal values on a basis are equal by [F3]. Hence $R=\rho (q_0)$ and $\rho$ is onto.

The image of $\rho$ lies in $\mathrm{SO}(3)$. By step 4.1 the endomorphism $\rho (q)$ preserves norms, so by [F4] it preserves inner products, satisfies $\rho (q{)}^{\ast }\rho (q)=I$ and is invertible, and its matrix in the orthonormal basis $(i,j,k)$ satisfies $R^{\mathsf{T}}R=I$ by [F4]. In the orthonormal basis $(u,w,uw)$ of step 2.2 the identities of step 3.1 show that the columns of the matrix of $\rho (q)$ are $(1,0,0)$, $(0,C,S)$ and $(0,-S,C)$; in the Leibniz formula of [F5] for this matrix only the identity permutation and one transposition contribute, giving determinant $C^2+S^2=1$. Determinants of endomorphisms may be computed in any ordered basis by [F5], so $\det \rho (q)=1$ and $\rho (q)\in \mathrm{SO}(3)$; for $q=\pm 1$ the endomorphism is the identity. Thus $\rho$ is a well-defined map $S^3\to \mathrm{SO}(3)$.

The map $\rho$ is a homomorphism with kernel $\{\pm 1\}$. For unit $q_1,q_2$, associativity of multiplication gives $(q_1{q}_2)v(q_1{q}_2{)}^{-1}=q_1(q_{2}v{q}_2^{-1})q_1^{-1}$, that is $\rho (q_1{q}_2)=\rho (q_1)\rho (q_2)$, and $\rho (1)$ is the identity. If $\rho (q)$ is the identity then $q$ commutes with $i,j,k$: comparing $qi$ with $iq$ in the coordinates of [F1] forces the $j$- and $k$-coefficients of $q$ to vanish, and then comparing $qj$ with $jq$ forces the $i$-coefficient to vanish, so $q$ is real, and being a unit it is $\pm 1$; conversely $\pm 1$ act trivially. Hence $\ker \rho =\{\pm 1\}$, and because $\rho (q^{-1}{q}^{\mathrm{\prime }})=\rho (q{)}^{-1}\rho (q^{\mathrm{\prime }})$ we have $\rho (q^{\mathrm{\prime }})=\rho (q)$ exactly when $q^{\mathrm{\prime }}=\pm q$.

The map $\rho :S^3\to \mathrm{SO}(3)$ is continuous. By step 2.3 the map $S^3\to {\mathbb{R}}^9$ recording the matrix of the endomorphism $v\mapsto qv\bar{q}$ is continuous, and by step 5.1 that endomorphism is $\rho (q)\in \mathrm{SO}(3)$; since $\mathrm{SO}(3)$ carries the subspace topology of the nine entries, the map $\rho$ into $\mathrm{SO}(3)$ is continuous by [F8].

The induced map on the orbit space is a continuous bijection. Let $G=\{\pm 1\}$. By step 6.1, $\rho (q^{\mathrm{\prime }})=\rho (q)$ exactly when $q^{\mathrm{\prime }}=\pm q$, so $\rho$ is constant on the orbits of $G$ and its fibres are exactly those orbits; note also that $\rho (-q)=\rho (q)$, since $(-q)v(-q{)}^{-1}=qv{q}^{-1}$. Since $\pi$ is a quotient map by [F11] and $\rho$ is continuous by step 6.2, the characteristic property and the factorisation clause of [F11] give a continuous map $\bar{\rho }:S^3\mathrm{/}G\to \mathrm{SO}(3)$ with $\bar{\rho }\circ \pi =\rho$; it is injective because the fibres of $\rho$ are the orbits and it is surjective by step 4.2.

The induced map is a homeomorphism. The orbit space $S^3\mathrm{/}G$ is compact, being the continuous image under $\pi$ of the compact space $S^3$ by [F9] and step 2.4, and $\mathrm{SO}(3)$ is Hausdorff, being a subspace of the nine-dimensional matrix space ${\mathbb{R}}^9$ with its product topology, hence metrizable, by [F5] and [F9]. The continuous bijection $\bar{\rho }$ of step 7.1 is therefore a homeomorphism by the compact-to-Hausdorff clause of [F9].

The map $\rho$ is a two-sheeted covering. Let $y\in \mathrm{SO}(3)$ and let $V$ be an evenly covered neighbourhood of ${\bar{\rho }}^{-1}(y)$ for the covering $\pi$ of step 2.4, so that ${\pi }^{-1}(V)$ is a disjoint union of open sheets, each mapped homeomorphically onto $V$ by $\pi$; each sheet meets each fibre of $\pi$ in exactly one point, so there are exactly two sheets, the fibres of $\pi$ being the two-point orbits of step 7.1. Put $W=\bar{\rho }(V)$, which is open by step 8.1. Then ${\rho }^{-1}(W)={\pi }^{-1}({\bar{\rho }}^{-1}(W))={\pi }^{-1}(V)$ is a disjoint union of two open sets, and on each of them $\rho$ is the composite of the homeomorphism $\pi$ with the homeomorphism $\bar{\rho }$, hence a homeomorphism onto $W$. So every point of $\mathrm{SO}(3)$ has an evenly covered neighbourhood with two sheets; $\rho$ is a continuous surjection by step 6.2 and step 4.2, and $\mathrm{SO}(3)$ is thereby homeomorphic to $S^3\mathrm{/}\{\pm 1\}$ through $\bar{\rho }$.

Covering projections induce isomorphisms on higher homotopy groups. By step 2.1 and step 2.5, for every covering $p:E\to B$ and every $n\ge 2$ the homomorphism $p_{\ast }:{\pi }_n(E,e_0)\to {\pi }_n(B,p(e_0))$ is bijective, hence an isomorphism of the groups of [F13]. Applying this to the covering $\rho :S^3\to \mathrm{SO}(3)$ of step 9.1 with $e_0=1$, where $\rho (1)=I$, the homomorphism ${\rho }_{\ast }:{\pi }_3(S^3,1)\to {\pi }_3(\mathrm{SO}(3),I)$ is an isomorphism.

The map $\rho$ is not nullhomotopic. Suppose $H:S^3\times I\to \mathrm{SO}(3)$ were a homotopy with $H_0=\rho$ and $H_1$ constant. The identity map of $S^3$ is a lift of $H_0=\rho$ through the covering $\rho$ of step 9.1, because $\rho \circ \mathrm{id}=\rho$; lifting $H$ by [F12] gives $\tilde{H}:S^3\times I\to S^3$ with ${\tilde{H}}_0=\mathrm{id}$ and $\rho \circ \tilde{H}=H$. The map ${\tilde{H}}_1$ lifts the constant map $H_1$, so its image lies in one fibre of $\rho$, a two-point set; since $S^3$ is connected by [F10], the continuous image ${\tilde{H}}_1(S^3)$ is connected and contained in a set of two points separated in the Hausdorff space $S^3$ by [F9], so ${\tilde{H}}_1$ is constant. Thus the identity of $S^3$ is homotopic to a constant map, and by [F14] those two maps have equal degree, contradicting the values $1$ and $0$ established in step 1.6. Hence $\rho$ is not nullhomotopic.

The third homotopy group of $\mathrm{SO}(3)$. Transport the based sphere map $\rho$ to the cubical model through [F13] and write $[\rho ]\in {\pi }_3(\mathrm{SO}(3),I)$ for its class; since ${\rho }_{\ast }$ is the isomorphism of step 10.1, functoriality in [F13] gives ${\rho }_{\ast }[\mathrm{id}]=[\rho \circ \mathrm{id}]=[\rho ]$ for the generator $[\mathrm{id}]$ of step 1.6. Composing the degree isomorphism of step 1.6 with the inverse of ${\rho }_{\ast }$ gives an isomorphism ${\pi }_3(\mathrm{SO}(3),I)\cong \mathbb{Z}$ carrying $[\rho ]$ to the degree-one generator, and an isomorphism carries generators to generators, so ${\pi }_3(\mathrm{SO}(3),I)$ is infinite cyclic generated by $[\rho ]$; in particular $[\rho ]\mathrm{\ne }0$.

The clutched bundle over $S^4$ is nontrivial. By [F16] with $n=3$ and $k=4$ the clutching construction applied to $\rho$ produces an oriented rank-three real vector bundle $E_{\rho }\to S^4$, and the classification of [F16] identifies the isomorphism class of $E_{\rho }$ with the homotopy class of $\rho$. If the underlying real bundle $E_{\rho }$ were trivial, a trivialization would preserve or reverse the specified orientation everywhere, since $S^4$ is connected by [F10]; composing with a fixed reflection in the latter case gives an oriented trivialization. Thus it would be orientation-preservingly isomorphic to $E_c$ for a constant $c$ by step 1.7, so by that classification $\rho$ would be homotopic to the constant map $c$, which step 10.2 excludes. Hence $E_{\rho }$ is nontrivial, and with step 11.1 this completes the proof of all four clauses of the statement. The argument selects only single vectors in steps 1.3 and 3.2 and finite data elsewhere, so no choice principle is used.