feat(PhyslibAlpha): cohomology class of the affine symplectic group (Souriau)

[KevorkianPhilippe]

AI disclosure

This file was generated with Claude (Claude Code: Fable 5.1 for the file, Opus 5.5 for opening
this PR) 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; the proofs were first found against those frozen
statements by two local models running on my own hardware (a Lean best-first prover and a 27B
general model), then rewritten by Claude for this file. The bibliographic reference (Souriau 1970,
chapter 11, pp. 104-117, and the equations (6.24)-(6.25), (10.12), (10.28)-(10.32) cited in the
docstrings) was checked by me on the printed pages, not by the AI.

Stacked on #1680 (moment-map-1): the diff includes its commit; only the last commit is new
here.

Summary

Adds PhyslibAlpha/ClassicalMechanics/MomentMapCohomology.lean, the group level of Souriau's
chapter 11 for the affine symplectic group Sp(E) ⋉ E of his example (10.12), acting on a real
symplectic vector space by x ↦ B x + C. It defines the group, its Lie algebra, the adjoint and
coadjoint actions and the moment, and proves that the defect θ(a) = μ(a_E(x)) - a_{𝔤*}(μ(x))
does not depend on x and equals μ(C) (11.17 a), that θ is a 1-cocycle in Mathlib's
groupCohomology vocabulary (11.17 b), and that its class is non-zero as soon as E ≠ 0. No
manifold or Lie group structure is involved.

Declarations added (namespace ClassicalMechanics.AffineSymplecticGroup unless noted)

Section A:

• AffineSymplecticGroup (structure, in ClassicalMechanics): the affine maps x ↦ B x + C
  with B preserving σ (10.12).
• Instances Mul, One, Inv, Group, and MulAction on E (a_E(x) = B x + C).
• mul_linear, mul_translation, one_linear, one_translation, inv_linear,
  inv_translation, ext, smul_def: the group law and the action on components.

Section B:

• affineSymplecticAlgebra, mem_affineSymplecticAlgebra: the Lie algebra, pairs (A, b) with
  A infinitesimally symplectic ((10.28)-(10.32)).
• vectorField: Z_E(x) = A x + b, as in AffineSymplecticAction (feat(PhyslibAlpha): Souriau's moment map on a symplectic vector space, cocycle and Noether's theorem #1680).
• adjoint, adjoint_one, adjoint_mul: the adjoint action (6.24).
• vectorField_adjoint: (6.25), (Ad(a) Z)_E (a_E x) = B (Z_E x); vectorField_injective.

Section C:

• Instances SMul, MulAction, DistribMulAction on Module.Dual ℝ (affineSymplecticAlgebra σ):
  the coadjoint action (11.15), μ ∘ Ad(a⁻¹); coadjoint_smul_apply.
• moment, moment_apply, moment_zero: the moment (11.7) of the affine symplectic action.

Section D:

• moment_smul_sub_smul_moment: (11.17 a) in closed form, θ(a) = μ(C).
• isCocycle₁_moment_translation: (11.17 b), θ is a groupCohomology.IsCocycle₁.
• sigmaLinear, sigmaLinear_apply, hasFDerivAt_quad, hasFDerivAt_moment: derivative
  computations, (11.7) for this group.
• hasDerivAt_moment_translation: part of (11.17 c), the derivative of θ at the identity along
  a curve equals the cocycle of feat(PhyslibAlpha): Souriau's moment map on a symplectic vector space, cocycle and Noether's theorem #1680 (a relation by formula).
• not_isCoboundary₁_moment_translation: the class of θ is not zero when E ≠ 0.

Section E:

• planeForm_not_isCoboundary₁: the same for the symplectic plane.

Also: one line in PhyslibAlpha.lean.

Reviewer map

1. The module docstring, then section A (the group and its action).
2. moment (section C) and moment_smul_sub_smul_moment (section D): the main computation.
3. isCocycle₁_moment_translation and not_isCoboundary₁_moment_translation.
4. Section B (adjoint action) and the rest of section C.
5. The derivative computations of section D (technical).

Checks run

• lake build -KCI PhyslibAlpha on the branch merged with current master: success, no warning in
  this file.
• lake exe runPhyslibAlphaLinters, alphaFileImports.py, noAlphaImports.py,
  ./scripts/PhyslibAlpha/alphaPythonLinters.sh, ./scripts/lint-style.sh: pass.
• #print axioms on every declaration: [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]

To fix the lints here you'll probably have to add something to .codespellignore.

[jstoobysmith]

I've merged your other pull request in this direction. Do you mind updating this to deal with the conflict?

awaiting-author

[jstoobysmith]

Looks good, approved

[KevorkianPhilippe]

Done: master is merged in (1466b96); the conflict was only in the import list of
PhyslibAlpha.lean. The codespell error is fixed by dropping the French chapter title from the
references, a change that came in with #1680, so .codespellignore is left as it is.

Drafted with Claude, reviewed and validated by me.

-awaiting-author