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 18 commits into
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.
| 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.
Removed references to Landau & Lifshitz and Goldstein.
Removed redundant import statements and added TODO notes for documentation and proof.
Added import for time module in FreeParticle.
Added definitions and lemmas for a classical free particle, including velocity, kinetic energy, and Newton's second law.
Updated TODO comments to specify conservation of linear momentum.
Pranav-Magdum
left a comment
Pranav-Magdum
left a comment
There was a problem hiding this comment.
I have made the changes according to the comments
| reduces to the equation `m q'' = 0`, expressing that the acceleration | ||
| vanishes identically. | ||
| -/ | ||
|
|
Co-authored-by: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
Added documentation for the mass parameter in FreeParticle.
Pranav-Magdum
left a comment
Pranav-Magdum
left a comment
There was a problem hiding this comment.
made the suggested changes
|
@Pranav-Magdum Thanks for fixing my comments. The linters of this are still not passing, would you mind fixing the errors there. It is possible to run the linters locally (discussed here: https://github.com/leanprover-community/physlib/blob/master/scripts/README.md), but you can also rely on the GitHub workflows. |
| 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₀ |
There was a problem hiding this comment.
These proofs should only be indented by two spaces not four. Only the theorem statement (and definition types) should be indented by four, if that makes sense. I'm happy to make this change if you would like. This is an annoying 'style' thing, which just helps with the maintainability of the code.
There was a problem hiding this comment.
sure, if you can make the change.
|
@Pranav-Magdum I made some changes, I think this should pass the linters now - if it does, I will approve and merge. Many thanks for this PR! Hopefully this is the first of many :). |
jstoobysmith
added
the
ready-to-merge
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.