/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/modulepublicimportPhyslib.SpaceAndTime.Space.ModulepublicimportPhyslib.Meta.Informal.BasicpublicimportMathlib.Geometry.Manifold.Algebra.SmoothFunctions
Rigid bodies
A rigid body is one where the distance and relative orientation between particles does not change.
In other words, the body remains undeformed.
In this module we will define the basic properties of a rigid body, including
mass
center of mass
inertia tensor
References
Landau and Lifshitz, Mechanics, page 100, Section 32
@[expose]publicsectionTODO"The definition of a rigid body is currently defined via linear maps
from the space of smooth functions to ℝ. When possible, it should be change
to *continuous* linear maps. "
lemmainertiaTensor_symmetric{d:ℕ}(R:RigidBodyd)(ij:Find):R.inertiaTensorij=R.inertiaTensorji:=d:ℕR:RigidBodydi:Findj:Find⊢ R.inertiaTensorij=R.inertiaTensorjiAll goals completed! 🐙TODO"Move `cmap` and `cmap_apply` to a more general location, such as a file in
`SpaceAndTime/Space/` or `Mathematics/`. Alternatively, define a version of `ρ` taking an
unbundled `(f : Space d → ℝ) (hf : ContDiff ℝ ⊤ f)` in place of a `ContMDiffMap`."
Bundle a smooth real-valued function on Space d as an element of the space of test
functions. Keeping this as a named constructor ensures the resulting type head stays
ContMDiffMap, so the module/ring operations and comp resolve correctly.
One can describe the motion of rigid body with a fixed (inertial) coordinate system (X,Y,Z)
and a moving system (x₁,x₂,x₃) rigidly attached to the body.
A rigid body in three-dimensional space has six degrees of freedom:
three translational (for the position of its centre of mass) and three
rotational (for its orientation).
The velocity v of any point in a rigid body is
v = V + Ω × r,
where V is the velocity of the origin of the moving system and Ω is the angular velocity.
The motion of a rigid body can be decomposed into a translation of some reference point plus a
rotation about that point. There exists a time-dependent vector V(t) and angular velocity ω(t)
such that v(r) = V + ω × r, where r is measured from the reference point.
The centre of mass of a rigid body moves as if all mass were concentrated at that
point and acted upon by the resultant external force: M a_CM = ∑ F_ext.
The total angular momentum about a point O is L = ∫ r × v dm. With v = V + ω × r about the
centre of mass, L = R × (M V) + I_CM ω, where R is the centre of mass position.
In the inertial frame, the translational equation of motion of a rigid body is given by
dP/dt = F, where P is the total linear momentum and F is the total external force acting
on the body.
In the inertial frame, the rotational equation of motion of a rigid body about the center of
mass is given by dM/dt = K, where M is the total angular momentum and K is the total
external torque.
The kinetic energy decomposes into translational and rotational parts:
T = (1/2) M |V|² + (1/2) ω ⋅ I_CM ω.
Here V is the velocity of the centre of mass and I_CM is the inertia tensor about that point.
If I_O is the inertia tensor about a point O, then the inertia tensor about a parallel point O'
displaced by a is I_{O'} = I_O + M(|a|² 1 − a ⊗ a). This is the parallel-axis theorem.
Because the inertia tensor is real symmetric, there exists an orthonormal basis of principal
axes in which it is diagonal. The corresponding directions are the principal axes of inertia.
A rotating body-fixed frame is a coordinate system attached to the body
that rotates with the body relative to an inertial (fixed) frame. The frame
is characterised by its angular velocity vector Ω(t).
The time derivative in the rotating frame, d'/dt, is the derivative
of the components of a vector with respect to time when expressed in the
rotating (body-fixed) frame.
For any vector field A(t), its inertial-frame time derivative equals the rotating-frame
derivative plus the contribution from the frame rotation:
(dA/dt)_inertial = (dA/dt)_rotating + Ω × A.
Here Ω is the angular velocity of the rotating frame.
For linear momentum, the relation between inertial and rotating derivatives is
(dP/dt)_inertial = d'P/dt + Ω × P.
So, d'P/dt + Ω × P = F which is the linear-momentum equation in the rotating frame.
For angular momentum, the relation between inertial and rotating derivatives is
(dM/dt)_inertial = d'M/dt + Ω × M,
and with the rotational form of Newton's law M_tot = (dM/dt)_inertial this yields
d'M/dt + Ω × M = K,
the angular-momentum equation in the rotating frame.
When motion is described in body-fixed principal axes (I₁, I₂, I₃ diagonal), the equations of
rotational motion (Euler’s equations) are:
I₁ dω₁/dt + (I₃ − I₂) ω₂ ω₃ = M₁, with cyclic permutations.
M is the external torque about the centre of mass.
A rigid body can perform steady (uniform) rotation about any principal axis if the torque about
that axis vanishes. Stability depends on the ordering of principal moments.
Rotations about the largest and smallest principal axes are stable under small perturbations;
rotation about the intermediate axis is unstable (tennis-racket effect).
If a rigid body is confined to planar motion, its dynamics reduce to a two-dimensional problem:
the inertia reduces to a scalar moment and rotation is described
by a single angular velocity.
The power delivered to a rigid body by forces is P = ∑ Fᵢ ⋅ vᵢ = F_tot ⋅ V + M ⋅ ω, where F_tot
is total force, V the reference point velocity, and M the torque. Translational and rotational
contributions separate.
Small oscillations about a stable equilibrium orientation are governed by linearised equations
obtained by expanding energy to second order in angular displacements. Normal modes and
frequencies depend on inertia and restoring torques.