From d02aae5f37bacdfc7162e0c42a3d08d9561d426c Mon Sep 17 00:00:00 2001 From: Pranav-Magdum Date: Tue, 5 May 2026 19:59:48 +0530 Subject: [PATCH 01/14] Add FreeParticle module for classical mechanics This file introduces the FreeParticle module in classical mechanics, detailing the properties and behaviors of a free particle, including Newton's second law, constant velocity, and energy conservation. --- .../FreeParticle/Basic.lean | 125 ++++++++++++++++++ 1 file changed, 125 insertions(+) create mode 100644 Physlib/ClassicalMechanics/FreeParticle/Basic.lean diff --git a/Physlib/ClassicalMechanics/FreeParticle/Basic.lean b/Physlib/ClassicalMechanics/FreeParticle/Basic.lean new file mode 100644 index 000000000..0c2673e67 --- /dev/null +++ b/Physlib/ClassicalMechanics/FreeParticle/Basic.lean @@ -0,0 +1,125 @@ +/- +Copyright (c) 2025 Pranav Magdum. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Pranav Magdum +-/ + +/-! +# The Free Particle + +## i. Overview + +The free particle is one of the simplest systems in classical mechanics: a particle of mass `m` +moving with no external forces acting on it. Physically, this means the particle just keeps moving +at constant velocity. + +In this file, we work in a simple 1D coordinate system where position and velocity are functions +of time with values in `ℝ`. This keeps things easy to reason about. A more complete treatment would +use manifolds and tangent bundles, but that’s overkill here. + +## ii. Key results + +The main things we show about the free particle are: + +In the `Basic` module: +- `FreeParticle` stores the mass of the particle. +- `NewtonsSecondLaw` encodes the equation `m * q'' = 0`. +- `accel_zero` shows that this implies `q'' = 0`. +- `velocity_const_of_zero_acc` shows that zero acceleration means velocity is constant. +- `energy_conservation_of_equationOfMotion` shows that kinetic energy stays constant over time. + +So overall, we formalise the usual chain: +Newton’s law → zero acceleration → constant velocity → constant energy. + +## iii. Table of contents + +- A. The setup +- B. Equation of motion + - B.1. Newton's second law + - B.2. Zero acceleration +- C. What zero acceleration implies + - C.1. Constant velocity +- D. Energy + - D.1. Kinetic energy + - D.2. Energy conservation + +## iv. References + +- Landau & Lifshitz, *Mechanics* +- Goldstein, *Classical Mechanics* + +-/ +import Mathlib.Data.Real.Basic +import Mathlib.Analysis.Calculus.Deriv.Basic +import Physlib.Meta.TODO.Basic +namespace ClassicalMechanics + +TODO "Make the documantation more descriptive" +TODO "Prove momentum conservation" +TODO "Prove the velocity_const_of_zero_acc lemma" + +structure FreeParticle where + mass : ℝ + mass_pos : 0 < mass + +namespace FreeParticle + +abbrev Time := ℝ +abbrev Trajectory := Time → ℝ + +noncomputable +def velocity (s : FreeParticle) (q : Trajectory) (t : Time) : ℝ := + deriv q t + +noncomputable +def kinetic_energy (s : FreeParticle) (q : Trajectory) (t : Time) : ℝ := + (1 / 2) * s.mass * (s.velocity q t)^2 + +def NewtonsSecondLaw (s : FreeParticle) (q : Trajectory) (t : Time) : Prop := + s.mass * deriv (s.velocity q) t = 0 + +-- Step 1: get q'' = 0 +lemma accel_zero + (s : FreeParticle) + (q : Trajectory) + (h : ∀ t, s.NewtonsSecondLaw q t) : + ∀ t, deriv (deriv q) t = 0 := by + intro t + have h₀ : s.mass ≠ 0 := ne_of_gt s.mass_pos + have h1 := h t + exact (mul_eq_zero.mp h1).resolve_left h₀ + +-- Step 2: velocity is constant +lemma velocity_const_of_zero_acc + (q : ℝ → ℝ) + (h : ∀ t, deriv (deriv q) t = 0) + (hcont : Continuous (deriv q)) : + ∃ v₀, ∀ t, deriv q t = v₀ := by + -- this is a standard analysis result (can be proved later) + sorry + +-- Step 3: Energy conservation +theorem Energy_is_Conserved + (s : FreeParticle) + (q : Trajectory) + (h : ∀ t, s.NewtonsSecondLaw q t) + (hcont : Continuous (deriv q)) : + ∃ E, ∀ t, s.kinetic_energy q t = E := by + + -- get q'' = 0 + have h_acc : ∀ t, deriv (deriv q) t = 0 := + accel_zero s q h + + -- get constant velocity + rcases velocity_const_of_zero_acc q h_acc hcont with ⟨v₀, hv⟩ + + -- energy is constant + have h_ke : ∀ t, s.kinetic_energy q t = (1 / 2) * s.mass * v₀^2 := by + intro t + unfold kinetic_energy velocity + rw [hv t] + + exact ⟨(1 / 2) * s.mass * v₀^2, h_ke⟩ + +end FreeParticle +end ClassicalMechanics From 6f392927263bf9b6c7defec653f8b58f3e6bfecf Mon Sep 17 00:00:00 2001 From: Pranav-Magdum Date: Tue, 5 May 2026 20:02:02 +0530 Subject: [PATCH 02/14] Add import for FreeParticle.Basic module --- Physlib.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Physlib.lean b/Physlib.lean index 19fd8fe2b..6fa28c5e3 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -2,6 +2,7 @@ module public import Physlib.ClassicalFieldTheory.Local.Variation public import Physlib.ClassicalMechanics.Basic +public import Physlib.ClassicalMechanics.FreeParticle.Basic public import Physlib.ClassicalMechanics.DampedHarmonicOscillator.Basic public import Physlib.ClassicalMechanics.EulerLagrange public import Physlib.ClassicalMechanics.HamiltonsEquations From 63797eab156eef9c966917d2f68e3b3f4bd96860 Mon Sep 17 00:00:00 2001 From: Pranav-Magdum Date: Wed, 6 May 2026 10:05:22 +0530 Subject: [PATCH 03/14] Update copyright year and improve comments Updated copyright year from 2025 to 2026 and modified text for clarity. --- Physlib/ClassicalMechanics/FreeParticle/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Physlib/ClassicalMechanics/FreeParticle/Basic.lean b/Physlib/ClassicalMechanics/FreeParticle/Basic.lean index 0c2673e67..a89b6daca 100644 --- a/Physlib/ClassicalMechanics/FreeParticle/Basic.lean +++ b/Physlib/ClassicalMechanics/FreeParticle/Basic.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2025 Pranav Magdum. All rights reserved. +Copyright (c) 2026 Pranav Magdum. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Pranav Magdum -/ @@ -15,7 +15,7 @@ at constant velocity. In this file, we work in a simple 1D coordinate system where position and velocity are functions of time with values in `ℝ`. This keeps things easy to reason about. A more complete treatment would -use manifolds and tangent bundles, but that’s overkill here. +use manifolds and tangent bundles. ## ii. Key results From eb7b8e7c141113774861ca6af203e1c015773149 Mon Sep 17 00:00:00 2001 From: Pranav-Magdum Date: Sat, 9 May 2026 20:07:55 +0530 Subject: [PATCH 04/14] Remove references section from Basic.lean Removed references to Landau & Lifshitz and Goldstein. --- Physlib/ClassicalMechanics/FreeParticle/Basic.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/Physlib/ClassicalMechanics/FreeParticle/Basic.lean b/Physlib/ClassicalMechanics/FreeParticle/Basic.lean index a89b6daca..840dac592 100644 --- a/Physlib/ClassicalMechanics/FreeParticle/Basic.lean +++ b/Physlib/ClassicalMechanics/FreeParticle/Basic.lean @@ -45,8 +45,6 @@ Newton’s law → zero acceleration → constant velocity → constant energy. ## iv. References -- Landau & Lifshitz, *Mechanics* -- Goldstein, *Classical Mechanics* -/ import Mathlib.Data.Real.Basic From d1413351cea602e25bd42fd1b6a3462e0223b72f Mon Sep 17 00:00:00 2001 From: Pranav-Magdum Date: Sat, 9 May 2026 20:12:46 +0530 Subject: [PATCH 05/14] used module system Removed redundant import statements and added TODO notes for documentation and proof. --- Physlib/ClassicalMechanics/FreeParticle/Basic.lean | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/Physlib/ClassicalMechanics/FreeParticle/Basic.lean b/Physlib/ClassicalMechanics/FreeParticle/Basic.lean index 840dac592..9c98228c5 100644 --- a/Physlib/ClassicalMechanics/FreeParticle/Basic.lean +++ b/Physlib/ClassicalMechanics/FreeParticle/Basic.lean @@ -3,6 +3,11 @@ Copyright (c) 2026 Pranav Magdum. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Pranav Magdum -/ +module + +public import Mathlib.Data.Real.Basic +public import Mathlib.Analysis.Calculus.Deriv.Basic +public import Physlib.Meta.TODO.Basic /-! # The Free Particle @@ -47,9 +52,7 @@ Newton’s law → zero acceleration → constant velocity → constant energy. -/ -import Mathlib.Data.Real.Basic -import Mathlib.Analysis.Calculus.Deriv.Basic -import Physlib.Meta.TODO.Basic + namespace ClassicalMechanics TODO "Make the documantation more descriptive" From e293688797c0aa98ca899dea0b726b43a721a18a Mon Sep 17 00:00:00 2001 From: Pranav-Magdum Date: Sat, 9 May 2026 20:25:25 +0530 Subject: [PATCH 06/14] Add time module import to Basic.lean Added import for time module in FreeParticle. --- Physlib/ClassicalMechanics/FreeParticle/Basic.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Physlib/ClassicalMechanics/FreeParticle/Basic.lean b/Physlib/ClassicalMechanics/FreeParticle/Basic.lean index 9c98228c5..aca2b682d 100644 --- a/Physlib/ClassicalMechanics/FreeParticle/Basic.lean +++ b/Physlib/ClassicalMechanics/FreeParticle/Basic.lean @@ -8,7 +8,7 @@ module public import Mathlib.Data.Real.Basic public import Mathlib.Analysis.Calculus.Deriv.Basic public import Physlib.Meta.TODO.Basic - +public import Physlib.SpaceAndTime.Time.Basic /-! # The Free Particle @@ -65,7 +65,6 @@ structure FreeParticle where namespace FreeParticle -abbrev Time := ℝ abbrev Trajectory := Time → ℝ noncomputable From c41ac7972a8ff648686f1050bc62de38ca27c3d1 Mon Sep 17 00:00:00 2001 From: Pranav-Magdum Date: Sat, 9 May 2026 20:28:42 +0530 Subject: [PATCH 07/14] Rename kinetic_energy to kineticEnergy and update theorem --- Physlib/ClassicalMechanics/FreeParticle/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Physlib/ClassicalMechanics/FreeParticle/Basic.lean b/Physlib/ClassicalMechanics/FreeParticle/Basic.lean index aca2b682d..8ce7bb475 100644 --- a/Physlib/ClassicalMechanics/FreeParticle/Basic.lean +++ b/Physlib/ClassicalMechanics/FreeParticle/Basic.lean @@ -72,7 +72,7 @@ def velocity (s : FreeParticle) (q : Trajectory) (t : Time) : ℝ := deriv q t noncomputable -def kinetic_energy (s : FreeParticle) (q : Trajectory) (t : Time) : ℝ := +def kineticEnergy (s : FreeParticle) (q : Trajectory) (t : Time) : ℝ := (1 / 2) * s.mass * (s.velocity q t)^2 def NewtonsSecondLaw (s : FreeParticle) (q : Trajectory) (t : Time) : Prop := @@ -99,7 +99,7 @@ lemma velocity_const_of_zero_acc sorry -- Step 3: Energy conservation -theorem Energy_is_Conserved +theorem kineticEnergy_conserved (s : FreeParticle) (q : Trajectory) (h : ∀ t, s.NewtonsSecondLaw q t) From 77fb62858405564ef657f00d653e380350a4186c Mon Sep 17 00:00:00 2001 From: Pranav-Magdum Date: Sat, 9 May 2026 20:42:25 +0530 Subject: [PATCH 08/14] Added Doc strings Added definitions and lemmas for a classical free particle, including velocity, kinetic energy, and Newton's second law. --- .../FreeParticle/Basic.lean | 67 +++++++++++++++++-- 1 file changed, 63 insertions(+), 4 deletions(-) diff --git a/Physlib/ClassicalMechanics/FreeParticle/Basic.lean b/Physlib/ClassicalMechanics/FreeParticle/Basic.lean index 8ce7bb475..076fab289 100644 --- a/Physlib/ClassicalMechanics/FreeParticle/Basic.lean +++ b/Physlib/ClassicalMechanics/FreeParticle/Basic.lean @@ -58,27 +58,66 @@ namespace ClassicalMechanics TODO "Make the documantation more descriptive" TODO "Prove momentum conservation" TODO "Prove the velocity_const_of_zero_acc lemma" +/-- +A classical free particle with positive mass. +A free particle is a mechanical system evolving in the absence of +external forces. The dynamics are therefore entirely determined by +Newton's second law with zero force. + +The only parameter of the system is the particle mass. The assumption +that the mass is strictly positive is physically natural and is used +throughout the development when simplifying the equation of motion. +-/ structure FreeParticle where mass : ℝ mass_pos : 0 < mass namespace FreeParticle - +/-- +A trajectory is a time-dependent position function describing the motion +of the particle in one spatial dimension. Defining the trajectory. +-/ abbrev Trajectory := Time → ℝ +/-- +The velocity of a trajectory at a given time. +This is defined as the time derivative of the position function. +-/ noncomputable def velocity (s : FreeParticle) (q : Trajectory) (t : Time) : ℝ := deriv q t +/-- +The kinetic energy of the free particle along a trajectory. + +This is given by the classical expression `E = (1 / 2) m v²`, +where `m` is the particle mass and `v` is the velocity. +-/ + noncomputable def kineticEnergy (s : FreeParticle) (q : Trajectory) (t : Time) : ℝ := (1 / 2) * s.mass * (s.velocity q t)^2 +/-- +Newton's second law for the free particle. + +Since no external forces act on the particle, Newton's second law +reduces to the equation `m q'' = 0`, expressing that the acceleration +vanishes identically. +-/ + def NewtonsSecondLaw (s : FreeParticle) (q : Trajectory) (t : Time) : Prop := s.mass * deriv (s.velocity q) t = 0 --- Step 1: get q'' = 0 +/-- +Newton's second law for a free particle implies that the acceleration +vanishes identically. + +Since the particle mass is strictly positive, the equation +`m q'' = 0` can be simplified to `q'' = 0` by cancelling the mass +factor. +-/ lemma accel_zero (s : FreeParticle) (q : Trajectory) @@ -89,7 +128,19 @@ lemma accel_zero have h1 := h t exact (mul_eq_zero.mp h1).resolve_left h₀ --- Step 2: velocity is constant +/-- +If the acceleration of a trajectory vanishes everywhere, then the +velocity is constant. + +More precisely, if the second derivative of the trajectory is zero +for all times, then there exists a constant `v₀` such that the +velocity is equal to `v₀` at every time. + +The continuity assumption on `deriv q` is included to apply standard +results from real analysis relating vanishing derivatives to constant +functions. +-/ + lemma velocity_const_of_zero_acc (q : ℝ → ℝ) (h : ∀ t, deriv (deriv q) t = 0) @@ -98,7 +149,15 @@ lemma velocity_const_of_zero_acc -- this is a standard analysis result (can be proved later) sorry --- Step 3: Energy conservation +/-- +A free particle satisfying the equation of motion conserves kinetic energy. + +The proof follows the standard argument from classical mechanics: +Newton's second law implies that the acceleration vanishes, which in +turn implies that the velocity is constant. Since the kinetic energy +depends only on the square of the velocity, it follows that the kinetic +energy is constant in time. +-/ theorem kineticEnergy_conserved (s : FreeParticle) (q : Trajectory) From 166aa24dba0b5647a21e6500d6fd21ae80892760 Mon Sep 17 00:00:00 2001 From: Pranav-Magdum Date: Sat, 9 May 2026 20:50:10 +0530 Subject: [PATCH 09/14] removed extra lines and added sorryful attribute --- Physlib/ClassicalMechanics/FreeParticle/Basic.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/Physlib/ClassicalMechanics/FreeParticle/Basic.lean b/Physlib/ClassicalMechanics/FreeParticle/Basic.lean index 076fab289..b583ed2d7 100644 --- a/Physlib/ClassicalMechanics/FreeParticle/Basic.lean +++ b/Physlib/ClassicalMechanics/FreeParticle/Basic.lean @@ -140,7 +140,7 @@ The continuity assumption on `deriv q` is included to apply standard results from real analysis relating vanishing derivatives to constant functions. -/ - +[@sorryful] lemma velocity_const_of_zero_acc (q : ℝ → ℝ) (h : ∀ t, deriv (deriv q) t = 0) @@ -168,10 +168,8 @@ theorem kineticEnergy_conserved -- get q'' = 0 have h_acc : ∀ t, deriv (deriv q) t = 0 := accel_zero s q h - -- get constant velocity rcases velocity_const_of_zero_acc q h_acc hcont with ⟨v₀, hv⟩ - -- energy is constant have h_ke : ∀ t, s.kinetic_energy q t = (1 / 2) * s.mass * v₀^2 := by intro t From 8278bd52b9521e2ce019c840e0fbd9006f350207 Mon Sep 17 00:00:00 2001 From: Pranav-Magdum Date: Sat, 9 May 2026 20:53:19 +0530 Subject: [PATCH 10/14] Refine TODO comments in Basic.lean Updated TODO comments to specify conservation of linear momentum. --- Physlib/ClassicalMechanics/FreeParticle/Basic.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Physlib/ClassicalMechanics/FreeParticle/Basic.lean b/Physlib/ClassicalMechanics/FreeParticle/Basic.lean index b583ed2d7..949a0c119 100644 --- a/Physlib/ClassicalMechanics/FreeParticle/Basic.lean +++ b/Physlib/ClassicalMechanics/FreeParticle/Basic.lean @@ -55,9 +55,9 @@ Newton’s law → zero acceleration → constant velocity → constant energy. namespace ClassicalMechanics -TODO "Make the documantation more descriptive" -TODO "Prove momentum conservation" -TODO "Prove the velocity_const_of_zero_acc lemma" + +TODO "Prove conservation of linear momentum for the free particle." + /-- A classical free particle with positive mass. From bfc2d88e18bd67cbbf563f2db368ecf8b4014e24 Mon Sep 17 00:00:00 2001 From: Pranav-Magdum Date: Sun, 10 May 2026 16:49:09 +0530 Subject: [PATCH 11/14] Update Physlib/ClassicalMechanics/FreeParticle/Basic.lean Co-authored-by: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> --- Physlib/ClassicalMechanics/FreeParticle/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Physlib/ClassicalMechanics/FreeParticle/Basic.lean b/Physlib/ClassicalMechanics/FreeParticle/Basic.lean index 949a0c119..3d0c1cf65 100644 --- a/Physlib/ClassicalMechanics/FreeParticle/Basic.lean +++ b/Physlib/ClassicalMechanics/FreeParticle/Basic.lean @@ -140,7 +140,7 @@ The continuity assumption on `deriv q` is included to apply standard results from real analysis relating vanishing derivatives to constant functions. -/ -[@sorryful] +@[sorryful] lemma velocity_const_of_zero_acc (q : ℝ → ℝ) (h : ∀ t, deriv (deriv q) t = 0) From 25e08749514da93993d5e9e256983c58d52377c1 Mon Sep 17 00:00:00 2001 From: Pranav-Magdum Date: Sun, 10 May 2026 21:27:30 +0530 Subject: [PATCH 12/14] doc string for mass parameter in FreeParticle structure Added documentation for the mass parameter in FreeParticle. --- Physlib/ClassicalMechanics/FreeParticle/Basic.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/Physlib/ClassicalMechanics/FreeParticle/Basic.lean b/Physlib/ClassicalMechanics/FreeParticle/Basic.lean index 3d0c1cf65..c0ae55c50 100644 --- a/Physlib/ClassicalMechanics/FreeParticle/Basic.lean +++ b/Physlib/ClassicalMechanics/FreeParticle/Basic.lean @@ -70,6 +70,13 @@ that the mass is strictly positive is physically natural and is used throughout the development when simplifying the equation of motion. -/ structure FreeParticle where +/-- +The mass of the free particle. + +This parameter determines the inertial response of the particle in +Newton's second law. +-/ + mass : ℝ mass_pos : 0 < mass From 86e3c47ad9d4f119a33f7659c390958c7eb31fdb Mon Sep 17 00:00:00 2001 From: Pranav-Magdum Date: Sun, 10 May 2026 21:32:31 +0530 Subject: [PATCH 13/14] added and removed lines --- Physlib/ClassicalMechanics/FreeParticle/Basic.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Physlib/ClassicalMechanics/FreeParticle/Basic.lean b/Physlib/ClassicalMechanics/FreeParticle/Basic.lean index c0ae55c50..15698a3ed 100644 --- a/Physlib/ClassicalMechanics/FreeParticle/Basic.lean +++ b/Physlib/ClassicalMechanics/FreeParticle/Basic.lean @@ -85,12 +85,14 @@ namespace FreeParticle A trajectory is a time-dependent position function describing the motion of the particle in one spatial dimension. Defining the trajectory. -/ + abbrev Trajectory := Time → ℝ + /-- The velocity of a trajectory at a given time. - This is defined as the time derivative of the position function. -/ + noncomputable def velocity (s : FreeParticle) (q : Trajectory) (t : Time) : ℝ := deriv q t @@ -113,7 +115,6 @@ Since no external forces act on the particle, Newton's second law reduces to the equation `m q'' = 0`, expressing that the acceleration vanishes identically. -/ - def NewtonsSecondLaw (s : FreeParticle) (q : Trajectory) (t : Time) : Prop := s.mass * deriv (s.velocity q) t = 0 From 2bedc6c13394113df740cdaa6e0d23dd42ccf434 Mon Sep 17 00:00:00 2001 From: Pranav-Magdum Date: Sun, 10 May 2026 21:37:47 +0530 Subject: [PATCH 14/14] reformatting --- Physlib/ClassicalMechanics/FreeParticle/Basic.lean | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/Physlib/ClassicalMechanics/FreeParticle/Basic.lean b/Physlib/ClassicalMechanics/FreeParticle/Basic.lean index 15698a3ed..e7334c918 100644 --- a/Physlib/ClassicalMechanics/FreeParticle/Basic.lean +++ b/Physlib/ClassicalMechanics/FreeParticle/Basic.lean @@ -76,23 +76,21 @@ The mass of the free particle. This parameter determines the inertial response of the particle in Newton's second law. -/ - mass : ℝ mass_pos : 0 < mass namespace FreeParticle + /-- A trajectory is a time-dependent position function describing the motion of the particle in one spatial dimension. Defining the trajectory. -/ - abbrev Trajectory := Time → ℝ /-- The velocity of a trajectory at a given time. This is defined as the time derivative of the position function. -/ - noncomputable def velocity (s : FreeParticle) (q : Trajectory) (t : Time) : ℝ := deriv q t @@ -103,7 +101,6 @@ The kinetic energy of the free particle along a trajectory. This is given by the classical expression `E = (1 / 2) m v²`, where `m` is the particle mass and `v` is the velocity. -/ - noncomputable def kineticEnergy (s : FreeParticle) (q : Trajectory) (t : Time) : ℝ := (1 / 2) * s.mass * (s.velocity q t)^2