Dependency graph

Legend

Boxes: definitions
Ellipses: theorems and lemmas
Blue border: the statement of this result is ready to be formalized; all prerequisites are done
Orange border: the statement of this result is not ready to be formalized; the blueprint needs more work
Blue background: the proof of this result is ready to be formalized; all prerequisites are done
Green border: the statement of this result is formalized
Green background: the proof of this result is formalized
Dark green background: the proof of this result and all its ancestors are formalized
Dark green border: this is in Mathlib

Definition 29Areal velocity and swept area

The signed areal velocity along a curve $\gamma $ is

\[ \frac{1}{2m} \left\langle \frac{L(0)}{\| L(0)\| }, q(t) \times p(t) \right\rangle , \]

where $L(0) = q(0) \times p(0)$. The swept area on a time interval $[t_1, t_2]$ is:

\[ \mathcal{A}(t_1, t_2) = \int _{t_1}^{t_2} \text{(signed areal velocity)}\, dt. \]

LaTeX

Lean

Kepler.signedArealVelocity
Kepler.sweptAreaOn

Definition 3Energy, angular momentum, and Laplace–Runge–Lenz vector

For a phase point $z = (q, p)$, define:

\[ H(q,p) = \frac{\| p\| ^2}{2m} - \frac{\mu }{\| q\| }, \qquad L = q \times p, \qquad A = p \times L - \frac{m\mu }{\| q\| }q. \]

Here $H$ is the total energy (kinetic minus potential), $L$ is the angular momentum vector, and $A$ is the Laplace–Runge–Lenz vector. All three are proved constant along every non-collision solution in Chapter 4.

LaTeX

Lean

Kepler.cross
Kepler.energy
Kepler.angularMomentum
Kepler.laplaceLenz

Definition 23Eccentricity and semi-axes

For a phase point $z = (q, p)$ away from collision, define:

\[ e = \frac{\| A\| }{m\mu }, \qquad \ell = \frac{\| L\| ^2}{m\mu }, \qquad a = -\frac{\mu }{2H}, \qquad b = a\sqrt{1-e^2}. \]

Here $e$ is the eccentricity. $\ell $ is the semi-latus rectum. $a$ is the semi-major axis, meaning half the length of the long axis of the ellipse. $b$ is the semi-minor axis, meaning half the length of the short axis of the ellipse. Since $L$, $A$, and $H$ are conserved, all four quantities are constant along a solution. Geometric data. The center of the ellipse is not at the origin. The origin is a focus. The distance from the center to the focus is $ae$. The relation $b^2 = a\ell $ will be used later.

LaTeX

Lean

Kepler.eccentricity
Kepler.semiLatusRectum
Kepler.semiMajorAxis
Kepler.semiMinorAxis

Definition 5Solutions

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).

LaTeX Lean

Definition 19Negative-energy shell and rescaled observables

Fix $h {\lt} 0$. The negative-energy shell $M_h$ is the set of all phase points $(q, p)$ with $H(q, p) = h$ and $r \neq 0$. Equivalently, it is the fixed-energy surface cut out by the equation $H = h$ inside the non-collision phase space, so it has dimension five.

On $M_h$, define the rescaled Lenz vector:

\[ K = \frac{A}{\sqrt{-2mh}}, \qquad K_u = u \cdot K. \]

This is well-defined because $h$ is a fixed negative number, so $\sqrt{-2mh}$ is an honest real constant on the whole surface. The rescaling is chosen so that $\{ K_u, K_v\} = L_{u \times v}$ on $M_h$ (proved in Theorem 21).

LaTeX

Lean

Kepler.K_u
Kepler.NegativeEnergyShell
Kepler.so4ModelBracket
Kepler.mu_h

Definition 2Radial distance and non-collision locus

The radial distance is $r = \| q\| $. The non-collision phase space is the subset where $r \neq 0$, i.e., where the planet is not at the origin.

LaTeX

Lean

Kepler.radialDist
Kepler.NoncollisionPhaseSpace

Definition 32Configuration and orbital period

A configuration period is a minimal positive time $T {\gt} 0$ such that $q(t + T) = q(t)$ for all $t$. An orbital period adds the condition that the swept area over $[0, T]$ equals $\pi ab$.

LaTeX

Lean

Kepler.HasConfigurationPeriod
Kepler.HasOrbitalPeriod

Definition 1Phase space and parameters

