Orbits of nondegenerate special orthogonal groups

A special orthogonal transformation carries any vector of a fixed nonzero norm to any other, provided the nondegenerate quadratic space has dimension at least two. This is the linear-algebra input for transitive actions on nonzero quadratic levels; see Lawson--Michelsohn, Spin Geometry, Chapter I, Section 2.

theorem QuadraticMap.exists_specialOrthogonal_map_eq_of_nondegenerate {K : Type u} {V : Type v} [Field K] [NeZero 2] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (hQ : Nondegenerate) (hrank : 2 ≤ Module.finrank K V) {x y : V} (hxy : Q x = Q y) (hy : Q y ≠ 0) : ∃ (g : ↥(TauCeti.QuadraticMap.specialOrthogonalGroup Q)), ↑g x = y

A nondegenerate special orthogonal group acts transitively on every nonzero quadratic level set when the quadratic space has dimension at least two.