Imports
/-
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 Physlib.SpaceAndTime.Time.Derivatives
public import Mathlib.Analysis.Calculus.MeanValueThe 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.
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.
linearMomentum_conserved shows that linear momentum stays constant over time.
kineticEnergy_conserved shows that kinetic energy stays constant over time.
So overall, we formalise the usual chain: Newton’s law → zero acceleration → constant velocity → constant momentum and 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. Momentum
D.1. Linear momentum
D.2. Momentum conservation
E. Energy
E.1. Kinetic energy
E.2. Energy conservation
iv. References
@[expose] public sectionA 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.
The mass of the free particle.
This parameter determines the inertial response of the particle in Newton's second law.
structure FreeParticle where mass : ℝ
mass_pos : 0 < massA 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.
set_option linter.unusedVariables false in@[nolint unusedArguments]
noncomputable
def velocity (s : FreeParticle) (q : Trajectory) (t : Time) : ℝ :=
deriv q tNewton'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 = 0Newton'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) (h : ∀ t, s.NewtonsSecondLaw q t) :
∀ t, deriv (deriv q) t = 0 :=
fun t => (mul_eq_zero.mp (h t)).resolve_left s.mass_pos.ne'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 second-order differentiability assumption is included to apply standard results from real analysis relating vanishing derivatives to constant functions.
All goals completed! 🐙If a free-particle trajectory has constant velocity, then its linear momentum is constant.
lemma linearMomentum_conserved_of_velocity_const (s : FreeParticle) (q : Trajectory)
(h : ∃ v₀, ∀ t, s.velocity q t = v₀) :
∃ p, ∀ t, s.linearMomentum q t = p := s:FreeParticleq:Trajectoryh:∃ v₀, ∀ (t : Time), s.velocity q t = v₀⊢ ∃ p, ∀ (t : Time), s.linearMomentum q t = p
s:FreeParticleq:Trajectoryv₀:ℝhv:∀ (t : Time), s.velocity q t = v₀⊢ ∃ p, ∀ (t : Time), s.linearMomentum q t = p
exact ⟨s.mass * v₀, fun t => s:FreeParticleq:Trajectoryv₀:ℝhv:∀ (t : Time), s.velocity q t = v₀t:Time⊢ s.linearMomentum q t = s.mass * v₀ All goals completed! 🐙⟩A free particle satisfying the equation of motion conserves linear momentum.
Newton's second law implies that the acceleration vanishes, so the velocity is constant. Since the particle mass is fixed, the linear momentum is constant in time.
theorem linearMomentum_conserved (s : FreeParticle) (q : Trajectory)
(h : ∀ t, s.NewtonsSecondLaw q t) (hcont : ContDiff ℝ 2 q) :
∃ p, ∀ t, s.linearMomentum q t = p :=
linearMomentum_conserved_of_velocity_const s q
(velocity_const_of_zero_acc q (accel_zero s q h) hcont)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)
(h : ∀ t, s.NewtonsSecondLaw q t) (hcont : ContDiff ℝ 2 q) :
∃ E, ∀ t, s.kineticEnergy q t = E := s:FreeParticleq:Trajectoryh:∀ (t : Time), s.NewtonsSecondLaw q thcont:ContDiff ℝ 2 q⊢ ∃ E, ∀ (t : Time), s.kineticEnergy q t = E
s:FreeParticleq:Trajectoryh:∀ (t : Time), s.NewtonsSecondLaw q thcont:ContDiff ℝ 2 qv₀:ℝhv:∀ (t : Time), ∂ₜ q t = v₀⊢ ∃ E, ∀ (t : Time), s.kineticEnergy q t = E
s:FreeParticleq:Trajectoryh:∀ (t : Time), s.NewtonsSecondLaw q thcont:ContDiff ℝ 2 qv₀:ℝhv:∀ (t : Time), ∂ₜ q t = v₀t:Time⊢ s.kineticEnergy q t = 1 / 2 * s.mass * v₀ ^ 2
All goals completed! 🐙