Physlib.ClassicalMechanics.FreeParticle.Basic

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.

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

10 declarations

abbrev

Trajectory $q(t)$ of a particle

#Trajectory

A trajectory $q$ is a function $q: \text{Time} \to \mathbb{R}$ that maps a time $t$ to the position of a particle in one spatial dimension.

definition

Velocity $v(t) = \dot{q}(t)$ of a trajectory

#velocity

For a free particle $s$ and its trajectory $q: \text{Time} \to \mathbb{R}$ , the velocity at time $t$ is defined as the time derivative of the position function $q$ at that time, denoted by $\dot{q}(t)$ or $\frac{dq}{dt}(t)$ .

definition

Linear momentum $p(t) = m v(t)$ of a free particle

#linearMomentum

For a free particle $s$ with mass $m$ and a trajectory $q: \text{Time} \to \mathbb{R}$ , the linear momentum $p(t)$ at time $t$ is defined as the product of the particle's mass $m$ and its velocity $v(t) = \dot{q}(t)$ : $p(t) = m \cdot v(t)$

definition

Kinetic energy $E = \frac{1}{2} m v^2$ of a free particle

#kineticEnergy

For a free particle $s$ with mass $m$ and a trajectory $q: \text{Time} \to \mathbb{R}$ , the kinetic energy at time $t$ is defined as $E = \frac{1}{2} m v(t)^2$ , where $v(t) = \dot{q}(t)$ is the velocity of the particle at that time.

definition

Newton's second law for a free particle $m \ddot{q}(t) = 0$

#NewtonsSecondLaw

Given a free particle $s$ with mass $m$ , a trajectory $q: \text{Time} \to \mathbb{R}$ , and a specific time $t$ , Newton's second law for the free particle is the proposition that the product of the mass and the second time derivative of the trajectory at $t$ is zero, expressed as $m \cdot \ddot{q}(t) = 0$ .

theorem

Newton's Second Law Implies Zero Acceleration for a Free Particle

#accel_zero

Given a free particle $s$ with mass $m$ and a trajectory $q: \text{Time} \to \mathbb{R}$ , if Newton's second law holds for all time $t$ (i.e., $m \cdot \ddot{q}(t) = 0$ for all $t$ ), then the acceleration of the particle is zero for all time $t$ , such that $\ddot{q}(t) = 0$ .

theorem

Zero Acceleration Implies Constant Velocity

#velocity_const_of_zero_acc

For any twice continuously differentiable trajectory $q : \text{Time} \to \mathbb{R}$ , if the second derivative $\frac{d^2q}{dt^2}(t) = 0$ for all $t \in \text{Time}$ , then there exists a constant $v_0 \in \mathbb{R}$ such that the velocity $\frac{dq}{dt}(t) = v_0$ for all $t \in \text{Time}$ .

theorem

Constant velocity implies constant linear momentum

#linearMomentum_conserved_of_velocity_const

For a free particle $s$ with mass $m$ and a trajectory $q: \text{Time} \to \mathbb{R}$ , if there exists a constant $v_0$ such that the velocity $v(t) = \dot{q}(t) = v_0$ for all $t$ , then there exists a constant $p$ such that the linear momentum $p(t) = m \cdot v(t) = p$ for all $t$ .

theorem

Conservation of Linear Momentum for a Free Particle

#linearMomentum_conserved

Consider a free particle $s$ with mass $m$ and a trajectory $q: \text{Time} \to \mathbb{R}$ that is twice continuously differentiable ( $C^2$ ). If the particle satisfies Newton's second law $m \ddot{q}(t) = 0$ for all times $t \in \text{Time}$ , then its linear momentum $p(t) = m \dot{q}(t)$ is conserved. That is, there exists a constant value $p \in \mathbb{R}$ such that $p(t) = p$ for all $t$ .

theorem

Newton's Second Law implies Kinetic Energy Conservation for a Free Particle

#kineticEnergy_conserved

Consider a free particle $s$ with mass $m$ and a trajectory $q: \text{Time} \to \mathbb{R}$ that is twice continuously differentiable ( $C^2$ ). If $q$ satisfies Newton's second law for all times $t$ , such that $m \ddot{q}(t) = 0$ , then there exists a constant value $E$ such that for all $t$ , the kinetic energy of the particle, $K(t) = \frac{1}{2} m \dot{q}(t)^2$ , is equal to $E$ .

Physlib.ClassicalMechanics.FreeParticle.Basic

The Free Particle

i. Overview

ii. Key results

iii. Table of contents

iv. References

Trajectory q(t)q(t)q(t) of a particle

Velocity v(t)=q˙(t)v(t) = \dot{q}(t)v(t)=q˙​(t) of a trajectory

Linear momentum p(t)=mv(t)p(t) = m v(t)p(t)=mv(t) of a free particle

Kinetic energy E=12mv2E = \frac{1}{2} m v^2E=21​mv2 of a free particle

Newton's second law for a free particle mq¨(t)=0m \ddot{q}(t) = 0mq¨​(t)=0

Newton's Second Law Implies Zero Acceleration for a Free Particle

Zero Acceleration Implies Constant Velocity

Constant velocity implies constant linear momentum

Conservation of Linear Momentum for a Free Particle

Newton's Second Law implies Kinetic Energy Conservation for a Free Particle

Trajectory $q(t)$ of a particle

Velocity $v(t) = \dot{q}(t)$ of a trajectory

Linear momentum $p(t) = m v(t)$ of a free particle

Kinetic energy $E = \frac{1}{2} m v^2$ of a free particle

Newton's second law for a free particle $m \ddot{q}(t) = 0$