The phase space is $\mathbb {R}^3 \times \mathbb {R}^3$. A point is written $(q, p)$ where $q \in \mathbb {R}^3$ is the position and $p \in \mathbb {R}^3$ is the momentum. The mass $m {\gt} 0$ and gravitational parameter $\mu {\gt} 0$ are positive real constants.

LaTeX

Lean

Kepler.Vec3
Kepler.PhaseSpace
Kepler.MassParam
Kepler.GravitationalParam

Definition 13Partial derivatives and Poisson bracket

For a smooth function $F$ on phase space, write $\partial _{q_i}F$ for its partial derivative in the $q_i$ direction and $\partial _{p_i}F$ in the $p_i$ direction. The Poisson bracket is:

\[ \{ F, G\} = \sum _{i=1}^3 \! \left(\partial _{q_i}F \cdot \partial _{p_i}G - \partial _{p_i}F \cdot \partial _{q_i}G\right). \]

If $H$ is the Hamiltonian, then $\{ F,H\} $ is the time derivative of $F$ along the motion.

LaTeX

Lean

Kepler.partialQ
Kepler.partialP
Kepler.poissonBracket
Kepler.keplerHamiltonian

Definition 16Momentum maps, comoment maps, and rotation observables

Suppose a Lie algebra $\mathfrak g$ acts on a phase space $M$ by infinitesimal symmetries. A momentum map is a map

\[ \mu \colon M \longrightarrow \mathfrak g^* \]

such that pairing with $\xi \in \mathfrak g$ gives the Hamiltonian for the infinitesimal motion generated by $\xi $. The associated comoment map is the linear map

\[ \tilde\mu \colon \mathfrak g \longrightarrow C^\infty (M), \qquad \tilde\mu (\xi )(x) = \langle \mu (x), \xi \rangle . \]

Lean uses the comoment because the declarations are scalar observables.

In the Kepler problem we identify $\mathfrak {so}(3)$ with $\mathbb {R}^3$ using the cross product. For $u \in \mathbb {R}^3$, define the scalar functions

\[ L_u = u \cdot L = u \cdot (q \times p), \qquad A_u = u \cdot A. \]

The map $u \mapsto L_u$ is the rotational comoment built from the angular momentum.

LaTeX

Lean

Kepler.comomentMap
Kepler.L_u
Kepler.A_u

Definition 4Kepler vector field

The Kepler equations of motion are

\[ \dot q = \frac{1}{m}p, \qquad \dot p = -\mu \frac{q}{\| q\| ^3}. \]

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.

LaTeX Lean

Theorem 9Conservation of angular momentum

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.

LaTeX Lean

Lemma 14Basic canonical brackets

The coordinate functions satisfy:

\[ \{ q_i, q_j\} = 0, \qquad \{ p_i, p_j\} = 0, \qquad \{ q_i, p_j\} = \delta _{ij}. \]

Proof ▶

From the definition, $\{ q_i, q_j\} = \sum _k(\delta _{ik} \cdot 0 - 0 \cdot \delta _{jk}) = 0$, and $\{ p_i, p_j\} = 0$ similarly. For the mixed bracket: $\{ q_i, p_j\} = \sum _k \delta _{ik}\delta _{jk} = \delta _{ij}$.

LaTeX Lean

Proposition 12Basic identities for $L$, $A$, and $H$

Away from collision, the following four identities hold:

$L \cdot A = 0$ ($L$ and $A$ are perpendicular)
$A \in \mathrm{span}\{ q, p\} $ ($A$ lies in the orbital plane)
$A \cdot q = \| L\| ^2 - m\mu r$
$\| A\| ^2 = (m\mu )^2 + 2mH\| L\| ^2$.

Proof ▶

(i). Since $L = q \times p$, the vector $L$ is perpendicular to both $q$ and $p$. Therefore:

\[ L \cdot A = L \cdot (p \times L) - \frac{m\mu }{r}(L \cdot q) = 0 - 0 = 0. \]

(The scalar triple product $L \cdot (p \times L) = (L \times p) \cdot L$ vanishes because a cross product is perpendicular to both factors.)

(ii). Apply the BAC-CAB identity to $p \times L = p \times (q \times p)$:

\[ p \times (q \times p) = q\| p\| ^2 - p(q \cdot p). \]

Both terms are scalar multiples of $q$ and $p$, so $A = p \times L - (m\mu /r)q \in \mathrm{span}\{ q, p\} $.

