Classical Mechanics Rigid Body Informal Lemmas

Stream: PhysLean

[Afiq Hatta]

Hey @Joseph Tooby-Smith I started working on informal lemmas for the rigid body in classical mechanics.

this is really rough - i will be breaking the lemmas down even more. But the main feedback i wanted to ask for is if you thought it was okay to follow landau's approach to proving the rigid body results in his first volume

informal_lemma motion_of_particle_in_rigid_body where
  tag := "LL32-MP"
  deps := [``RigidBody]
  statement :=
  "The angular velocity of rotation of a rigid body from a system of coordinates fixed in the body is independent of the system chosen."

informal_lemma angular_velocity_is_well_defined where
  tag := "LL32-AM"
  deps := [``RigidBody]
  statement :=
  "The angular velocity of rotation of a rigid body from a system of coordinates fixed in the body is independent of the system chosen."

informal_lemma decomposition_of_motion where
  tag := "LL32-DM"
  deps := [``RigidBody]
  statement :=
  "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."

informal_lemma center_of_mass_point_moves_as_particle where
  tag := "LL32-CM"
  deps := [``RigidBody]
  statement :=
  "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."

informal_lemma angular_momentum_about_point where
  tag := "LL32-L"
  deps := [``RigidBody]
  statement :=
  "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."

informal_lemma kinetic_energy_decomposition where
  tag := "LL32-TK"
  deps := [``RigidBody]
  statement :=
  "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."

informal_lemma parallel_axis_theorem where
  tag := "LL32-PA"
  deps := [``RigidBody]
  statement :=
  "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."

informal_lemma inertia_tensor_positive_semidefinite where
  tag := "LL32-IPS"
  deps := [``RigidBody]
  statement :=
  "The inertia tensor is symmetric and positive semi-definite: for any vector u, u ⋅ (I u) ≥ 0, with equality only if all mass lies on a line or point."

informal_lemma principal_axes_exist where
  tag := "LL32-PAE"
  deps := [``RigidBody]
  statement :=
  "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."

informal_lemma euler_equations where
  tag := "LL32-EQ"
  deps := [``RigidBody]
  statement :=
  "When motion is described in body-fixed principal axes (I_1, I_2, I_3 diagonal), the equations of rotational motion (Euler’s equations) are: I_1 dω_1/dt + (I_3 − I_2) ω_2 ω_3 = M_1, with cyclic permutations. M is the external torque about the centre of mass."

informal_lemma steady_rotation_conditions where
  tag := "LL32-SR"
  deps := [``RigidBody]
  statement :=
  "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."

informal_lemma intermediate_axis_instability where
  tag := "LL32-IAI"
  deps := [``RigidBody]
  statement :=
  "Rotations about the largest and smallest principal axes are stable under small perturbations; rotation about the intermediate axis is unstable (tennis-racket effect)."

informal_lemma reduction_to_two_body where
  tag := "LL32-RTB"
  deps := [``RigidBody]
  statement :=
  "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."

informal_lemma rigid_body_work_and_power where
  tag := "LL32-WP"
  deps := [``RigidBody]
  statement :=
  "The power delivered to a rigid body by forces is P = ∑ F_i ⋅ v_i = F_tot ⋅ V + M ⋅ ω, where F_tot is total force, V the reference point velocity, and M the torque. Translational and rotational contributions separate."

[Joseph Tooby-Smith]

I think this looks great! And I think it is a really nice idea to use the tags to represent the result in Landau and Lifshitz! I'm assuming e.g.. "LL32" means Landau and Lifshitz page 32?

The' statement' I think need to actually be doc-strings (unless you've changed something else which means they can be statements).

[Afiq Hatta]

ah yeah i need to change those