feat(ClassicalMechanics): add rotational kinetic energy and prove T = ½ω·Iω

[giuseppesorge]

This PR adds the rotational kinetic energy of a rigid body and proves T = ½ ω · I ω = ½ ∫ |ω × r|² dm. It is the rotational half of König's theorem (Landau–Lifshitz §32) and the natural sequel to the merged L = I ω (#1366).

A rigid body spinning with angular velocity ω about its reference point carries the point at r with velocity ω × r, so its kinetic energy is T = ½ ∫ |ω × r|² dm. Since |ω × r|² = ω · (r × (ω × r)) and the angular momentum is L = ∫ r × (ω × r) dm = I ω, this is the quadratic form T = ½ ω · L = ½ ω · (I ω).

Physlib/ClassicalMechanics/RigidBody/KineticEnergy.lean (new)

• RigidBody.rotationalKineticEnergy ω — ½ (ω ⬝ᵥ inertiaTensor *ᵥ ω), the rotational kinetic energy about the reference point;
• rotationalKineticEnergy_eq_angularMomentum — T = ½ ω · L (contraction of ω with the angular momentum);
• rotationalKineticEnergy_eq_integral — T = ½ ∫ |ω × r|² dm, the physical form justifying the quadratic form as the rotational kinetic energy.

Physlib/Mathematics/CrossProduct.lean

• Matrix.dotProduct_cross_cross_self — the scalar triple-product identity w · (v × (w × v)) = (w × v) · (w × v) (over ℝ, |w × v|²) for v w : Fin 3 → R over any CommRing R, the algebraic core relating the ω·L contraction to the local speed |ω × r|². Sits alongside the existing cross_cross_self_apply in the general cross-product file.

Notes:

• |ω × r|² is written as the self-dot-product (ω ⨯₃ x) ⬝ᵥ (ω ⨯₃ x): on Fin 3 → ℝ the mathlib norm ‖·‖ is the sup norm, so ‖ω ⨯₃ x‖² would be the wrong quantity.
• The inertia tensor here is about the reference-frame origin, so rotationalKineticEnergy is the kinetic energy of rotation about that fixed reference point — no centre of mass = origin assumption is made. König's full decomposition T = ½M|V|² + ½ω·Iω (which specialises the reference point to the centre of mass) is the next step.
• All four declarations reduce to [propext, Classical.choice, Quot.sound].

Toward #893.

[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.

[gloges]

Just a few minor comments/suggestions.

For my own understanding, why is Fin 3 → ℝ favored over EuclideanSpace ℝ (Fin 3)? The latter would address the point you raise about the sup norm.

[gloges]

Suggested change

	simp only [dotProduct, angularMomentum]
	rw [Finset.sum_congr rfl (fun i (_ : i ∈ Finset.univ) =>
	(smul_eq_mul (ω i) _).symm.trans (map_smul R.ρ (ω i) _).symm), ← map_sum]
	simp_rw [dotProduct, angularMomentum, ← smul_eq_mul, ← map_smul, ← map_sum]

[gloges]

Suggested change

	A rigid body rotating with angular velocity `ω` about its reference point carries the point at
	position `r` with velocity `ω × r`, so its kinetic energy is `T = ½ ∫ |ω × r|² dm`. Since
	For a rigid body rotating with angular velocity `ω` about its reference point the point at
	position `r` has velocity `ω × r`, so its kinetic energy is `T = ½ ∫ |ω × r|² dm`. Since

[gloges]

I would recommend extracting out this ContDiff statement about the cross/dot product into a separate lemma.

[giuseppesorge]

Thanks! Applied all three — reworded the docstring, extracted the integrand smoothness into contDiff_rotationalSpeedSq, and golfed the ω pull-through to your simp_rw one-liner. On Fin 3 → ℝ vs EuclideanSpace ℝ (Fin 3): the whole rigid-body cross-product API is on Fin 3 → ℝ — mathlib's ⨯₃, RigidBody.inertiaTensor : Matrix (Fin 3) (Fin 3) ℝ acting via *ᵥ, and angularMomentum ω : Fin 3 → ℝ are all there. Switching to EuclideanSpace ℝ (Fin 3) (= PiLp 2) would add WithLp/coercion friction at every ⨯₃ / *ᵥ / ⬝ᵥ site. The sup-norm caveat only affects how |·|² is written, and the explicit self-⬝ᵥ sidesteps it without changing the API — so Fin 3 → ℝ keeps consistency with the existing inertia-tensor / angular-momentum layer.

[jstoobysmith]

Would now move to the CrossProduct file

[jstoobysmith]

awaiting-author

[giuseppesorge]

Done — generalized it to Fin 3 → ℝ as Matrix.contDiff_cross_dotProduct_cross and moved it to the CrossProduct file (adding the ContDiff import there); the kinetic-energy integrand now composes it with the coordinate coercion of Space 3.

[giuseppesorge]

-awaiting-author

[jstoobysmith]

Looks good - approved.