(iii). Use the cyclic property of the scalar triple product:

\[ (p \times L) \cdot q = L \cdot (q \times p) = L \cdot L = \| L\| ^2. \]

Therefore:

\[ A \cdot q = (p \times L) \cdot q - \frac{m\mu }{r}\| q\| ^2 = \| L\| ^2 - m\mu r. \]

(iv). Since $p \perp L$, we have $\| p \times L\| ^2 = \| p\| ^2\| L\| ^2$. Using the result of (iii) for the cross term:

\begin{align*} \| A\| ^2 & = \| p \times L\| ^2 - \frac{2m\mu }{r}(p \times L) \cdot q + (m\mu )^2 \\ & = \| p\| ^2\| L\| ^2 - \frac{2m\mu }{r}\| L\| ^2 + (m\mu )^2 \\ & = \left(\| p\| ^2 - \frac{2m\mu }{r}\right)\| L\| ^2 + (m\mu )^2 \\ & = 2mH\| L\| ^2 + (m\mu )^2. \end{align*}

LaTeX Lean

Theorem 26Cartesian ellipse form

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. \]

LaTeX Lean

Theorem 34Area of one full orbit

If $T$ is a configuration period, then $\mathcal{A}(0, T) = \pi ab$.

Proof ▶

By Proposition 33, the orbit sweeps the interior of the ellipse exactly once over $[0, T]$. The area enclosed by an ellipse with semi-axes $a$ and $b$ is $\pi ab$.

LaTeX Lean

Proposition 24Planarity and parameter relations

Assume $H {\lt} 0$ and $L \neq 0$. Then:

Planarity. The position $q(t)$ and momentum $p(t)$ stay in the fixed plane $\Pi = \{ y \in \mathbb {R}^3 : L \cdot y = 0\} $. The Lenz vector $A$ also lies in $\Pi $.
$0 \le e {\lt} 1$, $a {\gt} 0$, $b {\gt} 0$.
$b^2 = a\ell $.
$b = a\sqrt{1-e^2}$.
$\sqrt{a^2 - b^2} = ae$ (focal distance formula).

Proof ▶

(a). Since $L = q \times p$, the vector $L$ is perpendicular to both $q$ and $p$ at every instant. Because $L$ is constant, the plane $\Pi $ is fixed, and $q(t)$ stays in it for all time. The vector $A$ lies in $\Pi $ by identity (i): $L \cdot A = 0$.

(b). From identity (iv):

\[ e^2 = \frac{\| A\| ^2}{(m\mu )^2} = 1 + \frac{2H\| L\| ^2}{m\mu ^2}. \]

Since $H {\lt} 0$ and $\| L\| {\gt} 0$, we get $e^2 {\lt} 1$, so $0 \le e {\lt} 1$. Since $H {\lt} 0$, $a = -\mu /(2H) {\gt} 0$. Also $1-e^2 {\gt} 0$, so $\sqrt{1-e^2} {\gt} 0$. Hence $b = a\sqrt{1-e^2} {\gt} 0$.

(c). Substitute the definitions:

\[ a\ell = \frac{-\mu }{2H} \cdot \frac{\| L\| ^2}{m\mu } = \frac{-\| L\| ^2}{2mH} = b^2. \]

(d). From (b) and (c): $e^2 = 1 - \ell /a = 1 - b^2/a^2$, so $b^2 = a^2(1-e^2)$, giving $b = a\sqrt{1-e^2}$.

(e). From (d): $a^2 - b^2 = a^2 - a^2(1-e^2) = a^2 e^2$, so $\sqrt{a^2-b^2} = ae$.

LaTeX

Lean

Kepler.planarity
Kepler.eccentricity_lt_one
Kepler.semi_major_axis
Kepler.semiLatusRectum_eq_semiMajorAxis_mul_one_sub_eccentricity_sq
Kepler.semiMinorAxis_sq

Proposition 33One period traverses the ellipse once

For a bounded orbit with configuration period $T$, the orbit traces the ellipse exactly once over $[0, T]$.

Proof ▶

Lean proves that there are orthonormal vectors $e_A$ and $e_B$ in the orbital plane and a function $\theta (t)$ such that

\[ q(t) = a(\cos \theta (t) - e)e_A + b \sin \theta (t)e_B. \]

