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 rename to velocity

[RaunakChhatwal]

Done, also renamed acc. Though I would like to keep pos abbreviated

[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]

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.