feat(PhyslibAlpha): the mass cocycle of the Galilean group (Souriau)

[KevorkianPhilippe]

AI disclosure

This file was generated with Claude (Claude Code, Opus 5.5) under my supervision, following
AI-POLICY.md and AGENTS.md. I have read every definition and lemma statement and I vouch that
they state what the docstrings say. The main statements (sections B, C, E, F) adapt a separate
development where they were frozen before any proof was written and proved by local models
(BFS-Prover-V2, Qwen3.8-27B) and by Claude, on a Galilean group of its own with rotations in
SO(3). This file restates them on Physlib's GalileanGroup 3, which has rotations in O(3), and in
Mathlib's cohomology vocabulary, and adds declarations with no counterpart there (the O(3) lemmas
of section A, smul_time_position, vectorField_injective, the vector space structure and the
closed-form coadjoint action on torsors). Claude wrote or adapted all the proofs of this file; the
extension to O(3) was checked numerically before it was proved, and a second, independent Claude
session then checked every statement and docstring against the printed pages; its main finding
(the non-coboundary statements must also be stated on SO(3)) is in the second commit of this
PR. The
bibliographic references (Souriau 1970, pp. 52-53, 108, 109, 111, 112, 113, 139-140, 151-153, and
the equation numbers cited in the docstrings) were checked by me on the printed pages, not by the
AI.

Summary