So $\theta (t)$ parametrizes the ellipse. The same theorem also gives a derivative formula for $\theta $. Since $x(t) = a(\cos \theta (t) - e)$ and $y(t) = b\sin \theta (t)$ together determine $q(t)$ in the orbital plane, the angle $\theta (t)$ determines $q(t)$. Note that for the eccentric anomaly, $r(t) = a(1 - e\cos \theta (t))$.

The Lean theorem gives the areal velocity formula in terms of $\theta $:

\[ \frac{d\mathcal A}{dt} = \frac{ab}{2}(1 - e\cos \theta (t))\, \dot\theta (t). \]

The second law says this equals the positive constant $\| L\| /(2m)$. Since $0 \le e {\lt} 1$, we have $1 - e\cos \theta {\gt} 0$, so it follows that

\[ \dot\theta = \frac{\| L\| }{mab(1 - e\cos \theta )} {\gt} 0. \]

So $\theta (t)$ is strictly increasing. The orbit is traversed in one direction.

The Lean theorem also states that $\theta (T) = \theta (0) + 2\pi $. Therefore $q$ traces the ellipse exactly once.

LaTeX Lean

Theorem 11Conservation of energy

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. \]

LaTeX Lean

Theorem 31Equal areas in equal times

Two time intervals of the same length sweep the same area.

Proof ▶

The swept area on $[t_1, t_1 + \Delta t]$ equals $(\| L\| /2m) \cdot \Delta t$, which depends only on the length $\Delta t$. So any two intervals of length $\Delta t$ sweep equal areas.

LaTeX

Lean

Kepler.equal_areas_in_equal_times
Kepler.kepler_second_law_source

Theorem 27The origin is a focus

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.

LaTeX

Lean

Kepler.kepler_first_law_focus_geometry
Kepler.kepler_first_law_origin_is_focus

Theorem 28Kepler’s First Law

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).

LaTeX Lean

Theorem 21Hidden $\mathfrak {so}(4)$ comoment map

On the shell $H = h {\lt} 0$, the map

\[ \mu _h(u, v) = L_u + K_v \]

is an $\mathfrak {so}(4)$-comoment map for the bracket of Proposition 20.

Proof ▶

We check directly that $\{ \mu _h(u,v), \mu _h(u',v')\} = \mu _h([(u,v),(u',v')])$. The only subtlety is that the formula

\[ \{ A_u, A_v\} = -2mH\, L_{u \times v} \]

holds on the full phase space, where $H$ is still a function. We may replace $H$ by the constant $h$ only after restricting to the surface $M_h$.

From Theorem 18 and the definition of $K_u$:

\[ \{ K_u, K_v\} = \frac{1}{-2mh}\{ A_u, A_v\} = \frac{-2mH}{-2mh}L_{u \times v} = L_{u \times v} \quad \text{(since $H = h$ on $M_h$)}. \]

Also $\{ L_u, K_v\} = K_{u \times v}$ because $L_u$ rotates $A$ (and hence $K$) by the same formula as for $L$. Therefore:

\begin{align*} \{ L_u + K_v,\, L_{u'} + K_{v'}\} & = \{ L_u, L_{u'}\} + \{ L_u, K_{v'}\} + \{ K_v, L_{u'}\} + \{ K_v, K_{v'}\} \\ & = L_{u \times u'} + K_{u \times v'} + K_{v \times u'} + L_{v \times v'} \\ & = L_{u \times u' + v \times v'} + K_{u \times v' + v \times u'} \\ & = \mu _h\bigl([(u,v),(u’,v’)]\bigr). \end{align*}

LaTeX

Lean

Kepler.hidden_so4_shell_algebra
Kepler.hidden_so4_comoment

Theorem 18Poisson algebra of $L$ and $A$

Away from collision, for all $u, v \in \mathbb {R}^3$:

\[ \{ L_u, L_v\} = L_{u \times v}, \qquad \{ L_u, A_v\} = A_{u \times v}, \qquad \{ A_u, A_v\} = -2mH\, L_{u \times v}. \]

Both $L_u$ and $A_u$ Poisson-commute with $H$.

Proof ▶

The first identity is Theorem 17. The second follows because $A$ is built from $q$ and $p$ by vector operations that commute with rotations. Since $L_u$ rotates both $q$ and $p$, it also rotates every vector expression built from them. Explicitly, using the same Leibniz argument: $\{ L_u, A\} = u \times A$, so $\{ L_u, A_v\} = v \cdot (u \times A) = (u \times v) \cdot A = A_{u \times v}$.

