feat(ClassicalMechanics): add rigid-body angular momentum and prove L = Iω

[giuseppesorge]

This PR adds the angular momentum of a rigid body and proves the fundamental identity L = I ω, the first step of the Landau–Lifshitz §32 rigid-body dynamics arc (#893).

For a body rotating with angular velocity ω about its reference point, each point at r moves with velocity ω × r, so the angular momentum is L = ∫ r × (ω × r) dm. Expanding the double cross product, r × (ω × r) = |r|² ω − (r · ω) r, shows that L is linear in ω with matrix the (already-formalized) inertia tensor.

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

• RigidBody.angularMomentum ω — the angular momentum, defined as ρ applied componentwise to the physical integrand r × (ω × r) (mathlib's ⨯₃ on the Space 3 coordinates);
• angularMomentum_eq_inertiaTensor_mulVec — L = inertiaTensor *ᵥ ω.

Physlib/Mathematics/CrossProductMatrix.lean

• Matrix.cross_cross_self_apply — the general bac−cab expansion [v ⨯₃ (w ⨯₃ v)]ᵢ = |v|² wᵢ − (v · w) vᵢ for v w : Fin 3 → ℝ, a thin componentwise corollary of mathlib's cross_cross_eq_smul_sub_smul'. It is the algebraic core of L = Iω and, being a general cross-product identity with no physics content, lives in the general cross-product file rather than the classical-mechanics one.

Builds only on merged master (RigidBody.inertiaTensor and the ρ mass-distribution API in Basic.lean, plus the cross-product file from #1324/#1363). All declarations reduce to [propext, Classical.choice, Quot.sound].

This is the shared algebraic kernel of the next steps: König's kinetic-energy decomposition T = ½M|V|² + ½ ω · Iω is the same expansion dotted with ω, and Euler's equations consume L = Iω.

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.

[jstoobysmith]

I think either we:

1. Move this lemma to a CrossProduct file,
2. or, rename this file to CrossProduct.

[giuseppesorge]

Thanks! Went with option 1 — moved cross_cross_self_apply into a new Physlib/Mathematics/CrossProduct.lean, keeping CrossProductMatrix.lean for the hat map, and pointed AngularMomentum.lean at the new file.

[giuseppesorge]

-awaiting-author

[jstoobysmith]

Looks good - approved.