feat(ClassicalMechanics): Newtonian point-particle systems

[RaunakChhatwal]

Summary

This PR introduces basic definitions for forces and Newtonian point-particle systems in classical mechanics.

Forces

Adds Force, representing a time-dependent force acting on an object, together with:

• InternalForce, which additionally records the source of a force
• InternalForce.reverse, representing the equal-and-opposite force with source and target exchanged
• netForce, which sums the internal and external forces acting on a given object

Point particles

Adds Particle, consisting of:

• positive mass
• a trajectory relative to a reference frame
• twice-differentiability of the trajectory in inertial frames

and defines the associated:

• velocity
• acceleration
• position in affine absolute space

Particles and forces are indexed by the reference frame in which they are described. This makes the frame dependence explicit in the types and prevents accidentally combining positions, velocities, accelerations, or forces expressed in different frames.

Point-particle systems

Adds PointParticle.System, representing a finite collection of particles in an inertial reference frame, together with internal and external forces.

Newton's laws are encoded as properties of a system:

• Newton's second law: the net force on each particle equals its mass times its acceleration
• Newton's third law: internal forces come in equal-and-opposite pairs

The PR also introduces convenient system-level definitions for:

• particle mass, position, velocity, acceleration, momentum, and kinetic energy
• internal/external system forces
• reverse and central internal forces
• total mass
• total momentum
• net external force
• total kinetic energy

Finally, the new Force and PointParticle.Defs modules are exported from Physlib.lean.

[github-actions]

Thank you for this pull-request (PR). If this is your first PR, welcome to the community!

Below is what will happen next. Please read carefully if you are not familiar with the process. You may open other PRs while this one is being reviewed, and can stack PRs on top of each other, so don't let these steps slow you down.

1. Some automated checks will be run on your PR. You can see the results of these checks at the buttom of your PR page. If any of these checks fail, you will need to fix the issues before your PR can be merged. You can learn more about these here, including how to run them locally, which is sometimes quicker than relying on the GitHub Actions. If you have never had a PR merged before, you may have to wait for a reviewer to manually start these checks (this is for security).

2. A reviewer will look at your PR and may ask you to make changes. This may happen a couple of days after you submit your PR, so you may need to be patient. But it should not be longer than that - if it is please bring it to the attention of the community on the Zulip. The level of review will depend on where your PR is submitted. If it is submitted to ./Physlib or ./QuantumInfo, the review will be more thorough than if it is submitted to ./PhyslibAlpha. You can find out more about what the review process is looking for in our review guidelines. If a reviewer adds an awaiting-author label to your PR, address the review comments, then please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

3. The reviewer will either approve your PR, or request more changes (in which case we return to step 2). Once your PR is approved, it will be merged by a maintainer, this should happen shortly after approval, though you may get more comments at this stage.

Tip: The easiest way to get have a fast review is to submit a PR that is small and self-contained, and has clear documentation explaining why things are the way they are in your chages.

If you have any problems or questions, please reach out to the community on the Zulip.

[jstoobysmith]

Gave some high level comments to start. I think you should look at the other classical mechanics files to see how they have been done.

[jstoobysmith]

We should check, but I think we might already have PosReals defined somewhere

[RaunakChhatwal]

I don't think there is one. For instance, Positive/Ring.lean uses {x : R // 0 < x} directly. I did narrow the SMul instance for R+ to frame.Vector to minimize redundancy.

[jstoobysmith]

Would copy the structure of QuantumHarmonicOscillator here. Let Particle contain only the mass (definning the system). Then define ConfigurationSpace for the particles position. Then trajectories are maps from Time to ConfigurationSpace.

[RaunakChhatwal]

Particle is supposed to represent the properties (i.e. mass and position over time) of an actual particle. It is not a dynamical system by itself, and especially not the unconstrained one-particle lagrangian system. It's meant to constitute Newtonian particle systems in NewtonianSystem/Defs.lean, and I don't think configuration spaces should be involved in a foundation for newtonian mechanics

[jstoobysmith]

But you have included the trajectory in it, which is a specification of the kinematics of a particle. Would maybe rename this to ParticleKinematics in this case.

[RaunakChhatwal]

A particle's motion is just one property, there's also mass (and maybe charge in the future). Also, lean in general allows one to hypothetically consider different values of a variable. Like different hypothetical trajectories for the same particle variable

[jstoobysmith]