For the third identity, $\{ A_u, A_v\} = -2mH\, L_{u \times v}$, we expand $A = F - m\mu U$. The right-hand side still contains the energy function $H$. Only after restricting to a fixed-energy surface will that coefficient become a constant.

Write $A = F - m\mu U$ where

\[ F = p \times L, \qquad U = \frac{q}{r}. \]

For constant $u$, let $F_u = u \cdot F$ and $U_u = u \cdot U$. Expand:

\[ \{ A_u, A_v\} = \{ F_u, F_v\} - m\mu \bigl(\{ F_u, U_v\} + \{ U_u, F_v\} \bigr) + (m\mu )^2\{ U_u, U_v\} . \]

So we compute three smaller brackets.

Step 1: $\{ F_u, F_v\} = -\| p\| ^2 L_{u \times v}$. Write $F_u = \| p\| ^2 X_u - (q \cdot p) P_u$ where $X_u = u \cdot q$ and $P_u = u \cdot p$. From the canonical brackets and the Leibniz rule:

\begin{align*} \{ q \cdot p,\, X_u\} & = -X_u, \qquad \{ q \cdot p,\, P_u\} = P_u, \\ \{ \| p\| ^2,\, X_u\} & = -2P_u, \qquad \{ \| p\| ^2,\, P_u\} = 0. \end{align*}

Expanding $\{ F_u, F_v\} $ by bilinearity and collecting all terms gives:

\[ \{ F_u, F_v\} = \| p\| ^2(P_u X_v - P_v X_u) = -\| p\| ^2\, L_{u \times v}. \]

Step 2: $\{ F_u, U_v\} + \{ U_u, F_v\} = -(2/r)\, L_{u \times v}$. Using the Leibniz rule on $U_v = X_v/r$:

\[ \{ F_u, U_v\} = \frac{\{ F_u, X_v\} }{r} + X_v\{ F_u, r^{-1}\} . \]

Computing $\{ F_u, X_v\} $ and $\{ F_u, r\} $ from the Leibniz rule, then adding the antisymmetric term $\{ U_u, F_v\} $, all remaining terms cancel except:

\[ \{ F_u, U_v\} + \{ U_u, F_v\} = -\frac{2}{r}\, L_{u \times v}. \]

Step 3: $\{ U_u, U_v\} = 0$. Both $U_u$ and $U_v$ depend only on $q$, so all $p$-derivatives vanish and the bracket is zero.

Combining:

\begin{align*} \{ A_u, A_v\} & = -\| p\| ^2 L_{u \times v} + m\mu \cdot \frac{2}{r}\, L_{u \times v} \\ & = -\! \left(\| p\| ^2 - \frac{2m\mu }{r}\right)L_{u \times v} = -2mH\, L_{u \times v}. \end{align*}

LaTeX

Lean

Kepler.poisson_L_u_H
Kepler.poisson_A_u_H
Kepler.LA_poisson_algebra

Theorem 10Conservation of the Laplace–Runge–Lenz vector

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. \]

LaTeX Lean

Proposition 20The model algebra is $\mathfrak {so}(4)$

On $\mathbb {R}^3 \oplus \mathbb {R}^3$, define the bracket:

\[ [(u,v),(u',v')] = \bigl(u \times u' + v \times v',\, u \times v' + v \times u'\bigr). \]

This is isomorphic to $\mathfrak {so}(4)$ via the linear bijection $\Phi \colon \mathbb {R}^3 \oplus \mathbb {R}^3 \to \mathfrak {so}(4)$:

\[ \Phi (u,v) = \begin{pmatrix} 0 & -u_3 & u_2 & v_1 \\ u_3 & 0 & -u_1 & v_2 \\ -u_2 & u_1 & 0 & v_3 \\ -v_1 & -v_2 & -v_3 & 0 \end{pmatrix}. \]

Proof ▶

The matrix $\Phi (u, v)$ is antisymmetric, so it lies in $\mathfrak {so}(4)$. The map $\Phi $ is linear and bijective (both spaces are six-dimensional). A direct matrix multiplication verifies the bracket identity $[\Phi (u,v), \Phi (u',v')] = \Phi ([(u,v),(u',v')])$, so $\Phi $ is a Lie algebra isomorphism.

LaTeX

Lean

