Add basic formalisation of the free particle in classical mechanics#1081
Add basic formalisation of the free particle in classical mechanics#1081Pranav-Magdum wants to merge 3 commits intoleanprover-community:masterfrom
Conversation
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.
| @@ -0,0 +1,125 @@ | |||
| /- | |||
| Copyright (c) 2025 Pranav Magdum. All rights reserved. | |||
| - Goldstein, *Classical Mechanics* | ||
|
|
||
| -/ | ||
| import Mathlib.Data.Real.Basic |
There was a problem hiding this comment.
Should go before the doc-string. Also we are now using the module system (see another Physlib file as an example of how to import within the module system).
|
|
||
| TODO "Make the documantation more descriptive" | ||
| TODO "Prove momentum conservation" | ||
| TODO "Prove the velocity_const_of_zero_acc lemma" |
There was a problem hiding this comment.
Could make these more descriptive.
| deriv q t | ||
|
|
||
| noncomputable | ||
| def kinetic_energy (s : FreeParticle) (q : Trajectory) (t : Time) : ℝ := |
There was a problem hiding this comment.
kineticEnergy (no underscores in names of definitions)
|
|
||
| namespace FreeParticle | ||
|
|
||
| abbrev Time := ℝ |
There was a problem hiding this comment.
I would get this from SpaceTime.Time.Basic rather than defining it again.
| exact (mul_eq_zero.mp h1).resolve_left h₀ | ||
|
|
||
| -- Step 2: velocity is constant | ||
| lemma velocity_const_of_zero_acc |
There was a problem hiding this comment.
Since this is not yet proved it will need the @[sorryful] attribute. May need an import to get this to work.
| sorry | ||
|
|
||
| -- Step 3: Energy conservation | ||
| theorem Energy_is_Conserved |
There was a problem hiding this comment.
kineticEnergy_conserved would be a better name I think.
|
|
||
| -- get constant velocity | ||
| rcases velocity_const_of_zero_acc q h_acc hcont with ⟨v₀, hv⟩ | ||
|
|
There was a problem hiding this comment.
Could we remove these new lines in the proof?
| ## iv. References | ||
|
|
||
| - Landau & Lifshitz, *Mechanics* | ||
| - Goldstein, *Classical Mechanics* |
There was a problem hiding this comment.
Could we either 1) remove these references, or 2) Add specific page numbers.
|
|
||
| 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. |
There was a problem hiding this comment.
would remove the but that's overkill here.
Updated copyright year from 2025 to 2026 and modified text for clarity.
2 participants
This PR adds a simple formalisation of the free particle: a particle of mass m with no external forces acting on it.
The goal is to capture the standard first-step reasoning from classical mechanics in Lean. Starting from Newton’s second law (m * q'' = 0), we show:
acceleration is zero,
velocity is constant,
kinetic energy is conserved.
The development is intentionally minimal and 1-dimensional (ℝ → ℝ) to keep things easy to follow. The harder analysis step (showing zero acceleration implies constant velocity) is currently isolated in a lemma, so the overall structure is clear and can be extended later.