Let \(V\) be a finite-dimensional real vector space with
\(\dim V\geq 2\), and let \(Q\) be positive definite. If
\(Q(x)=Q(y)=c>0\), then some \(s\in \operatorname {Spin}(Q)\) satisfies
\[\operatorname {spinVectorAction}_Q(s,x)=y.\]
In particular, Spin acts transitively on the unit level \(Q(v)=1\).
This is a statement about the algebraic vector action; no topology or
compactness is needed.
Cartan's anisotropic-normal reflection has determinant \(-1\)
[cartan1981theory, Section 9, pp. 9--10]. His even-reflection
correction appears in [cartan1981theory, Section 10, p. 10].
The following two-case calculation gives the sphere orbit explicitly.
The formal surjectivity theorem uses positive \(Q\) directly: every
nonzero value \(Q(v)\) has a real square root, making the spinor norm
trivial on \(SO(Q)\)
CliffordAlgebra.orthogonalSpinorNorm_eq_one_of_posDef.
This is a separate route from the fixed-sign
sufficient hypothesis in Theorem [fcap-001B].