3.1 The Vector Field
The Kepler equations of motion are
The first equation says velocity equals momentum divided by mass. The second is Newton’s law for the inverse-square gravitational force. In Lean, the second component is defined by cases so the expression makes sense on all of \(\mathbb {R}^3 \times \mathbb {R}^3\). The case \(q = 0\) is never reached by a non-collision solution.
A curve \(\gamma \colon \mathbb {R}\to \mathbb {R}^3 \times \mathbb {R}^3\) is a solution if:
\(\gamma '(t)\) equals the Kepler vector field at \(\gamma (t)\) for every \(t\),
\(\| q(t)\| \neq 0\) for every \(t\) (no collision).
For every solution, \(\dot q = p/m\).
By Definition 5, the derivative \(\gamma '(t)\) agrees with the Kepler vector field at \(\gamma (t)\). Taking the first component of that vector field gives exactly
For every solution, \(\dot p = -\mu q/\| q\| ^3\).
Again \(\gamma '(t)\) equals the Kepler vector field at \(\gamma (t)\), so taking the second component gives the momentum equation. In the formalization the vector field is defined by cases so that it makes sense on all of \(\mathbb {R}^3 \times \mathbb {R}^3\). However, a non-collision solution never reaches \(q = 0\), so along the trajectory we are always in the branch
For every solution, \(q \times \dot p = 0\).
By the momentum equation, \(\dot p = (-\mu /\| q\| ^3)q\) is a scalar multiple of \(q\). The cross product of any vector with a scalar multiple of itself is zero: