Physlib.ClassicalMechanics.PointParticle.NewtonianSystem.Basic

For any Newtonian system, its associated reference frame is an inertial frame.

The type of vectors in the vector space associated with the reference frame of the Newtonian system.

Given a Newtonian system $\mathcal{S}$, `Particle` is the type representing the individual point particles that belong to the system's collection of particles. Each particle $p$ of this type is associated with a mass $m \in \mathbb{R}^+$ and a position vector $\mathbf{r}$ in the system's reference frame.

The mass of a particle $p$ in a Newtonian system, represented as a positive real number $m \in \mathbb{R}_{>0}$.

Given a Newtonian system $\mathcal{S}$ and a particle $p$ belonging to it, the function returns the position vector $\mathbf{r}(t)$ of the particle $p$ at a given time $t$ within the system's associated vector space $V$.

For a particle $p$ belonging to a Newtonian system $\mathcal{S}$, its velocity at time $t$ is the vector $\mathbf{v}(t)$ in the system's associated vector space, defined as the time derivative of its position vector $\mathbf{r}(t)$: $$\mathbf{v}(t) = \frac{d\mathbf{r}}{dt}$$ This value corresponds to the velocity of the underlying particle in the system's inertial reference frame.

For a particle $p$ belonging to a Newtonian system $\mathcal{S}$, its acceleration at time $t$ is the vector $\mathbf{a}(t)$ in the system's associated vector space $V$. This is defined as the time derivative of the particle's velocity vector $\mathbf{v}(t)$: $$\mathbf{a}(t) = \frac{d\mathbf{v}}{dt} = \frac{d^2\mathbf{r}}{dt^2}$$ where $\mathbf{r}(t)$ is the position of the particle. This quantity represents the instantaneous acceleration of the particle within the system's inertial reference frame.

For a particle $p$ belonging to a Newtonian system, its momentum at time $t$ is the vector $\mathbf{p}(t)$ defined as the product of the particle's mass $m$ and its velocity $\mathbf{v}(t)$ at that time: $$\mathbf{p}(t) = m \mathbf{v}(t)$$ The resulting vector $\mathbf{p}(t)$ lies in the vector space associated with the system's reference frame.

For a particle $p$ in a Newtonian system $\mathcal{S}$, its kinetic energy at time $t$ is the real number defined by the formula: $$K(t) = \frac{1}{2} m \|\mathbf{v}(t)\|^2$$ where $m$ is the particle's mass and $\mathbf{v}(t)$ is the magnitude of its velocity vector at time $t$ in the system's reference frame.

In a Newtonian point-particle system, the type of all forces is defined as the disjoint union (sum type) of the system's internal forces and its external forces.

In a Newtonian system $\mathcal{S}$, the type of forces $\text{Force}$ is the disjoint union of internal forces and external forces. The function `inner` maps a force $f \in \text{Force}$ to its underlying representation as a force acting on particles within the system's reference frame. It extracts the specific force data regardless of whether $f$ is categorized as an internal or external force.

In a Newtonian point-particle system $\mathcal{S}$, this definition provides an automatic conversion (coercion) from the type of system forces $\text{Force}$ (the disjoint union of internal and external forces) to the underlying force representation $\text{Force}(\text{Particle})$ defined in the system's reference frame. This conversion is performed by the function `inner`, which extracts the physical force data regardless of whether the force is internal or external.

For a given force $f$ in a Newtonian system $\mathcal{S}$, this function returns the vector value of the force at a specific time $t \in \text{Time}$, denoted as $\mathbf{F}_f(t)$, within the vector space $V$ associated with the system's reference frame.

In a Newtonian system $\mathcal{S}$, this definition allows a force $f \in \text{Force}$ to be treated as a function of time. Specifically, it enables the notation $f(t)$ to represent the vector value of the force $\mathbf{F}_f(t)$ at time $t \in \text{Time}$ within the system's vector space $V$.

For a given force $f$ in a Newtonian system $\mathcal{S}$, its target is the particle $p \in \text{Particle}$ upon which the force acts.

In a Newtonian point-particle system, where the type of all forces is defined as the disjoint union of internal and external forces ($F = F_{\text{int}} \oplus F_{\text{ext}}$), this predicate determines whether a given force $f \in F$ is an internal force. Specifically, it returns true if $f$ belongs to the summand $F_{\text{int}}$.

