Research proof index

The squared-speed integrand of kineticEnergy splits into the squared rotational speed |Ṙ (y − c)|², a term linear in the body-frame coordinate y − c, and the constant squared centre-of-mass speed ⟪V, V⟫.

The centre of mass of the moving mass distribution tracks the prescribed trajectory: for a body of nonzero mass, the centre of mass of massDistribution M t is exactly comTrajectory t. This is the decisive check that comTrajectory and orientation are wired correctly in RigidBodyMotion.

The velocity of a body point decomposes as v = Ṙ (y − c) + V: the rate of change of the orientation acting on the body-frame position, plus the centre-of-mass velocity.

A rigid body in pure translation (constant orientation) has every point moving with the centre-of-mass velocity: v = V.

For a set of 1-family SM charges satisfying all ACCs except the gravitational, if the Q charge is zero then the charges satisfy the gravitational ACCs.

The derivative of modelDiffeo provides an equivalence between Space d and EuclideanSpace ℝ (Fin d). This equivalences takes the basis of EuclideanSpace ℝ (Fin d) to the basis of Space d, and vice versa.