Kepler’s Laws from Comoment Maps

7.2 Orbit Equation

Theorem 25 Exact orbit equation
✓
#

Uses

Lean declarations

If \(L \neq 0\), then in polar coordinates in the orbital plane \(\Pi \), with the polar axis along \(A\), the orbit satisfies

\[ r = \frac{\ell }{1 + e\cos \theta }. \]

If \(A = 0\) then \(e = 0\) and \(r = \ell \) (constant), so the orbit is a circle.

Proof ▶

The starting point is identity (iii) from Proposition 12:

\[ A \cdot q = \| L\| ^2 - m\mu r. \]

Assume first that \(A \neq 0\). Choose polar coordinates in the fixed orbital plane so that the polar axis points along \(A\). If \(\theta \) is the angle between \(q\) and \(A\), then

\[ A \cdot q = \| A\| \, \| q\| \cos \theta = \| A\| r\cos \theta . \]

Substituting this into the identity above gives

\[ \| A\| r\cos \theta = \| L\| ^2 - m\mu r. \]

Now collect the terms involving \(r\):

\[ r\bigl(m\mu + \| A\| \cos \theta \bigr) = \| L\| ^2. \]

Finally divide numerator and denominator by \(m\mu \):

\[ r = \frac{\| L\| ^2/(m\mu )}{1 + (\| A\| /(m\mu ))\cos \theta } = \frac{\ell }{1 + e\cos \theta }. \]

This is the standard polar equation of a conic with focus at the origin.

If \(A = 0\), then \(e = 0\) and the same identity reduces to

\[ 0 = \| L\| ^2 - m\mu r, \]

so \(r = \ell \) is constant. Thus the orbit is the circular special case.

Theorem 26 Cartesian ellipse form
✓
#

Uses

Lean declarations

For \(H {\lt} 0\), \(L \neq 0\), and \(A \neq 0\), the orbit in orthonormal coordinates \((x, y)\) in \(\Pi \) (with \(x\)-axis along \(A\)) satisfies

\[ \frac{(x + ae)^2}{a^2} + \frac{y^2}{b^2} = 1. \]

If \(A = 0\), the orbit is a circle of radius \(a\).

Proof ▶

Start from the polar equation and write \(x = r\cos \theta \) in the chosen coordinates. Then

\[ r + ex = \ell . \]

Since \(r^2 = x^2 + y^2\), squaring both sides removes the remaining polar variable:

\[ x^2 + y^2 = (\ell - ex)^2 = \ell ^2 - 2e\ell x + e^2 x^2. \]

Move everything to one side:

\[ (1 - e^2)x^2 + 2e\ell x + y^2 = \ell ^2. \]

Because \(H {\lt} 0\), Proposition 24 gives \(0 \le e {\lt} 1\), so \(1-e^2 {\gt} 0\) and we may divide by it. Then complete the square in \(x\). Using \(a = \ell /(1-e^2)\) and \(b^2 = a\ell \), we obtain

\[ \left(x + \frac{e\ell }{1-e^2}\right)^2 + \frac{y^2}{1-e^2} = \frac{\ell ^2}{(1-e^2)^2}, \]
\[ \frac{(x + ae)^2}{a^2} + \frac{y^2}{b^2} = 1. \]
Theorem 27 The origin is a focus
✓
#

Uses

Lean declarations

For the noncircular case, the ellipse \(\tfrac {(x+ae)^2}{a^2} + \tfrac {y^2}{b^2} = 1\) has its center at \((-ae, 0)\). The focal half-distance is \(\sqrt{a^2 - b^2} = ae\), so the two foci are at \((-ae \pm ae, 0)\), that is \((0, 0)\) and \((-2ae, 0)\). The origin is a focus.

Proof ▶

The center is at \((-ae, 0)\) by inspection of the equation. The focal half-distance is \(\sqrt{a^2 - b^2} = ae\) by Proposition 24(e). Moving from the center by \(\pm ae\) along the \(x\)-axis gives foci at \((0, 0)\) and \((-2ae, 0)\). So the origin is a focus.

Theorem 28 Kepler’s First Law
✓
#

Uses

Lean declarations

For a non-collision solution with \(H {\lt} 0\) and \(L \neq 0\):

  • The orbit lies in the plane \(\Pi \) perpendicular to \(L\).

  • The eccentricity satisfies \(0 \le e {\lt} 1\) and the parameters \(e, \ell , a, b\) are given by the formulas in Definition 23.

  • The orbit satisfies the polar equation \(r = \ell /(1 + e\cos \theta )\).

  • The orbit is an ellipse with the origin at one focus (or a circle of radius \(a\) if \(A = 0\)).

Proof ▶

Collect Proposition 24 (planarity and parameter bounds), Theorem 25 (orbit equation), Theorem 26 (Cartesian form), and Theorem 27 (origin is a focus).