1 Introduction

This blueprint accompanies a Lean 4 formalization of Kepler’s three laws of planetary motion. It follows the proof strategy of Guillemin and Sternberg in Variations on a Theme by Kepler.

The physical setup. We study a particle of mass \(m\) moving in \(\mathbb {R}^3\) under the gravitational attraction of a fixed body at the origin. Its position is \(q \in \mathbb {R}^3\) and its momentum is \(p \in \mathbb {R}^3\). The Hamiltonian is

\[ H(q,p) = \frac{\| p\| ^2}{2m} - \frac{\mu }{\| q\| }, \]

where \(\mu {\gt} 0\) is the gravitational parameter. The kinetic energy is \(\| p\| ^2/(2m)\) and the potential energy is \(-\mu /\| q\| \). We only consider non-collision trajectories, meaning \(\| q(t)\| \neq 0\) for all \(t\).

What negative energy means. The condition \(H {\lt} 0\) says that the total energy is negative. The motion is then bounded. For the inverse-square law, this is exactly the case of ellipses. If one fixes a specific value \(h {\lt} 0\), then the equation \(H = h\) cuts out a five-dimensional level set inside the six-dimensional phase space. In Lean we also keep the non-collision condition \(r \neq 0\) as part of this fixed-energy surface. This level set is often called an energy shell. We will usually say fixed-energy surface. It is just the set of phase points with that one fixed energy.

What we prove. For every non-collision trajectory with negative energy and nonzero angular momentum, we prove:

First law. The orbit lies in a fixed plane and is an ellipse with the origin at one focus.
Second law. The line from the origin to the planet sweeps area at a constant rate:

\[ \frac{d\mathcal{A}}{dt} = \frac{\| L\| }{2m}, \]

where \(L = q \times p\) is the angular momentum vector. Equal areas are swept in equal times.
Third law. If \(T\) is the orbital period and \(a\) is the semi-major axis, then

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

The two key conserved vectors. Two vector quantities stay constant along every Kepler trajectory. The first is the angular momentum

\[ L = q \times p. \]

Because \(L\) is perpendicular to both \(q\) and \(p\), its constancy immediately forces the motion to stay in one fixed plane.

The second is the Laplace–Runge–Lenz vector

\[ A = p \times L - \frac{m\mu }{\| q\| }q. \]

It points along the major axis of the orbit toward perihelion. Its length records the eccentricity. Thus \(L\) determines the orbital plane and \(A\) determines the ellipse in that plane.

Proof sketch. First, conservation of \(L\) gives a fixed plane, so the motion is two-dimensional. Next, the identity

\[ A \cdot q = \| L\| ^2 - m\mu r \qquad (r = \| q\| ) \]

turns the constancy of \(A\) into the polar equation

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

which is the equation of a conic with focus at the origin. The negative-energy condition then implies \(0 \le e {\lt} 1\), so the conic is an ellipse. That proves Kepler’s first law.

Kepler’s second law comes from the same conserved angular momentum:

\[ \frac{d\mathcal A}{dt} = \frac{\| L\| }{2m}. \]

So the areal velocity is constant. Finally, one full period sweeps exactly the area \(\pi ab\) of the ellipse, and comparing that area with the constant areal velocity gives

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

That is Kepler’s third law.

Momentum maps and comoment maps. Let \(\mathfrak {g}\) be a Lie algebra acting on a phase space \(M\). A momentum map is a map

\[ \mu \colon M \longrightarrow \mathfrak {g}^*. \]

The corresponding comoment map is the scalar-valued map

\[ \tilde\mu \colon \mathfrak {g} \longrightarrow C^\infty (M) \]

given by

\[ \tilde\mu (\xi )(x) = \langle \mu (x), \xi \rangle . \]

The defining relation is

\[ \bigl\{ \tilde\mu (u),\, \tilde\mu (v)\bigr\} = \tilde\mu \bigl([u,v]\bigr) \qquad \text{for all } u, v \in \mathfrak {g}. \]

So each \(u \in \mathfrak {g}\) gives a Hamiltonian function \(\tilde\mu (u)\). Its Poisson brackets match the Lie bracket in \(\mathfrak {g}\). Lean uses this scalar-valued form.