Depends on #1684 (MomentMap/GalileanMass.lean, the Lie algebra level), whose commits this branch
contains. This PR is the three commits on GalileanMassCocycle.lean: the last one moves it into
MomentMap/, next to GalileanMass.lean, as agreed in #1684; the merge commits bring in #1684
and master (the last one also updates the import of GalileanMass.lean, which #1684 moved).

Adds PhyslibAlpha/ClassicalMechanics/MomentMap/GalileanMassCocycle.lean, the group level of
Souriau's chapter 12, built on Physlib's GalileanGroup 3 rather than on a new group. It defines
the action of the Galilean group on the evolution space of N free material points (12.76), the
adjoint action on GalileanAlgebra (6.24), a real vector space structure on GalileanTorsor and
the coadjoint action (11.15), and Souriau's cocycle θ₀(a) = {c × b, c - b e, b, ½ ‖b‖²} (12.127).
It proves that the moment of the free points satisfies μ(a • y) - a • μ(y) = (Σ m_j) θ₀(a)
(12.126), that θ₀ is a 1-cocycle whose multiples M θ₀ are coboundaries only for M = 0
(12.128), (12.136), and that its derivative at the identity is the algebra cocycle f₀ of #1684
(12.130). The cohomology vocabulary is Mathlib's (groupCohomology.IsCocycle₁, IsCoboundary₁), as
in #1681.

GalileanGroup takes its rotation part in O(3), Souriau in SO(3). The identities hold on O(3) once
the rotation vector ω (an axial vector) is transformed with a factor det R, and restrict to
Souriau's group. A non-coboundary statement does not restrict to a subgroup, so the statements of
p. 151 and (12.136) are also proved on properGalileanGroup (det R = 1), which is Souriau's
group (12.73). The module docstring lists what is not formalised.

Declarations added (namespace ClassicalMechanics)

Section A (orthogonal matrices, Fin 3 → ℝ):

• ofLp_orthogonal_smul, ofLp_real_smul: the actions on EuclideanSpace ℝ (Fin 3) in
  coordinates.
• orthogonal_transpose_mul_self, orthogonal_mul_transpose_self, orthogonal_inv_val,
  orthogonal_det_mul_self, orthogonal_det_inv, orthogonal_adjugate.
• orthogonal_mulVec_dotProduct, dotProduct_transpose_mulVec.
• orthogonal_mulVec_cross: R (u × v) = det R • (R u × R v);
  orthogonal_transpose_mulVec_cross; cross_dotProduct_det_smul_transpose_mulVec.

Section B (sub-namespace EvolutionSpace):

• SMul and MulAction (GalileanGroup 3) (EvolutionSpace N): (12.76), (12.77); smul_t,
  smul_r, smul_v.
• smul_time_position: on each point, the action is GalileanGroup's action on Time × Space 3.
• tangentSMul, smul_line: the differential of the (affine) action.
• lagrangeForm_smul: (12.76), invariance of the Lagrange form.

Section C:

• SMul and MulAction (GalileanGroup 3) GalileanAlgebra: the adjoint action (6.24);
  GalileanAlgebra.smul_ω, smul_β, smul_γ, smul_ε, GalileanAlgebra.inv_smul_eq.
• EvolutionSpace.vectorField_smul: (6.25); EvolutionSpace.vectorField_injective.

Section D (sub-namespace GalileanTorsor):

• equivProd; AddCommGroup and Module ℝ instances; pair_add, pair_sub, pair_zero,
  pair_smul, ext_pair.
• SMul, MulAction and DistribMulAction of GalileanGroup 3: the coadjoint action;
  coadjoint_pair: (11.15); coadjoint_smul_real: it is linear.

Section E:

• massCocycle: θ₀ (12.127); massCocycle_one.
• isCocycle₁_massCocycle: (12.128).
• eq_zero_of_smul_massCocycle_boost: the witness of p. 151, a pure boost.
• isCoboundary₁_smul_massCocycle_iff, not_isCoboundary₁_massCocycle: p. 151 on the whole
  group.
• properGalileanGroup: the subgroup det R = 1, Souriau's group (12.73);
  isCocycle₁_massCocycle_proper, isCoboundary₁_smul_massCocycle_proper_iff,
  not_isCoboundary₁_massCocycle_proper: (12.128) and p. 151 on it.
• EvolutionSpace.moment_smul_sub: (12.126)-(12.127) with m = Σ_j m_j, (12.132).
• EvolutionSpace.not_isCoboundary₁_moment_smul_sub, ..._proper: (12.136) for the system, on
  the whole group and on Souriau's group.

Section F:

• hasDerivAt_massCocycle: (12.130), along curves through the identity;
  hasDerivAt_massCocycle_line: the same along s ↦ (1, s b', s c', s e').

Also: one line in PhyslibAlpha.lean. Two private helper lemmas (hasDerivAt_dotProduct,
hasDerivAt_cross) and one (mulVec_cross_mulVec) serve sections F and A.

Reviewer map

1. The module docstring, in particular the O(3) paragraph.
2. The three actions: EvolutionSpace (section B), GalileanAlgebra (section C, with
   vectorField_smul), GalileanTorsor (section D, with coadjoint_pair).
3. Section E: massCocycle, moment_smul_sub, isCocycle₁_massCocycle, then the coboundary
   statements and properGalileanGroup.
4. hasDerivAt_massCocycle (section F).
5. Section A (orthogonal matrices, technical).

Checks run

• lake build -KCI and lake build -KCI PhyslibAlpha on the branch, with current master merged
  in (toolchain v4.34.1): success, no warning in this file.
• lake exe runPhyslibAlphaLinters, alphaFileImports.py, noAlphaImports.py,
  ./scripts/PhyslibAlpha/alphaPythonLinters.sh, ./scripts/lint-style.sh,
  scripts/api_map_linter.py, codespell: pass.
• #print axioms on every public lemma: [propext, Classical.choice, Quot.sound].

🤖 Generated with Claude Code

[github-actions]

Thank you for this pull-request (PR). If this is your first PR, welcome to the community!

Below is what will happen next. Please read carefully if you are not familiar with the process. You may open other PRs while this one is being reviewed, and can stack PRs on top of each other, so don't let these steps slow you down.

1. Some automated checks will be run on your PR. You can see the results of these checks at the buttom of your PR page. If any of these checks fail, you will need to fix the issues before your PR can be merged. You can learn more about these here, including how to run them locally, which is sometimes quicker than relying on the GitHub Actions. If you have never had a PR merged before, you may have to wait for a reviewer to manually start these checks (this is for security).

2. A reviewer will look at your PR and may ask you to make changes. This may happen a couple of days after you submit your PR, so you may need to be patient. But it should not be longer than that - if it is please bring it to the attention of the community on the Zulip. The level of review will depend on where your PR is submitted. If it is submitted to ./Physlib or ./QuantumInfo, the review will be more thorough than if it is submitted to ./PhyslibAlpha. You can find out more about what the review process is looking for in our review guidelines. If a reviewer adds an awaiting-author label to your PR, address the review comments, then please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

3. The reviewer will either approve your PR, or request more changes (in which case we return to step 2). Once your PR is approved, it will be merged by a maintainer, this should happen shortly after approval, though you may get more comments at this stage.

Tip: The easiest way to get have a fast review is to submit a PR that is small and self-contained, and has clear documentation explaining why things are the way they are in your chages.

If you have any problems or questions, please reach out to the community on the Zulip.