feat(ClassicalMechanics): add the body-frame angular velocity of a rigid body

[giuseppesorge]

Body-frame angular velocity of a rigid body

Adds the co-rotating (body-frame) angular velocity to
Physlib/ClassicalMechanics/RigidBody/AngularVelocity.lean, mirroring the existing spatial
angular-velocity section (angularVelocityTensor / angularVelocity). This is the natural
kinematic prerequisite for the inertia tensor in body-fixed axes and, downstream, Euler's
equations. One new concept, one file, no new files.

The spatial tensor is Ω = Ṙ Rᵀ; the body-frame tensor is its conjugate Ω_body = Rᵀ Ṙ = Rᵀ Ω R,
again skew-symmetric, with 3-dimensional dual ω_body = Ω_bodyᵛ.

New declarations (all in namespace RigidBodyMotion)

Declaration	Statement
bodyAngularVelocityTensor (def)	Ω_body(t) = R(t)ᵀ Ṙ(t)
bodyAngularVelocityTensor_eq	unfolding lemma (rfl)
bodyAngularVelocityTensor_transpose	skew-symmetry Ω_bodyᵀ = -Ω_body, from Rᵀ R = 1
orientation_mul_bodyAngularVelocityTensor	Ṙ = R Ω_body
angularVelocityTensor_eq_orientation_conj	Ω = R Ω_body Rᵀ (body ↔ spatial bridge)
bodyAngularVelocity (def, d = 3)	ω_body(t) = Ω_body(t)ᵛ via the hat map
bodyAngularVelocity_eq	unfolding lemma (rfl)
crossProductMatrix_bodyAngularVelocity	[ω_body]ₓ = Ω_body
bodyAngularVelocityTensor_of_orientation_const	constant orientation ⇒ Ω_body = 0
bodyAngularVelocity_of_orientation_const	constant orientation ⇒ ω_body = 0

The module docstring gains a paragraph on the body frame; references updated to Landau–Lifshitz
Sections 31 and 32.

Reviewer reading order

bodyAngularVelocityTensor → bodyAngularVelocityTensor_transpose (skew) →
orientation_mul_bodyAngularVelocityTensor (Ṙ = R Ω_body) →
angularVelocityTensor_eq_orientation_conj (Ω = R Ω_body Rᵀ) → bodyAngularVelocity →
crossProductMatrix_bodyAngularVelocity → the two const-orientation lemmas.

Verification

• lake build Physlib.ClassicalMechanics.RigidBody.AngularVelocity — succeeds; downstream
  KineticEnergy still builds.
• #print axioms on all 10 new declarations: only propext, Classical.choice, Quot.sound.
• lake exe runLinter Physlib.ClassicalMechanics.RigidBody.AngularVelocity — 0 issues in this
  file. (The reported errors are the pre-existing RigidBody/Basic.lean informal-stub
  underscore names and Meta/TODO, unchanged from master.)
• ./scripts/lint-style.sh — exit 0.

Follow-up (separate PR): König's theorem in the body frame,
T = ½ M ⟪V,V⟫ + rotationalKineticEnergy ω_body under centerOfMass = 0.

🤖 Drafted with AI assistance (Claude); the human author has reviewed and certifies every
statement.

[github-actions]

Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally.

If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks.

If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip.

Important: If a reviewer adds an awaiting-author label to your PR, once you have addressed the review comments, please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

[jstoobysmith]

Just a quick comment from me (will leave a full review to @nateabr). I think it might be worth explaining what the body frame actually is here more concretely, since I think this is the first time it has been mentioned anywhere in Physlib. E.g. How does it relate to the lab frame, is it inertial etc.

[giuseppesorge]

Good point, thanks — done. The module docstring now defines the body frame concretely: the coordinate system rigidly attached to the body (origin at the centre of mass, axes rotating with the body), in which every material point has time-independent coordinates. It also spells out how the frames are related — R(t) is the rotational part of the change of frame, mapping body-frame to lab-frame coordinates — and notes that the body frame is in general not inertial, but is the natural setting for the inertia tensor and Euler's equations since the mass distribution is time-independent there. I have rebased the stacked #1418 accordingly.