Kepler.Phi
Kepler.so4_model_isomorphic_to_so4

Proposition 7Momentum equation

For every solution, $\dot p = -\mu q/\| q\| ^3$.

Proof ▶

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

\[ \dot p(t) = -\mu \frac{q(t)}{\| q(t)\| ^3}. \]

LaTeX Lean

Theorem 25Exact orbit equation

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.

LaTeX Lean

Theorem 15Hamilton equations from the Poisson bracket

The Kepler equations of motion arise from the Poisson bracket with $H$:

\[ \{ q_i, H\} = \frac{p_i}{m}, \qquad \{ p_i, H\} = -\frac{\mu q_i}{\| q\| ^3}. \]

Proof ▶

By the canonical brackets and the chain rule:

\[ \{ q_i, H\} = \frac{\partial H}{\partial p_i} = \frac{p_i}{m}. \]

For the momentum bracket:

\[ \{ p_i, H\} = -\frac{\partial H}{\partial q_i} = -\frac{\partial }{\partial q_i}\! \left(-\frac{\mu }{\| q\| }\right) = -\frac{\mu q_i}{\| q\| ^3}. \]

LaTeX

Lean

Kepler.kepler_equations_poisson
Kepler.kepler_equations_poisson_vector

Proposition 6Position equation

For every solution, $\dot q = p/m$.

Proof ▶

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

\[ \dot q(t) = \frac{1}{m}p(t). \]

LaTeX Lean

Proposition 8The Kepler force is radial

For every solution, $q \times \dot p = 0$.

Proof ▶

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:

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

LaTeX Lean

Theorem 17Rotational comoment

The map $u \mapsto L_u$ is an $\mathfrak {so}(3)$-comoment map. Concretely:

\begin{align*} \{ q_i, L_u\} & = (u \times q)_i, \\ \{ p_i, L_u\} & = (u \times p)_i, \\ \{ L_u, L_v\} & = L_{u \times v}, \\ \{ L_u, H\} & = 0. \end{align*}

Proof ▶

We first identify the infinitesimal motion generated by $L_u$. Since

\[ L_u = (u \times q) \cdot p, \]

its derivative with respect to $p_i$ is $(u \times q)_i$. Therefore

\[ \{ q_i, L_u\} = (u \times q)_i. \]

So the Hamiltonian flow of $L_u$ rotates the position vector about the axis $u$.

Next rewrite $L_u$ as

\[ L_u = q \cdot (p \times u). \]

Then

\[ \frac{\partial L_u}{\partial q_i} = (p \times u)_i = -(u \times p)_i, \]

and therefore

\[ \{ p_i, L_u\} = (u \times p)_i. \]

So the same Hamiltonian simultaneously rotates the momentum vector about the same axis.

This proves the infinitesimal symmetry statement. To prove the comoment property, we must show that Poisson brackets of the functions $L_u$ reproduce the Lie bracket on $\mathfrak {so}(3)$. Apply the Leibniz rule to $L = q \times p$:

\[ \{ L_u, L\} = \{ L_u, q\} \times p + q \times \{ L_u, p\} = (u \times q) \times p + q \times (u \times p) = u \times (q \times p) = u \times L. \]

Therefore $\{ L_u, L_v\} = v \cdot \{ L_u, L\} = v \cdot (u \times L) = (u \times v) \cdot L = L_{u \times v}$. That is exactly the Lie bracket relation for $\mathfrak {so}(3) \cong \mathbb {R}^3$ with bracket $u \times v$.

Finally, $L_u$ is conserved because it generates rotations and the Hamiltonian only depends on the rotation-invariant quantities $\| p\| ^2$ and $r = \| q\| $. Indeed,

\[ \{ \| p\| ^2, L_u\} = 2p \cdot (u \times p) = 0, \qquad \{ r, L_u\} = \frac{q}{r} \cdot (u \times q) = 0. \]

Hence $\{ H, L_u\} = 0$, and by antisymmetry also $\{ L_u, H\} = 0$.

LaTeX Lean

Theorem 30Constant areal velocity

If $L \neq 0$, the signed areal velocity is constant and equal to $\| L\| /(2m)$.

Proof ▶

By definition,

\[ \frac{d\mathcal{A}}{dt} = \frac{1}{2m}\hat L_0 \cdot (q(t) \times p(t)), \]

where $\hat L_0 = L(0)/\| L(0)\| $. By conservation of angular momentum, $q(t) \times p(t) = L(0)$. Therefore