Would rename this ManyPointParticles or similar, and give it its own directory.

[RaunakChhatwal]

I would not include "PointParticle" in the name, since that is already the namespace. PointParticle.System should therefore be read as "point-particle system". I moved it to PointParticle/NewtonianSystem/Defs.lean, which is a subfolder of PointParticle because this formalization only applies to point particles and not rigid bodies, continuums, etc.

[RaunakChhatwal]

I think you should look at the other classical mechanics files to see how they have been done.

I mostly see disjoint examples in ClassicalMechanics and not many composable APIs. This PR introduces core data types like particles, forces, and newtonian systems. This will enable models and constraints to be expressed in terms of particles and forces (like in Pendulum/Defs.lean and Pendulum.lean), rather than having to start from a lagrangian derived in comments.

-awaiting-author

[jstoobysmith]

Sorry, have been a bit busy. Have reached out to others to see if they can review this. But it will likely be Monday before I can return to this. General comment: I think we could expand some of the module doc-string to include the justification behind the definitions in those files.

[RaunakChhatwal]

Thank you for taking the time to review, and I apologize for the terse docs. I've expanded the module docstrings to explain my motivations behind the definitions, including why particles include their positions over time. I hope this makes the intended data types clearer and gives us a better basis for discussing the design.

[jstoobysmith]

Some more comments

[jstoobysmith]

I would not define particle : system.Particle or any of the results which follow this. Instead you have all of these defined for a general frame.Particle, and they should all follow from that. Similar with force below.

[RaunakChhatwal]

The system level data types are an alias for the system's multisets, not the top level data types. The top level particles and forces don't identify corresponding elements of multisets, because different multiset elements may have the same underlying value. My intent is for downstream to work mostly with the multiset elements directly through the convenient aliases. Also, elements of multisets don't get the methods of the underlying type, they're accessible only through an inelegant .1 (like here).

[jstoobysmith]

But you have included the trajectory in it, which is a specification of the kinematics of a particle. Would maybe rename this to ParticleKinematics in this case.

[jstoobysmith]

Does ReferenceFrame contain a notion of time dimension (a basis on Time)? If not, I think it needs to if you want to define a force as an element of frame.Vector. More generally it would be nice to get all of this to work with the dimensions and units in PHyslib.

[RaunakChhatwal]

Time/Basic.lean

In this module we define the type Time, corresponding to time in a given (but arbitrary) set of units, with a given (but arbitrary) choice of origin (time zero)

ReferenceFrame contains neither origin nor basis in time because time coordinates are relative to that global arbitrary unit and origin. Even if we removed the global unit and origin, reference frames should only contain time origin because galilean frame transformations do not change the basis in time. Time coordinates then would need to be dimensionful.

Regarding the adoption of dimensions and units, my first step would be to refactor space as an arbitrary coordinate-free affine space over the displacement vector quantity and time as an arbitrary affine space over the time scalar quantity (used as 1d vector space).

An example from a prototype:

lemma affine_space_exists (V : Type) [AddGroup V] :
    ∃ P : Type, Nonempty (AffineSpace V P) :=
  ⟨V, ⟨inferInstance⟩⟩

def Space (dim : ℕ) : Type :=
  Classical.choose (affine_space_exists (Displacement dim))

instance {dim : ℕ} : AffineSpace (Displacement dim) (Space dim) :=
  Classical.choice (affine_space_exists (Displacement dim)).choose_spec

def Time : Type :=
  Classical.choose (affine_space_exists Duration)

instance : AffineSpace Duration Time :=
  Classical.choice (affine_space_exists Duration).choose_spec

Regardless, I think fundamental issues with the present design of dimensions/units should be discussed on zulip before undertaking adoption.

[jstoobysmith]

Ok, but then I think we should make it clear that here we are using that global origin and dimension on Time, meaning that value t is the value of the force in these units.

[RaunakChhatwal]

Force is just one vector function of time, among many others (like pos, velocity, momentum, etc). I clarified in ReferenceFrame.lean

[jstoobysmith]

awaiting-author

[RaunakChhatwal]

-awaiting-author

[jstoobysmith]

Move to near definition of frame.Vector

[jstoobysmith]

Would collapse the lines here, so that the arguments appear on one line

[jstoobysmith]

awaiting-author

[RaunakChhatwal]

-awaiting-author

[jstoobysmith]

Approved. Many thanks for the iterations. Will merge shortly.