From 3ccd6b0f6b3b8ddd874aa3c0fce581267fb88429 Mon Sep 17 00:00:00 2001 From: Hannah Date: Fri, 20 Feb 2026 00:54:22 +0000 Subject: [PATCH 1/3] Initial Commit --- .../Lagrangian/OrbitalMechanics.lean | 25 +++++++++++++++++++ 1 file changed, 25 insertions(+) create mode 100644 PhysLean/ClassicalMechanics/Lagrangian/OrbitalMechanics.lean diff --git a/PhysLean/ClassicalMechanics/Lagrangian/OrbitalMechanics.lean b/PhysLean/ClassicalMechanics/Lagrangian/OrbitalMechanics.lean new file mode 100644 index 00000000..003fdf72 --- /dev/null +++ b/PhysLean/ClassicalMechanics/Lagrangian/OrbitalMechanics.lean @@ -0,0 +1,25 @@ +/-! +Copyright (c) 2026 Hannah Dawe. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Hannah Dawe +-/ + +import Mathlib.Data.Real.Basic + +/-! +# Circular Orbit Vis Viva +Defines the orbital speed for a circular orbit (v^2 = G M / r). +-/ + +namespace ClassicalMechanics + +/-- Orbital speed for a circular orbit. -/ +def vis_viva_circle (G M r : ℝ) : ℝ := + Real.sqrt (G * M / r) + +/-- Lemma: the square of the circular orbit speed equals G M / r. -/ +lemma vis_viva_circle_sq (G M r : ℝ) (hr : r > 0) : + (vis_viva_circle G M r)^2 = G * M / r := by + simp [vis_viva_circle, Real.sqrt_sq hr.le] + +end ClassicalMechanics From 4b5f98d09f7949a2a10010690f4d8a4568000937 Mon Sep 17 00:00:00 2001 From: Hannah Date: Sat, 21 Feb 2026 01:35:40 +0000 Subject: [PATCH 2/3] added imports to PhysLean.lean to pass checks. Created OrbitalMechanics folder and renamed file to VisViva.lean. --- PhysLean.lean | 1 + .../VisViva.lean} | 11 ++++++----- 2 files changed, 7 insertions(+), 5 deletions(-) rename PhysLean/ClassicalMechanics/{Lagrangian/OrbitalMechanics.lean => OrbitalMechanics/VisViva.lean} (69%) diff --git a/PhysLean.lean b/PhysLean.lean index 920ac6ec..6f7c87a4 100644 --- a/PhysLean.lean +++ b/PhysLean.lean @@ -7,6 +7,7 @@ import PhysLean.ClassicalMechanics.HarmonicOscillator.ConfigurationSpace import PhysLean.ClassicalMechanics.HarmonicOscillator.Solution import PhysLean.ClassicalMechanics.Lagrangian.TotalDerivativeEquivalence import PhysLean.ClassicalMechanics.Mass.MassUnit +import Physlean.ClassicalMechanics.OrbitalMechanics.VisViva import PhysLean.ClassicalMechanics.Pendulum.CoplanarDoublePendulum import PhysLean.ClassicalMechanics.Pendulum.MiscellaneousPendulumPivotMotions import PhysLean.ClassicalMechanics.Pendulum.SlidingPendulum diff --git a/PhysLean/ClassicalMechanics/Lagrangian/OrbitalMechanics.lean b/PhysLean/ClassicalMechanics/OrbitalMechanics/VisViva.lean similarity index 69% rename from PhysLean/ClassicalMechanics/Lagrangian/OrbitalMechanics.lean rename to PhysLean/ClassicalMechanics/OrbitalMechanics/VisViva.lean index 003fdf72..cdd0de78 100644 --- a/PhysLean/ClassicalMechanics/Lagrangian/OrbitalMechanics.lean +++ b/PhysLean/ClassicalMechanics/OrbitalMechanics/VisViva.lean @@ -1,4 +1,4 @@ -/-! +/- Copyright (c) 2026 Hannah Dawe. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Hannah Dawe @@ -6,6 +6,7 @@ Authors: Hannah Dawe import Mathlib.Data.Real.Basic + /-! # Circular Orbit Vis Viva Defines the orbital speed for a circular orbit (v^2 = G M / r). @@ -14,12 +15,12 @@ Defines the orbital speed for a circular orbit (v^2 = G M / r). namespace ClassicalMechanics /-- Orbital speed for a circular orbit. -/ -def vis_viva_circle (G M r : ℝ) : ℝ := +def vis_viva_circular (G M r : ℝ) : ℝ := Real.sqrt (G * M / r) /-- Lemma: the square of the circular orbit speed equals G M / r. -/ -lemma vis_viva_circle_sq (G M r : ℝ) (hr : r > 0) : - (vis_viva_circle G M r)^2 = G * M / r := by - simp [vis_viva_circle, Real.sqrt_sq hr.le] +lemma vis_viva_circular_sq (G M r : ℝ) (hr : r > 0) : + (vis_viva_circular G M r)^2 = G * M / r := by + simp [vis_viva_circular, Real.sqrt_sq hr.le] end ClassicalMechanics From 246f416ed389e4f38dafb4af030b4012eabbd54f Mon Sep 17 00:00:00 2001 From: Hannah Date: Mon, 23 Feb 2026 22:19:35 +0000 Subject: [PATCH 3/3] Adding VisViva Structure, ConfigurationSpace, and renaming def to remove _. Fixed spelling mistake in PhysLean.lean. --- PhysLean.lean | 2 +- .../OrbitalMechanics/VisViva.lean | 23 ++++++++++++++----- 2 files changed, 18 insertions(+), 7 deletions(-) diff --git a/PhysLean.lean b/PhysLean.lean index 6f7c87a4..9f1ced34 100644 --- a/PhysLean.lean +++ b/PhysLean.lean @@ -7,7 +7,7 @@ import PhysLean.ClassicalMechanics.HarmonicOscillator.ConfigurationSpace import PhysLean.ClassicalMechanics.HarmonicOscillator.Solution import PhysLean.ClassicalMechanics.Lagrangian.TotalDerivativeEquivalence import PhysLean.ClassicalMechanics.Mass.MassUnit -import Physlean.ClassicalMechanics.OrbitalMechanics.VisViva +import PhysLean.ClassicalMechanics.OrbitalMechanics.VisViva import PhysLean.ClassicalMechanics.Pendulum.CoplanarDoublePendulum import PhysLean.ClassicalMechanics.Pendulum.MiscellaneousPendulumPivotMotions import PhysLean.ClassicalMechanics.Pendulum.SlidingPendulum diff --git a/PhysLean/ClassicalMechanics/OrbitalMechanics/VisViva.lean b/PhysLean/ClassicalMechanics/OrbitalMechanics/VisViva.lean index cdd0de78..342fd26d 100644 --- a/PhysLean/ClassicalMechanics/OrbitalMechanics/VisViva.lean +++ b/PhysLean/ClassicalMechanics/OrbitalMechanics/VisViva.lean @@ -6,7 +6,6 @@ Authors: Hannah Dawe import Mathlib.Data.Real.Basic - /-! # Circular Orbit Vis Viva Defines the orbital speed for a circular orbit (v^2 = G M / r). @@ -14,13 +13,25 @@ Defines the orbital speed for a circular orbit (v^2 = G M / r). namespace ClassicalMechanics +structure VisViva where + G : ℝ -- gravitational constant + M : ℝ -- central mass body + m : ℝ -- orbiting mass body # for later usage + +namespace VisViva + +structure ConfigurationSpace where + r : ℝ -- radius + /-- Orbital speed for a circular orbit. -/ -def vis_viva_circular (G M r : ℝ) : ℝ := - Real.sqrt (G * M / r) +def speedCircular (sys : VisViva) (cfg : ConfigurationSpace) : ℝ := + Real.sqrt (sys.G * sys.M / cfg.r) /-- Lemma: the square of the circular orbit speed equals G M / r. -/ -lemma vis_viva_circular_sq (G M r : ℝ) (hr : r > 0) : - (vis_viva_circular G M r)^2 = G * M / r := by - simp [vis_viva_circular, Real.sqrt_sq hr.le] +lemma speedCircular_sq (sys : VisViva) (cfg : ConfigurationSpace) (hr : cfg.r > 0) : + (speedCircular sys cfg)^2 = sys.G * sys.M / cfg.r := by + simp [speedCircular, Real.sqrt_sq hr.le] +end VisViva end ClassicalMechanics +