\[ \frac{d\mathcal{A}}{dt} = \frac{1}{2m}\hat L_0 \cdot L(0) = \frac{\| L\| }{2m}. \]

LaTeX Lean

Corollary 37Comoment formulation of the full proof

For the same solution, the map $u \mapsto L_u$ is an $\mathfrak {so}(3)$-comoment (Theorem 17), and on the shell $H = h {\lt} 0$ the map $(u, v) \mapsto L_u + K_v$ is an $\mathfrak {so}(4)$-comoment (Theorem 21). Combining these statements with Theorem 36 gives the full comoment-map proof of Kepler’s laws.

Proof ▶

Theorems 17, 21, and 36.

LaTeX

Lean

Kepler.hidden_so4_comoment_source
Kepler.kepler_laws_from_comoment_source

Theorem 35Kepler’s third law

For an orbital period $T$,

\[ T^2 = \frac{4\pi ^2 m}{\mu }\, a^3. \]

Proof ▶

By the second law, the area swept over one period is:

\[ \mathcal{A}(0, T) = \frac{\| L\| }{2m} \cdot T. \]

By Theorem 34, this equals $\pi ab$. So:

\[ T = \frac{2\pi m ab}{\| L\| }. \]

Squaring:

\[ T^2 = \frac{4\pi ^2 m^2 a^2 b^2}{\| L\| ^2}. \]

From Proposition 24(c), $b^2 = a\ell = a\| L\| ^2/(m\mu )$, so $\| L\| ^2 = mb^2\mu /a$. Substituting:

\[ T^2 = \frac{4\pi ^2 m^2 a^2 b^2}{mb^2\mu /a} = \frac{4\pi ^2 m}{\mu }\, a^3. \]

LaTeX

Lean

Kepler.kepler_third_law_of_period_and_area
Kepler.kepler_third_law

Theorem 36Kepler’s three laws

Let $\gamma $ be a non-collision solution with $H {\lt} 0$ and $L \neq 0$. Then:

First law. The orbit lies in the plane $\Pi $ perpendicular to $L$ and is an ellipse with the origin at one focus. Its eccentricity is $e = \| A\| /(m\mu ) {\lt} 1$, its semi-major axis is $a = -\mu /(2H)$, and its semi-latus rectum is $\ell = \| L\| ^2/(m\mu )$.
Second law. The areal velocity $d\mathcal{A}/dt = \| L\| /(2m)$ is constant, so equal areas are swept in equal times.
Third law. Every configuration period $T$ satisfies $T^2 = (4\pi ^2 m/\mu )\, a^3$.

Proof ▶

Part (1) is Theorem 28. Part (2) is Theorem 31. Part (3) is Theorem 35.

LaTeX Lean

Corollary 22Two commuting copies of $\mathfrak {so}(3)$

On the shell $M_h$, define:

\[ J^+_u = \tfrac {1}{2}(L_u + K_u), \qquad J^-_u = \tfrac {1}{2}(L_u - K_u). \]

Then $J^+$ and $J^-$ each satisfy the $\mathfrak {so}(3)$ bracket, and they commute with each other:

\[ \{ J^+_u, J^+_v\} = J^+_{u \times v}, \qquad \{ J^-_u, J^-_v\} = J^-_{u \times v}, \qquad \{ J^+_u, J^-_v\} = 0. \]

So $\mathfrak {so}(4) \cong \mathfrak {so}(3) \oplus \mathfrak {so}(3)$ via the splitting $(L, K) \mapsto (J^+, J^-)$.

Proof ▶

For the commutator, expand using the brackets from Theorem 21:

\begin{align*} \{ J^+_u, J^-_v\} & = \tfrac {1}{4}\bigl(\{ L_u, L_v\} - \{ L_u, K_v\} + \{ K_u, L_v\} - \{ K_u, K_v\} \bigr) \\ & = \tfrac {1}{4}\bigl(L_{u \times v} - K_{u \times v} + K_{u \times v} - L_{u \times v}\bigr) = 0. \end{align*}

The self-brackets $\{ J^+_u, J^+_v\} = J^+_{u \times v}$ and $\{ J^-_u, J^-_v\} = J^-_{u \times v}$ follow similarly.

LaTeX

Lean

Kepler.Jplus_u
Kepler.Jminus_u
Kepler.two_commuting_so3