Given a force $f$ in a Newtonian system, where the type of all forces is defined as the disjoint union (sum type) $\text{InternalForces} \oplus \text{ExternalForces}$, the property `External` holds if $f$ belongs to the right-hand component of the sum, identifying it as an external force.

The type representing the set of internal forces acting within a Newtonian system of point particles. Each element of this type corresponds to a specific force categorized as internal to the system.

In a Newtonian system, there is a natural inclusion that allows an internal force $f \in \text{InternalForce}$ to be treated as a general force $F \in \text{Force}$. Since the set of all forces $\text{Force}$ is defined as the disjoint union of internal and external forces ($\text{InternalForce} \oplus \text{ExternalForce}$), this mapping identifies an internal force as the corresponding element in the total set of forces.

For a given internal force $f$ in a Newtonian system, this function returns the force vector $\mathbf{f}(t)$ at time $t$. The result is an element of the vector space associated with the system's reference frame.

For a given internal force $f$ within a Newtonian system, its target is the specific particle $p$ belonging to the system upon which the force $f$ acts.

For an internal force $f$ in a Newtonian system $\mathcal{S}$, the function $f.\text{source}$ returns the particle $p \in \mathcal{S}$ that exerts the force.

In a Newtonian system of point particles, for any internal force $f$, the multiplicity (the number of occurrences) of $f$ in the multiset of internal forces is equal to the multiplicity of its reverse force $f_{\text{rev}}$.

For an internal force $f$ in a Newtonian system, the function `reverse` returns the corresponding reaction force $f_{\text{rev}}$. This force is characterized by having the source and target particles of $f$ swapped and a force vector that is the additive inverse $-\mathbf{f}(t)$ of the original force vector at any time $t$, consistent with Newton's Third Law.

An internal force $\mathbf{f}$ is central if, at any time $t$, the force vector $\mathbf{f}(t)$ is collinear with the line joining the source particle and the target particle. Specifically, there exists a scalar $c \in \mathbb{R}$ such that: $$\mathbf{f}(t) = c \cdot (\mathbf{r}_{\text{target}}(t) - \mathbf{r}_{\text{source}}(t))$$ where $\mathbf{r}_{\text{target}}(t)$ and $\mathbf{r}_{\text{source}}(t)$ are the position vectors of the target and source particles at time $t$, respectively.

For a given Newtonian system $\mathcal{S}$, the total mass $M$ is the sum of the masses $m_p$ of all particles $p$ contained within the system: $$M = \sum_{p \in \text{particles}} m_p$$ where each $m_p \in \mathbb{R}_{>0}$ is the individual mass of particle $p$.

For a given Newtonian system $\mathcal{S}$ at a time $t$, the total momentum $\mathbf{P}(t)$ is the vector sum of the individual momenta $\mathbf{p}_p(t)$ of all particles $p$ belonging to the system: $$\mathbf{P}(t) = \sum_{p \in \text{Particles}} \mathbf{p}_p(t)$$ where $\mathbf{p}_p(t) = m_p \mathbf{v}_p(t)$ is the momentum of particle $p$ at time $t$ in the system's reference frame.

For a Newtonian system $\mathcal{S}$ and a time $t$, the net external force $\mathbf{F}_{\text{ext}}(t)$ is the vector sum of all external forces acting within the system at that time: $$\mathbf{F}_{\text{ext}}(t) = \sum_{f \in \text{ExternalForces}} \mathbf{F}_f(t)$$ where $\text{ExternalForces}$ is the multiset of forces in the system satisfying the property of being external, and $\mathbf{F}_f(t)$ is the vector value of the force $f$ at time $t$ in the system's reference frame.

For a Newtonian system $\mathcal{S}$, the total kinetic energy $K(t)$ at time $t$ is the sum of the kinetic energies of all particles $p$ belonging to the system: $$K(t) = \sum_{p \in \mathcal{S}} K_p(t)$$ where $K_p(t) = \frac{1}{2} m_p \|\mathbf{v}_p(t)\|^2$ is the kinetic energy of particle $p$ with mass $m_p$ and velocity $\mathbf{v}_p(t)$ at time $t$.