Kepler’s Laws from Comoment Maps

4.1 Constancy Along Solutions

Theorem 9 Conservation of angular momentum
✓
#

Uses

Lean declarations

Along every solution, \(L = q \times p\) is constant.

Proof ▶

Differentiate \(L = q \times p\) using the product rule:

\[ \dot L = \dot q \times p + q \times \dot p. \]

Substitute the equations of motion:

\[ \dot L = \frac{p}{m} \times p + q \times \! \left(-\frac{\mu }{\| q\| ^3}q\right) = 0 + 0 = 0. \]

The first term vanishes because \(p \times p = 0\). The second vanishes because \(q \times q = 0\). So \(\dot L = 0\) and \(L\) is constant.

Theorem 10 Conservation of the Laplace–Runge–Lenz vector
✓
#

Uses

Lean declarations

Along every solution, \(A = p \times L - (m\mu /r)q\) is constant.

Proof ▶

Differentiate \(A = p \times L - (m\mu /r)q\). Since \(L\) is constant (\(\dot L = 0\)):

\[ \dot A = \dot p \times L - m\mu \frac{d}{dt}\! \left(\frac{q}{r}\right). \]

First term. Substitute \(\dot p = -(\mu /r^3)q\). Apply the BAC-CAB identity \(a \times (b \times c) = b(a \cdot c) - c(a \cdot b)\) to expand:

\[ -\frac{q}{r^3} \times (q \times p) = \frac{1}{r^3}\bigl(-q(q \cdot p) + p\| q\| ^2\bigr) = \frac{p}{r} - \frac{q(q \cdot p)}{r^3}. \]

Therefore:

\[ \dot p \times L = -\frac{\mu }{r^3}\, q \times (q \times p) = \mu \! \left(\frac{p}{r} - \frac{q(q \cdot p)}{r^3}\right). \]

Second term. Since \(r^2 = \| q\| ^2\), differentiating gives \(\dot r = (q \cdot \dot q)/r = (q \cdot p)/(mr)\). Therefore:

\[ \frac{d}{dt}\! \left(\frac{q}{r}\right) = \frac{\dot q}{r} - \frac{q\dot r}{r^2} = \frac{p}{mr} - \frac{q(q \cdot p)}{mr^3}. \]

Multiplying by \(m\mu \):

\[ m\mu \frac{d}{dt}\! \left(\frac{q}{r}\right) = \mu \! \left(\frac{p}{r} - \frac{q(q \cdot p)}{r^3}\right). \]

This equals the first term exactly, so they cancel:

\[ \dot A = \mu \! \left(\frac{p}{r} - \frac{q(q \cdot p)}{r^3}\right) - \mu \! \left(\frac{p}{r} - \frac{q(q \cdot p)}{r^3}\right) = 0. \]
Theorem 11 Conservation of energy
✓
#

Uses

Lean declarations

Along every solution, \(H = \| p\| ^2/(2m) - \mu /r\) is constant.

Proof ▶

Differentiate \(H\) along the trajectory:

\[ \dot H = \frac{p \cdot \dot p}{m} + \frac{\mu \dot r}{r^2}. \]

Substitute \(\dot p = -\mu q/r^3\) and \(\dot r = (q \cdot p)/(mr)\):

\[ \dot H = \frac{p}{m} \cdot \! \left(-\frac{\mu q}{r^3}\right) + \frac{\mu }{r^2} \cdot \frac{q \cdot p}{mr} = -\frac{\mu (p \cdot q)}{mr^3} + \frac{\mu (q \cdot p)}{mr^3} = 0. \]