feat(PhyslibAlpha): the mass as a cohomology class of the Galilean Lie algebra (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 statements were frozen before any proof was written and
proved first in a separate development, where the proofs came from local models (BFS-Prover-V2,
Qwen3.8-27B) and from Claude; Claude then wrote this file in Physlib style from that development.
A second, independent Claude session then checked every statement and docstring against the
printed pages; it found no error in the statements, and its corrections to the docstrings are the
second commit. The bibliographic references (Souriau 1970, pp. 27, 50, 109, 113-116, 132-133,
139-140, 148, 150-153, and the equation numbers cited in the docstrings) were checked by me on the
printed pages, not by the AI.

Summary

Adds PhyslibAlpha/ClassicalMechanics/MomentMap/GalileanMass.lean, one self-contained file
(imports Mathlib only) on Souriau's chapter 12: the total mass of a system of material points as the
cohomology class of the Galilean group, here at the level of the Lie algebra and for N free
material points in Fin 3 → ℝ. It defines the Galilean Lie algebra in Souriau's parametrisation
(ω, β, γ, ε) with his bracket, the torsors {l, g, p, E}, the 2-form
f₀(Z)(Z') = ⟨β, γ'⟩ - ⟨β', γ⟩, and the evolution space with its vector fields, Lagrange form
and moment. It proves (12.134), σ(Z_V, Z'_V) = μ[Z, Z'] + (Σ m_j) f₀(Z)(Z'), and that
M f₀ is a coboundary of the algebra only for M = 0. No manifold is involved.

Physlib has GalileanGroup in Physlib.SpaceAndTime.GalileanGroup.Basic, whose rotation part
ranges over O(3), while Souriau's group (12.73) has its rotation in SO(3). Both have the same Lie
algebra, with which this file works in dimension 3; the file links it to neither group (the module
docstring lists what is not formalised). The evolution space is presymplectic (12.114) and its
Lagrange form depends on the point, so the setting of
PhyslibAlpha.ClassicalMechanics.MomentMap.Basic (#1680) is not reused.

As agreed in the review, the two merged files on the moment map move into the same subdirectory
PhyslibAlpha/ClassicalMechanics/MomentMap/: MomentMap.lean becomes MomentMap/Basic.lean
(#1680) and MomentMapCohomology.lean becomes MomentMap/Cohomology.lean (#1681). Only their
imports and one docstring reference to the module name change (last commit).

Declarations added (namespace ClassicalMechanics)

Section A (sub-namespace GalileanAlgebra):

• GalileanAlgebra (structure, in ClassicalMechanics), with Zero and Add instances.
• bracket: Souriau's bracket (6.12 b), (11.22 a).
• bracket_antisymm, bracket_jacobi, bracket_boost_translation.

Section B:

• GalileanTorsor (structure): {l, g, p, E} (12.123); GalileanTorsor.pair: (12.122).

Section C (sub-namespace GalileanAlgebra):

• cocycle: f₀ (12.130); cocycle_antisymm; cocycle_cyclic (12.129);
  cocycle_boost_translation.
• smul_cocycle_isCoboundary_iff: M f₀ is a coboundary of the algebra iff M = 0;
  cocycle_not_coboundary.

Section D (sub-namespace EvolutionSpace):

• EvolutionSpace N (structure, in ClassicalMechanics), with a Sub instance.
• vectorField: Z_V (12.119); linearPart; vectorField_bracket.
• lagrangeForm: (12.40) with no forces; lagrangeForm_antisymm; lagrangeForm_motion
  ((12.41)-(12.43), the free motion is in the kernel of σ).

Section E (sub-namespace EvolutionSpace):

• moment (12.135); line; motion; pair_moment.
• hasDerivAt_moment: (12.124).
• moment_motion: (12.121).

Section F (sub-namespace EvolutionSpace):

• totalMass; centerOfMass.
• lagrangeForm_vectorField: (12.134) with m = Σ_j m_j.
• totalMass_cocycle_not_coboundary: (12.136) at the level of the algebra.
• moment_g, centerOfMass_motion: (12.141).

Also: the imports in PhyslibAlpha.lean. Two private helper lemmas (pair_term_line,
hasDerivAt_quadratic) serve hasDerivAt_moment.

Reviewer map

1. The module docstring, then the three structures and the definitions bracket,
   GalileanTorsor.pair, cocycle, vectorField, lagrangeForm, moment.
2. lagrangeForm_vectorField and totalMass_cocycle_not_coboundary (section F), the main
   results.
3. smul_cocycle_isCoboundary_iff and cocycle_cyclic (section C).
4. hasDerivAt_moment and moment_motion (section E).
5. The remaining lemmas (bracket identities, vectorField_bracket, (12.141)).

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 the three files of MomentMap/.
• 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.

[jstoobysmith]

Maybe we should think of a good subdirectory for these results?

[KevorkianPhilippe]

Agreed. All these files revolve around Souriau's moment map, so I would suggest PhyslibAlpha/ClassicalMechanics/MomentMap/: Basic.lean (now MomentMap.lean), Cohomology.lean (now MomentMapCohomology.lean), GalileanMass.lean, and the two follow-ups, on the Galilean group (GalileanMassCocycle.lean) and on its Lie algebra (GalileanAlgebraCohomology.lean). If that suits you, I will move this file there in this PR and the two merged files in a separate PR. Happy to use another name if you prefer.

Drafted with Claude, reviewed and validated by me.

[jstoobysmith]

This looks good to me. Feel free to move files in this pull request.

[jstoobysmith]

awaiting-author

[KevorkianPhilippe]

Done (ae21c03): MomentMap.lean is now MomentMap/Basic.lean, MomentMapCohomology.lean is MomentMap/Cohomology.lean, and this file is MomentMap/GalileanMass.lean; only the imports and two docstring references to the module name change. Master is also merged in, and the description is updated.

Drafted with Claude, reviewed and validated by me.

-awaiting-author

[jstoobysmith]

Approved, will merge shortly.