[jstoobysmith]

Great! May also want to consider if it makes sense to give the Body frame its own file system. Also at some-point, we should relate this to the action of rotation group and translation group on RidgidBody (discussed previously I think)

[giuseppesorge]

Thanks! On a dedicated file: my instinct is to keep the body-frame kinematics next to the spatial angular velocity for now — the two are tied together by the conjugation bridge Ω = R Ω_body Rᵀ and share the same time-derivative infrastructure — and to split out a dedicated file once the body-frame API grows beyond kinematics (inertia tensor in body axes, Euler's equations), which is where I am heading next. Happy to split already in this PR if you prefer.

On the group actions: agreed — that is exactly the TODO recorded in Motion.lean ("Define an action of the rotation and translation groups on RigidBodyMotion, and recover displacement as the composite of those group actions"). Once that action exists, the body frame is naturally characterised through it; I would tackle it together with the Euler-equations arc.

[jstoobysmith]

Why not define the angular velocity tensor through conjugation initially?

[giuseppesorge]

Both choices are equivalent — Rᵀ Ω R = Rᵀ (Ṙ Rᵀ) R = Rᵀ Ṙ is one line of algebra — so it is really a question of which fact is definitional. I defined Ω_body := Rᵀ Ṙ because that is the intrinsic, first-principles definition: the spatial and body tensors are the derivative Ṙ translated back to the identity from the two sides (Ω = Ṙ Rᵀ on the right, Ω_body = Rᵀ Ṙ on the left — the standard ġ g⁻¹ vs g⁻¹ ġ of geometric mechanics), so the two frames sit on an equal footing and neither is derived from the other; the conjugation is then a theorem rather than a definition. Proof economy is essentially a wash: under either definition every other fact is a one-liner. I kept the direct product-rule proof of skew-symmetry because it differentiates the second orthogonality identity Rᵀ R = 1, the left-handed twin of the spatial argument, so each tensor's membership in 𝔰𝔬(d) comes from its own defining identity — happy to golf it through the conjugation instead if you prefer.

I have now also added the converse bridge lemma bodyAngularVelocityTensor_eq_orientation_conj : Ω_body = Rᵀ Ω R (previously only Ω = R Ω_body Rᵀ was stated), so the conjugation you mention is available as a rewrite in both directions, and reworded the module/def docstrings so the definitional status is clear.

[nateabr]

Apologies I missed this comment and only saw it after my review. Although I appreciate the symmetry of your argument, but from maintenance perspective I do believe we would want a shorter algebraic proof.

[giuseppesorge]

No problem — agreed, and done: the latest commit golfs the skew-symmetry proof through the conjugation lemma (see the thread on bodyAngularVelocityTensor_transpose for the details).

[nateabr]

Generally things look great!

Adding Joseph's remarks have made the file better but I have to point out that the doc-strings for the lemmas are repeating points from the overview verbatim and are quite verbose/redundant (for eg. bodyAngularVelocityTensor). I would recommend making them more concise as your overview is great and explains everything quite well.

[nateabr]

I believe this is quite an easy golf using the other lemmas in this file.

You can use the conjugation lemma bodyAngularVelocityTensor_eq_orientation_conj and the spatial skew-symmetry angularVelocityTensor_transpose to prove it algebraically without calculus. Should be no more than 3-4 lines but please do check this.

This would require you to reorder the lemmas in this file but I do believe this is a better logical flow for the overall file

[giuseppesorge]

Done — good call. The body-frame section is now ordered def → Ṙ = R Ω_body → the two conjugation bridges → skew-symmetry, and bodyAngularVelocityTensor_transpose is a single algebraic rewrite from bodyAngularVelocityTensor_eq_orientation_conj plus the spatial angularVelocityTensor_transpose, no calculus. Agreed the file reads better this way.

[giuseppesorge]

Thanks for the review! Both points are addressed in the latest commit: the skew-symmetry proof is golfed via the conjugation lemma (with the section reordered accordingly), and the body-frame docstrings are now concise — the defs just name their objects and the lemmas carry one-line statements, leaving the discussion to the overview.

[jstoobysmith]

Merged - many thanks