Physlib.ClassicalMechanics.OrbitalMechanics.VisViva

Imports

/-
Copyright (c) 2026 Hannah Dawe. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Hannah Dawe
-/

module

public import Mathlib.Analysis.Real.Sqrt

Circular Orbit Vis Viva

The vis-viva equation relates the speed of an orbiting body to its position and the mass of the central body. This module defines a simplified version of the vis-viva equation that is restricted to circular orbits (v^2 = G M / r).

@[expose] public section

System parameters for the vis-viva equation in circular orbital mechanics.

Gravitational constant.

Central mass body.

Orbiting mass body.

              structure VisViva where  G : ℝ  M : ℝ  m : ℝ

Configuration space for orbital mechanics, defining the orbital radius.

Orbital radius.

structure ConfigurationSpace where r : ℝ

Lemma: the square of the circular orbit speed equals G M / r.

lemma speedCircular_sq (sys : VisViva) (cfg : ConfigurationSpace) (hr : 0 < cfg.r) (hG : 0 < sys.G)
    (hM : 0 < sys.M) :
    (speedCircular sys cfg)^2 = sys.G * sys.M / cfg.r :=
  Real.sq_sqrt (bysys:VisVivacfg:ConfigurationSpacehr:0 < cfg.rhG:0 < sys.GhM:0 < sys.M⊢ 0 ≤ sys.G * sys.M / cfg.r positivityAll goals completed! 🐙)