We identify \(\mathfrak {so}(3) \cong \mathbb {R}^3\) with bracket \([u,v] = u \times v\). For any \(u \in \mathbb {R}^3\), the function \(L_u := u \cdot L = u \cdot (q \times p)\) is conserved. The map \(u \mapsto L_u\) is an \(\mathfrak {so}(3)\)-comoment: it satisfies \(\{ L_u, L_v\} = L_{u \times v}\), which is exactly the comoment condition.

The fixed negative-energy surface and the hidden \(\mathfrak {so}(4)\) symmetry. The bracket identities for \(L\) and \(A\) depend on the energy:

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

So the sign of \(H\) matters. When \(H {\gt} 0\) one gets a different symmetry algebra. When \(H = 0\) one gets a limiting case. For Kepler’s laws for bounded orbits, the relevant case is \(H {\lt} 0\).

Fix \(h {\lt} 0\) and restrict attention to the fixed-energy surface \(H = h\). Because \(h\) is now a fixed negative number, the quantity \(-2mh\) is positive and we may rescale \(A\) by the real factor \(\sqrt{-2mh}\). Define

\[ K = \frac{A}{\sqrt{-2mh}}. \]

This rescaling removes the factor \(-2mH\) from the bracket once we are on the level set \(H = h\).

On the fixed-energy surface one gets

\[ \{ K_u, K_v\} = L_{u \times v}, \qquad \{ L_u, K_v\} = K_{u \times v}. \]

The six observables \(L_u\) and \(K_u\) therefore satisfy the bracket relations of \(\mathfrak {so}(4)\). The map \((u, v) \mapsto L_u + K_v\) is an \(\mathfrak {so}(4)\)-comoment on that fixed-energy surface. Here hidden symmetry means an extra conserved quantity that does not come from the standard action of spatial rotations. Without this extra conserved quantity, central-force orbits usually precess and do not close.

Proof in Lean.

Verify the equations of motion: \(\dot q = p/m\) and \(\dot p = -\mu q/\| q\| ^3\).
Prove that \(L\), \(A\), and \(H\) are constant along every solution.
Establish algebraic identities connecting \(L\), \(A\), and \(H\), in particular \(\| A\| ^2 = (m\mu )^2 + 2mH\| L\| ^2\).
Set up the Poisson bracket and show \(u \mapsto L_u\) is an \(\mathfrak {so}(3)\)-comoment.
Prove \(\{ A_u, A_v\} = -2mH\, L_{u \times v}\) and then, on the fixed-energy surface \(H = h {\lt} 0\), rescale to the hidden \(\mathfrak {so}(4)\) symmetry.
Use \(L\) to get a fixed orbital plane and use \(A \cdot q = \| L\| ^2 - m\mu r\) to derive \(r = \ell /(1 + e\cos \theta )\).
Use the negative-energy identity for \(\| A\| ^2\) to prove \(0 \le e {\lt} 1\), so the conic is an ellipse with the origin at a focus.
Use the constant areal velocity to prove the second law.
Combine the areal velocity with the ellipse area \(\pi ab\) to obtain the period law.

Geometry. The orbit lies in the plane perpendicular to \(L\). Inside that plane, \(A\) points toward perihelion. The origin is a focus of the ellipse. The major axis has length \(2a\).

Ellipse terminology. The major axis is the longest line through the center of the ellipse. The minor axis is the shortest line through the center and perpendicular to the major axis. The semi-major axis is half of the major axis. The semi-minor axis is half of the minor axis. If \(F\) is a focus, then the latus rectum is the chord through \(F\) perpendicular to the major axis. Its half-length is the semi-latus rectum \(\ell \). For an ellipse one has \(\ell = b^2/a\).

\includegraphics[width=7cm]{figures/ellipse-axes.png} — Figure 1.1 Basic ellipse axis terminology. Source: Wikimedia Commons, “Ellipse semi-major and minor axes.svg” by M. W. Toews. CC0 1.0.

Note on the Lean formalization. The source text works on \(T^*(\mathbb {R}^3 \setminus \{ 0\} )\). The Lean development instead uses the ambient space \(\mathbb {R}^3 \times \mathbb {R}^3\) and adds the hypothesis \(r \neq 0\) wherever needed. Each theorem below cites the Lean declaration that proves the same statement. The prose proofs summarize those same arguments at the mathematical level.