Completing an orthonormal pair by the cross product

The cross product of two orthogonal unit vectors in ℝ³ completes them to an orthonormal basis. The vectors orthogonal to the first vector are therefore exactly the linear combinations of the second vector and their cross product. This supplies the normal-plane frame used by TauCeti.exists_isSolidTorusNeighborhood.

Main results

• TauCeti.cross_orthonormal: the cross product completes an orthonormal pair and gives coordinates for the plane orthogonal to its first vector.

theorem TauCeti.cross_orthonormal {u n : EuclideanSpace ℝ (Fin 3)} (hu : ‖u‖ = 1) (hn : ‖n‖ = 1) (hun : inner ℝ u n = 0) : ‖WithLp.toLp 2 ((crossProduct u.ofLp) n.ofLp)‖ = 1 ∧ inner ℝ u (WithLp.toLp 2 ((crossProduct u.ofLp) n.ofLp)) = 0 ∧ inner ℝ n (WithLp.toLp 2 ((crossProduct u.ofLp) n.ofLp)) = 0 ∧ ∀ (v : EuclideanSpace ℝ (Fin 3)), inner ℝ u v = 0 ↔ v = inner ℝ n v • n + inner ℝ (WithLp.toLp 2 ((crossProduct u.ofLp) n.ofLp)) v • WithLp.toLp 2 ((crossProduct u.ofLp) n.ofLp)

Completing an orthonormal pair u, n of ℝ³ by the cross product u × n gives an orthonormal basis; in particular a vector is orthogonal to u exactly when it is a combination of n and u × n, with coefficients its inner products with them.