From c7d4f8bc9c5bcbdca80acde645b7f07fda80c8c2 Mon Sep 17 00:00:00 2001 From: Philippe Kevorkian Date: Thu, 24 Sep 2026 14:57:20 +0200 Subject: [PATCH 1/3] feat(PhyslibAlpha/ClassicalMechanics): the mass as a cohomology class of the Galilean Lie algebra Souriau's chapter 12 (SDS, Dunod 1970, pp. 132-153) at the level of the Lie algebra, for N free material points in Fin 3 -> R. Adds GalileanAlgebra (omega, beta, gamma, epsilon) with Souriau's bracket, GalileanTorsor {l, g, p, E} with the pairing (12.122), the 2-form f0 (12.130), and EvolutionSpace N with the vector fields (12.119), the Lagrange form (12.40) without forces and the moment (12.135). Results: the Jacobi identity; (12.129); M f0 is a coboundary of the algebra iff M = 0; (12.124) as a derivative along lines; (12.121) along the free motions; (12.134) with m = sum of the m_j; (12.136) at the level of the algebra; (12.141) g = m R - p t and the uniform motion of the centre of gravity of free points. Co-Authored-By: Claude Opus 5.5 --- PhyslibAlpha.lean | 1 + .../ClassicalMechanics/GalileanMass.lean | 460 ++++++++++++++++++ 2 files changed, 461 insertions(+) create mode 100644 PhyslibAlpha/ClassicalMechanics/GalileanMass.lean diff --git a/PhyslibAlpha.lean b/PhyslibAlpha.lean index e5b26955d..192cb991c 100644 --- a/PhyslibAlpha.lean +++ b/PhyslibAlpha.lean @@ -27,6 +27,7 @@ public import PhyslibAlpha.SpaceAndTime.Space.Surfaces.SphericalCylinder public import PhyslibAlpha.SpaceAndTime.Space.Surfaces.SolidCylinder public import PhyslibAlpha.SpaceAndTime.Space.Surfaces.SolidSphere public import PhyslibAlpha.SpaceAndTime.Space.Surfaces.SphericalShell +public import PhyslibAlpha.ClassicalMechanics.GalileanMass public import PhyslibAlpha.ClassicalMechanics.MomentMap public import PhyslibAlpha.ClassicalMechanics.NortonDome.Basic public import PhyslibAlpha.ClassicalMechanics.NortonDome.Determinism diff --git a/PhyslibAlpha/ClassicalMechanics/GalileanMass.lean b/PhyslibAlpha/ClassicalMechanics/GalileanMass.lean new file mode 100644 index 000000000..a86a7b76d --- /dev/null +++ b/PhyslibAlpha/ClassicalMechanics/GalileanMass.lean @@ -0,0 +1,460 @@ +/- +Copyright (c) 2026 Philippe Kevorkian. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Philippe Kevorkian +-/ +module + +public import Mathlib.LinearAlgebra.CrossProduct +public import Mathlib.Analysis.Calculus.Deriv.Add +public import Mathlib.Analysis.Calculus.Deriv.Mul +public import Mathlib.Analysis.Calculus.Deriv.Pow +/-! + +# The mass as a cohomology class of the Galilean Lie algebra (Souriau) + +## i. Overview + +In chapter 12 of Structure des systèmes dynamiques (Dunod 1970), Souriau computes the moment of +the Galilean group acting on the evolution space of a system of material points. The moment is a +torsor `μ = {l, g, p, E}` (12.122)-(12.123): `l` is the angular momentum and `p` the momentum +(12.140), and `g = m R - p t` with `R` the centre of gravity (12.141). The Lagrange form `σ` of the +system satisfies (12.134), `σ(Z_V(y))(Z'_V(y)) = μ[Z, Z'] + m f₀(Z)(Z')`, where +`f₀(Z)(Z') = ⟨β, γ'⟩ - ⟨β', γ⟩` (12.130) and `m = Σ_j m_j` is the total mass (12.135). Souriau +concludes (12.136) that the total mass characterises the cohomology class of the system, and that +this class is never zero. + +This file proves these facts at the level of the Lie algebra for `N` free material points in +`ℝ³ = Fin 3 → ℝ` (no forces: `F_j = 0`, hence `E_j = B_j = 0` in (12.44)-(12.45)). An element +`Z = (ω, β, γ, ε)` of the Galilean Lie algebra (12.74), (12.118) is a rotation `ω` (an axial +vector), a change of velocity `β`, a space translation `γ` and a time translation `ε`; it acts on +the evolution space, whose points are `y = (t, r_j, v_j)` (12.76), by the affine vector field +(12.119). The bracket is Souriau's, `[Z, Z']_V = DZ'_V(Z_V) - DZ_V(Z'_V)` ((6.12 b), (11.22 a)), +opposite to the usual commutator (`EvolutionSpace.vectorField_bracket`). + +What is not formalised here: +- the Galilean group itself, its action (12.73), (12.76) and its cocycle `θ₀` (12.126)-(12.128), + hence the passage from the algebra to the group used on p. 151 and in (12.136). The Galilean group + is `GalileanGroup` in `Physlib.SpaceAndTime.GalileanGroup.Basic`; this file works with its Lie + algebra in dimension `3`, in Souriau's parametrisation, and does not link the two; +- `GalileanAlgebra` has no vector space or `LieRing` structure here, only `Zero` and `Add`; the + Jacobi identity is proved as an equation; +- the dimension `1` of (12.131), the second half of (12.136) (Hamilton's Lagrangian is not + invariant), forces, the converse of (12.48), the invariance of `σ` (12.72), (12.76), and the + uniqueness of the moment up to a constant (the constant in `E` is a choice); +- the evolution space is only presymplectic (`EvolutionSpace.lagrangeForm_motion`), so the setting + of `PhyslibAlpha.ClassicalMechanics.MomentMap` is not used; the moment and the cocycle are + computed explicitly. + +## ii. Key results + +- `GalileanAlgebra.bracket_jacobi`: the Jacobi identity for Souriau's bracket. +- `GalileanAlgebra.cocycle_cyclic`: (12.129), `f₀` satisfies the cyclic identity. +- `GalileanAlgebra.smul_cocycle_isCoboundary_iff`: `M f₀` is an algebra coboundary, + `M f₀(Z)(Z') = μ₀[Z, Z']` for some torsor `μ₀`, if and only if `M = 0`. +- `EvolutionSpace.hasDerivAt_moment`: (12.124), the moment of the free points. +- `EvolutionSpace.moment_motion`: (12.121), the moment is constant along the free motions. +- `EvolutionSpace.lagrangeForm_vectorField`: (12.134) with `m = Σ_j m_j` (12.135). +- `EvolutionSpace.totalMass_cocycle_not_coboundary`: (12.136) at the level of the algebra, for a + non-zero total mass the cocycle of the system is not a coboundary. +- `EvolutionSpace.moment_g`, `EvolutionSpace.centerOfMass_motion`: (12.141), `g = m R - p t`, and + the uniform motion of the centre of gravity of free points. + +## iii. Table of contents + +- A. The Galilean Lie algebra +- B. Torsors +- C. The cocycle `f₀` +- D. The evolution space of free material points +- E. The moment +- F. The cocycle of the system and the mass + +## iv. References + +- J.-M. Souriau, Structure des systèmes dynamiques, Dunod, Paris, 1970: pp. 132-133 + (12.40)-(12.48), pp. 139-140 (12.72)-(12.76), pp. 150-153 (12.118)-(12.141); p. 50 (6.12 b) and + p. 113 (11.22 a) for the bracket; p. 116, note (1), for the coboundaries of the algebra. + +## References + +* J.-M. Souriau, *Structure des systèmes dynamiques*, Maîtrises de mathématiques, Dunod, + Paris, 1970, chapter 12, pp. 132-153. The equation numbers refer to this edition. + [ref: Souriau1970] + +-/ + +@[expose] public section + +noncomputable section + +namespace ClassicalMechanics + +open Matrix + +local notation "ℝ³" => Fin 3 → ℝ + +/-! + +## A. The Galilean Lie algebra + +-/ + +/-- An element `Z = (ω, β, γ, ε)` of the Lie algebra of the Galilean group, in Souriau's +parametrisation (12.74), (12.118). -/ +@[ext] +structure GalileanAlgebra where + /-- The infinitesimal rotation, as an axial vector. -/ + ω : ℝ³ + /-- The change of velocity (infinitesimal boost). -/ + β : ℝ³ + /-- The space translation. -/ + γ : ℝ³ + /-- The time translation. -/ + ε : ℝ + +namespace GalileanAlgebra + +instance : Zero GalileanAlgebra := ⟨⟨0, 0, 0, 0⟩⟩ + +instance : Add GalileanAlgebra := ⟨fun Z Z' => ⟨Z.ω + Z'.ω, Z.β + Z'.β, Z.γ + Z'.γ, Z.ε + Z'.ε⟩⟩ + +/-- Souriau's bracket on the Galilean Lie algebra. It is the bracket of the vector fields (12.119) +in the convention (6.12 b), (11.22 a), see `EvolutionSpace.vectorField_bracket`. -/ +def bracket (Z Z' : GalileanAlgebra) : GalileanAlgebra := + ⟨Z'.ω ⨯₃ Z.ω, Z'.ω ⨯₃ Z.β - Z.ω ⨯₃ Z'.β, + Z'.ω ⨯₃ Z.γ - Z.ω ⨯₃ Z'.γ + Z.ε • Z'.β - Z'.ε • Z.β, 0⟩ + +/-- The bracket is antisymmetric. -/ +lemma bracket_antisymm (Z Z' : GalileanAlgebra) : bracket Z Z' + bracket Z' Z = 0 := by + apply GalileanAlgebra.ext + · change Z'.ω ⨯₃ Z.ω + Z.ω ⨯₃ Z'.ω = 0 + simp + · change (Z'.ω ⨯₃ Z.β - Z.ω ⨯₃ Z'.β) + (Z.ω ⨯₃ Z'.β - Z'.ω ⨯₃ Z.β) = 0 + abel + · change (Z'.ω ⨯₃ Z.γ - Z.ω ⨯₃ Z'.γ + Z.ε • Z'.β - Z'.ε • Z.β) + + (Z.ω ⨯₃ Z'.γ - Z'.ω ⨯₃ Z.γ + Z'.ε • Z.β - Z.ε • Z'.β) = 0 + abel + · change (0 : ℝ) + 0 = 0 + simp + +/-- The Jacobi identity for Souriau's bracket. -/ +lemma bracket_jacobi (Z Z' Z'' : GalileanAlgebra) : + bracket Z (bracket Z' Z'') + bracket Z' (bracket Z'' Z) + bracket Z'' (bracket Z Z') = 0 := by + apply GalileanAlgebra.ext + · change (bracket Z (bracket Z' Z'')).ω + (bracket Z' (bracket Z'' Z)).ω + + (bracket Z'' (bracket Z Z')).ω = 0 + funext i + fin_cases i <;> simp [bracket, cross_apply, vecHead, vecTail] <;> ring + · change (bracket Z (bracket Z' Z'')).β + (bracket Z' (bracket Z'' Z)).β + + (bracket Z'' (bracket Z Z')).β = 0 + funext i + fin_cases i <;> simp [bracket, cross_apply, vecHead, vecTail] <;> ring + · change (bracket Z (bracket Z' Z'')).γ + (bracket Z' (bracket Z'' Z)).γ + + (bracket Z'' (bracket Z Z')).γ = 0 + funext i + fin_cases i <;> simp [bracket, cross_apply, vecHead, vecTail] <;> ring + · change (0 : ℝ) + 0 + 0 = 0 + simp + +/-- A change of velocity and a space translation commute. -/ +lemma bracket_boost_translation (β γ : ℝ³) : bracket ⟨0, β, 0, 0⟩ ⟨0, 0, γ, 0⟩ = 0 := by + simp [bracket] + rfl + +end GalileanAlgebra + +/-! + +## B. Torsors + +-/ + +/-- A torsor `μ = {l, g, p, E}`, an element of the dual of the Galilean Lie algebra (12.123). -/ +@[ext] +structure GalileanTorsor where + /-- The angular momentum part. -/ + l : ℝ³ + /-- The part paired with the changes of velocity. -/ + g : ℝ³ + /-- The momentum part. -/ + p : ℝ³ + /-- The energy part. -/ + E : ℝ + +/-- The pairing (12.122) of a torsor with an element of the Lie algebra, +`μ(Z) = ⟨l, ω⟩ - ⟨g, β⟩ + ⟨p, γ⟩ - E ε`. -/ +def GalileanTorsor.pair (μ : GalileanTorsor) (Z : GalileanAlgebra) : ℝ := + μ.l ⬝ᵥ Z.ω - μ.g ⬝ᵥ Z.β + μ.p ⬝ᵥ Z.γ - μ.E * Z.ε + +/-! + +## C. The cocycle `f₀` + +-/ + +namespace GalileanAlgebra + +/-- The 2-form `f₀(Z)(Z') = ⟨β, γ'⟩ - ⟨β', γ⟩` of (12.130). -/ +def cocycle (Z Z' : GalileanAlgebra) : ℝ := Z.β ⬝ᵥ Z'.γ - Z'.β ⬝ᵥ Z.γ + +/-- `f₀` is antisymmetric. -/ +lemma cocycle_antisymm (Z Z' : GalileanAlgebra) : cocycle Z Z' = -cocycle Z' Z := by + simp only [cocycle] + ring + +/-- (12.129): `f₀(Z)([Z', Z'']) + f₀(Z')([Z'', Z]) + f₀(Z'')([Z, Z']) = 0`. -/ +lemma cocycle_cyclic (Z Z' Z'' : GalileanAlgebra) : + cocycle Z (bracket Z' Z'') + cocycle Z' (bracket Z'' Z) + cocycle Z'' (bracket Z Z') = 0 := by + rw [cocycle, cocycle, cocycle, add_assoc, bracket, bracket, bracket] + simp only [cross_apply, vec3_dotProduct] + simp only [Fin.isValue, Nat.succ_eq_add_one, Nat.reduceAdd, sub_cons, head_cons, tail_cons, + sub_self, zero_empty, cons_add, empty_add_empty, Pi.sub_apply, cons_val_zero, Pi.smul_apply, + smul_eq_mul, cons_val_one, cons_val] + ring_nf + simp only [vecHead, vecTail] + simp only [Fin.isValue, Pi.smul_apply, smul_eq_mul, Nat.succ_eq_add_one, Nat.reduceAdd, + Function.comp_apply, Fin.succ_zero_eq_one, Fin.succ_one_eq_two] + ring_nf + +/-- `f₀` is not zero: its value on a change of velocity and a space translation along the same +axis is `1`. -/ +lemma cocycle_boost_translation : + cocycle ⟨0, ![1, 0, 0], 0, 0⟩ ⟨0, 0, ![1, 0, 0], 0⟩ = 1 := by + rw [cocycle] + simp + +/-- `M f₀` is a coboundary of the algebra, `M f₀(Z)(Z') = μ₀[Z, Z']` for some torsor `μ₀` +(p. 116, note (1)), if and only if `M = 0`. -/ +lemma smul_cocycle_isCoboundary_iff (M : ℝ) : + (∃ μ₀ : GalileanTorsor, ∀ Z Z' : GalileanAlgebra, M * cocycle Z Z' = μ₀.pair (bracket Z Z')) + ↔ M = 0 := by + constructor + · rintro ⟨μ₀, h⟩ + have h1 := h ⟨0, ![1, 0, 0], 0, 0⟩ ⟨0, 0, ![1, 0, 0], 0⟩ + rw [bracket_boost_translation ![1, 0, 0] ![1, 0, 0]] at h1 + change M * cocycle ⟨0, ![1, 0, 0], 0, 0⟩ ⟨0, 0, ![1, 0, 0], 0⟩ = + μ₀.l ⬝ᵥ 0 - μ₀.g ⬝ᵥ 0 + μ₀.p ⬝ᵥ 0 - μ₀.E * 0 at h1 + simp only [dotProduct, Pi.zero_apply, mul_zero, Finset.sum_const_zero, sub_zero, + add_zero] at h1 + rw [cocycle_boost_translation] at h1 + simpa using h1 + · intro hM + refine ⟨⟨0, 0, 0, 0⟩, fun Z Z' => ?_⟩ + rw [hM, GalileanTorsor.pair] + simp + +/-- `f₀` is not a coboundary of the algebra: no torsor `μ₀` satisfies `f₀(Z)(Z') = μ₀[Z, Z']` for +all `Z`, `Z'`. -/ +lemma cocycle_not_coboundary : + ¬ ∃ μ₀ : GalileanTorsor, ∀ Z Z' : GalileanAlgebra, cocycle Z Z' = μ₀.pair (bracket Z Z') := by + rintro ⟨μ₀, h⟩ + exact one_ne_zero <| (smul_cocycle_isCoboundary_iff 1).mp + ⟨μ₀, fun Z Z' => by rw [one_mul]; exact h Z Z'⟩ + +end GalileanAlgebra + +/-! + +## D. The evolution space of free material points + +-/ + +/-- A point, or a tangent vector, of the evolution space of `N` material points, +`y = (t, r_j, v_j)` (12.76). -/ +@[ext] +structure EvolutionSpace (N : ℕ) where + /-- The time. -/ + t : ℝ + /-- The positions. -/ + r : Fin N → ℝ³ + /-- The velocities. -/ + v : Fin N → ℝ³ + +namespace EvolutionSpace + +variable {N : ℕ} + +instance : Sub (EvolutionSpace N) := ⟨fun y y' => ⟨y.t - y'.t, y.r - y'.r, y.v - y'.v⟩⟩ + +open GalileanAlgebra + +/-- The vector field `Z_V` of `Z` on the evolution space (12.119): `δt = ε`, +`δr_j = ω × r_j + β t + γ`, `δv_j = ω × v_j + β`. -/ +def vectorField (Z : GalileanAlgebra) (y : EvolutionSpace N) : EvolutionSpace N := + ⟨Z.ε, fun j => Z.ω ⨯₃ y.r j + y.t • Z.β + Z.γ, fun j => Z.ω ⨯₃ y.v j + Z.β⟩ + +/-- The differential of the affine vector field `Z_V` (its linear part), applied to a tangent vector +`w`. -/ +def linearPart (Z : GalileanAlgebra) (w : EvolutionSpace N) : EvolutionSpace N := + ⟨0, fun j => Z.ω ⨯₃ w.r j + w.t • Z.β, fun j => Z.ω ⨯₃ w.v j⟩ + +/-- Souriau's bracket is the bracket of the vector fields in the convention (6.12 b), (11.22 a): +`[Z, Z']_V = DZ'_V(Z_V) - DZ_V(Z'_V)`. -/ +lemma vectorField_bracket (Z Z' : GalileanAlgebra) (y : EvolutionSpace N) : + vectorField (bracket Z Z') y + = linearPart Z' (vectorField Z y) - linearPart Z (vectorField Z' y) := by + apply EvolutionSpace.ext + · change (0 : ℝ) = 0 - 0 + simp + · funext j + change (bracket Z Z').ω ⨯₃ y.r j + y.t • (bracket Z Z').β + (bracket Z Z').γ = + (linearPart Z' (vectorField Z y)).r j - (linearPart Z (vectorField Z' y)).r j + funext i + fin_cases i <;> simp [bracket, linearPart, vectorField, cross_apply, vecHead, vecTail] <;> ring + · funext j + change (bracket Z Z').ω ⨯₃ y.v j + (bracket Z Z').β = + (linearPart Z' (vectorField Z y)).v j - (linearPart Z (vectorField Z' y)).v j + funext i + fin_cases i <;> simp [bracket, linearPart, vectorField, cross_apply, vecHead, vecTail] <;> ring + +/-- The Lagrange form of `N` free material points of masses `m j` at `y`, (12.40) with `F_j = 0`: +`σ(dy)(δy) = Σ_j ⟨m_j dv_j, δr_j - v_j δt⟩ - ⟨m_j δv_j, dr_j - v_j dt⟩`. -/ +def lagrangeForm (m : Fin N → ℝ) (y dy δy : EvolutionSpace N) : ℝ := + ∑ j, (m j * (dy.v j ⬝ᵥ (δy.r j - δy.t • y.v j)) - m j * (δy.v j ⬝ᵥ (dy.r j - dy.t • y.v j))) + +/-- `σ` is antisymmetric. -/ +lemma lagrangeForm_antisymm (m : Fin N → ℝ) (y dy δy : EvolutionSpace N) : + lagrangeForm m y dy δy = -lagrangeForm m y δy dy := by + simp [lagrangeForm] + +/-- (12.41)-(12.43): the velocity `(1, v_j, 0)` of the free motion through `y` lies in the kernel +of `σ` (one direction of (12.48)). -/ +lemma lagrangeForm_motion (m : Fin N → ℝ) (y δy : EvolutionSpace N) : + lagrangeForm m y ⟨1, y.v, 0⟩ δy = 0 := by + simp [lagrangeForm] + +/-! + +## E. The moment + +-/ + +/-- The moment of `N` free material points ((12.125) for one point, (12.135) for `N` points): +`l = Σ m_j r_j × v_j`, `g = Σ m_j (r_j - v_j t)`, `p = Σ m_j v_j`, `E = ½ Σ m_j ‖v_j‖²`. -/ +def moment (m : Fin N → ℝ) (y : EvolutionSpace N) : GalileanTorsor := + ⟨∑ j, m j • (y.r j ⨯₃ y.v j), ∑ j, m j • (y.r j - y.t • y.v j), ∑ j, m j • y.v j, + (1 / 2 : ℝ) * ∑ j, m j * (y.v j ⬝ᵥ y.v j)⟩ + +/-- The line `s ↦ y + s dy` of the evolution space. -/ +def line (y dy : EvolutionSpace N) (s : ℝ) : EvolutionSpace N := + ⟨y.t + s * dy.t, fun j => y.r j + s • dy.r j, fun j => y.v j + s • dy.v j⟩ + +/-- The free motion through `y`: `t + s`, `r_j + s v_j`, `v_j`. -/ +def motion (y : EvolutionSpace N) (s : ℝ) : EvolutionSpace N := + ⟨y.t + s, fun j => y.r j + s • y.v j, y.v⟩ + +/-- `μ(Z)` as a sum over the material points. -/ +lemma pair_moment (m : Fin N → ℝ) (y : EvolutionSpace N) (Z : GalileanAlgebra) : + (moment m y).pair Z = ∑ j, m j * ((y.r j ⨯₃ y.v j) ⬝ᵥ Z.ω - (y.r j - y.t • y.v j) ⬝ᵥ Z.β + + y.v j ⬝ᵥ Z.γ - (1 / 2 : ℝ) * Z.ε * (y.v j ⬝ᵥ y.v j)) := by + simp only [GalileanTorsor.pair, moment, sum_dotProduct, smul_dotProduct, smul_eq_mul] + rw [Finset.mul_sum, Finset.sum_mul, ← Finset.sum_sub_distrib, ← Finset.sum_add_distrib, + ← Finset.sum_sub_distrib] + refine Finset.sum_congr rfl (fun j _ => ?_) + ring + +/-- The `j`th term of `μ(Z)` along `y + s dy`, as a polynomial of degree two in `s`. -/ +private lemma pair_term_line (m t dt s : ℝ) (r v dr dv : ℝ³) (Z : GalileanAlgebra) : + m * (((r + s • dr) ⨯₃ (v + s • dv)) ⬝ᵥ Z.ω - ((r + s • dr) - (t + s * dt) • (v + s • dv)) ⬝ᵥ Z.β + + (v + s • dv) ⬝ᵥ Z.γ - (1 / 2 : ℝ) * Z.ε * ((v + s • dv) ⬝ᵥ (v + s • dv))) + = m * ((r ⨯₃ v) ⬝ᵥ Z.ω - (r - t • v) ⬝ᵥ Z.β + v ⬝ᵥ Z.γ - (1 / 2 : ℝ) * Z.ε * (v ⬝ᵥ v)) + + s * (m * (dv ⬝ᵥ ((Z.ω ⨯₃ r + t • Z.β + Z.γ) - Z.ε • v)) + - m * ((Z.ω ⨯₃ v + Z.β) ⬝ᵥ (dr - dt • v))) + + s ^ 2 * (m * ((dr ⨯₃ dv) ⬝ᵥ Z.ω + dt * (dv ⬝ᵥ Z.β) - (1 / 2 : ℝ) * Z.ε * (dv ⬝ᵥ dv))) := by + simp only [dotProduct, Fin.sum_univ_three, cross_apply, Pi.add_apply, Pi.sub_apply, + Pi.smul_apply, smul_eq_mul, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_two, + Matrix.head_cons, Matrix.tail_cons] + ring + +/-- The derivative at `0` of a polynomial of degree two. -/ +private lemma hasDerivAt_quadratic (a b c : ℝ) : + HasDerivAt (fun s : ℝ => a + s * b + s ^ 2 * c) b 0 := by + have h := (((hasDerivAt_id' (0 : ℝ)).mul_const b).const_add a).fun_add + ((hasDerivAt_pow 2 (0 : ℝ)).mul_const c) + simpa using h + +/-- (12.124): `σ(dy)(Z_V(y)) = dμ(Z)(dy)`, stated as the derivative at `s = 0` of +`s ↦ μ(y + s dy)(Z)`; `μ` is a moment of the action (12.120). -/ +lemma hasDerivAt_moment (m : Fin N → ℝ) (y dy : EvolutionSpace N) (Z : GalileanAlgebra) : + HasDerivAt (fun s => (moment m (line y dy s)).pair Z) (lagrangeForm m y dy (vectorField Z y)) + 0 := by + have hfun : (fun s => (moment m (line y dy s)).pair Z) = fun s => ∑ j, + (m j * ((y.r j ⨯₃ y.v j) ⬝ᵥ Z.ω - (y.r j - y.t • y.v j) ⬝ᵥ Z.β + y.v j ⬝ᵥ Z.γ + - (1 / 2 : ℝ) * Z.ε * (y.v j ⬝ᵥ y.v j)) + + s * (m j * (dy.v j ⬝ᵥ ((Z.ω ⨯₃ y.r j + y.t • Z.β + Z.γ) - Z.ε • y.v j)) + - m j * ((Z.ω ⨯₃ y.v j + Z.β) ⬝ᵥ (dy.r j - dy.t • y.v j))) + + s ^ 2 * (m j * ((dy.r j ⨯₃ dy.v j) ⬝ᵥ Z.ω + dy.t * (dy.v j ⬝ᵥ Z.β) + - (1 / 2 : ℝ) * Z.ε * (dy.v j ⬝ᵥ dy.v j)))) := by + funext s + rw [pair_moment] + refine Finset.sum_congr rfl (fun j _ => ?_) + exact pair_term_line (m j) y.t dy.t s (y.r j) (y.v j) (dy.r j) (dy.v j) Z + rw [hfun] + have hL : lagrangeForm m y dy (vectorField Z y) = ∑ j, + (m j * (dy.v j ⬝ᵥ ((Z.ω ⨯₃ y.r j + y.t • Z.β + Z.γ) - Z.ε • y.v j)) + - m j * ((Z.ω ⨯₃ y.v j + Z.β) ⬝ᵥ (dy.r j - dy.t • y.v j))) := rfl + rw [hL] + exact HasDerivAt.fun_sum (fun j _ => hasDerivAt_quadratic _ _ _) + +/-- (12.121): the moment is constant along every free motion. -/ +lemma moment_motion (m : Fin N → ℝ) (y : EvolutionSpace N) (s : ℝ) : + moment m (motion y s) = moment m y := by + simp [moment, motion] + congr + ext j + simp [add_smul] + +/-! + +## F. The cocycle of the system and the mass + +-/ + +/-- The total mass `m = Σ_j m_j` (12.135). -/ +def totalMass (m : Fin N → ℝ) : ℝ := ∑ j, m j + +/-- The centre of gravity `R = (Σ_j m_j r_j) / m` of (12.141). -/ +def centerOfMass (m : Fin N → ℝ) (y : EvolutionSpace N) : ℝ³ := + (totalMass m)⁻¹ • ∑ j, m j • y.r j + +/-- (12.134) with `m = Σ_j m_j` (12.135): `σ(Z_V(y))(Z'_V(y)) = μ[Z, Z'] + m f₀(Z)(Z')`. -/ +lemma lagrangeForm_vectorField (m : Fin N → ℝ) (y : EvolutionSpace N) (Z Z' : GalileanAlgebra) : + lagrangeForm m y (vectorField Z y) (vectorField Z' y) + = (moment m y).pair (bracket Z Z') + totalMass m * cocycle Z Z' := by + simp [lagrangeForm, GalileanTorsor.pair, moment, cocycle, totalMass, bracket, vectorField, + sum_dotProduct, smul_dotProduct, vec3_dotProduct, cross_apply, vecHead, vecTail, + Finset.sum_mul, ← Finset.sum_sub_distrib, ← Finset.sum_add_distrib] + apply Finset.sum_congr rfl + intro j _ + ring + +/-- (12.136) at the level of the algebra: for a non-zero total mass, the cocycle `m f₀` of the +system is not a coboundary of the algebra. -/ +lemma totalMass_cocycle_not_coboundary (m : Fin N → ℝ) (hM : totalMass m ≠ 0) : + ¬ ∃ μ₀ : GalileanTorsor, ∀ Z Z' : GalileanAlgebra, + totalMass m * cocycle Z Z' = μ₀.pair (bracket Z Z') := + fun h => hM ((smul_cocycle_isCoboundary_iff (totalMass m)).mp h) + +/-- (12.141): `g = m R - p t`, with `R` the centre of gravity, for a non-zero total mass. -/ +lemma moment_g (m : Fin N → ℝ) (hM : totalMass m ≠ 0) (y : EvolutionSpace N) : + (moment m y).g = totalMass m • centerOfMass m y - y.t • (moment m y).p := by + simp [moment, smul_sub] + simp only [centerOfMass, Finset.smul_sum] + congr 1 + all_goals simp [← mul_smul, mul_comm] + congr! with i + field_simp [hM] + +/-- (12.141) for free material points: along a free motion the centre of gravity moves uniformly +with velocity `p / m`. -/ +lemma centerOfMass_motion (m : Fin N → ℝ) (y : EvolutionSpace N) (s : ℝ) : + centerOfMass m (motion y s) = centerOfMass m y + s • ((totalMass m)⁻¹ • (moment m y).p) := by + simp [centerOfMass, motion, smul_smul] + simp [moment, mul_smul, Finset.smul_sum, Finset.sum_add_distrib, smul_add] + congr + ext i + simp only [Pi.smul_apply, smul_eq_mul, mul_assoc, mul_comm s] + +end EvolutionSpace + +end ClassicalMechanics From d45d65cf4664727ed160bdb61eecc79e999179f8 Mon Sep 17 00:00:00 2001 From: Philippe Kevorkian Date: Thu, 24 Sep 2026 18:40:57 +0200 Subject: [PATCH 2/3] docs(PhyslibAlpha/ClassicalMechanics): GalileanMass docstrings after a read-back against the book An independent read-back of GalileanMass.lean against the printed pages found no error in the statements and corrects the docstrings: the bracket of vector fields in (6.12 b) is (2.45), the usual Lie bracket of vector fields; only on the matrices (12.74) is Souriau's bracket the opposite of the usual commutator. Physlib's GalileanGroup has rotations in O(3) while Souriau's group (12.73) has them in SO(3). F_j = 0 alone does not give B_j = 0, which is the choice (12.49). Also: p. 151 works at the level of the group, the algebra coboundary is (11.24) with (11.16), (6.13 b), the presymplectic evolution space is (12.114), two more items in what is not formalised, and fuller references. Co-Authored-By: Claude Opus 5.5 --- .../ClassicalMechanics/GalileanMass.lean | 63 ++++++++++++------- 1 file changed, 42 insertions(+), 21 deletions(-) diff --git a/PhyslibAlpha/ClassicalMechanics/GalileanMass.lean b/PhyslibAlpha/ClassicalMechanics/GalileanMass.lean index a86a7b76d..cd848a8f5 100644 --- a/PhyslibAlpha/ClassicalMechanics/GalileanMass.lean +++ b/PhyslibAlpha/ClassicalMechanics/GalileanMass.lean @@ -21,29 +21,44 @@ torsor `μ = {l, g, p, E}` (12.122)-(12.123): `l` is the angular momentum and `p (12.140), and `g = m R - p t` with `R` the centre of gravity (12.141). The Lagrange form `σ` of the system satisfies (12.134), `σ(Z_V(y))(Z'_V(y)) = μ[Z, Z'] + m f₀(Z)(Z')`, where `f₀(Z)(Z') = ⟨β, γ'⟩ - ⟨β', γ⟩` (12.130) and `m = Σ_j m_j` is the total mass (12.135). Souriau -concludes (12.136) that the total mass characterises the cohomology class of the system, and that -this class is never zero. +remarks (12.136) that the total mass can be interpreted as characterising the corresponding +cohomology class of the Galilean group, and that this class is never zero. This file proves these facts at the level of the Lie algebra for `N` free material points in -`ℝ³ = Fin 3 → ℝ` (no forces: `F_j = 0`, hence `E_j = B_j = 0` in (12.44)-(12.45)). An element +`ℝ³ = Fin 3 → ℝ` (no forces, `F_j = 0`; with the choice `B_j = 0` of (12.49), which (12.135) +imposes on an isolated system, (12.44) gives `E_j = 0` and (12.45) reduces to (12.40)). An element `Z = (ω, β, γ, ε)` of the Galilean Lie algebra (12.74), (12.118) is a rotation `ω` (an axial vector), a change of velocity `β`, a space translation `γ` and a time translation `ε`; it acts on the evolution space, whose points are `y = (t, r_j, v_j)` (12.76), by the affine vector field -(12.119). The bracket is Souriau's, `[Z, Z']_V = DZ'_V(Z_V) - DZ_V(Z'_V)` ((6.12 b), (11.22 a)), -opposite to the usual commutator (`EvolutionSpace.vectorField_bracket`). +(12.119). The bracket is Souriau's (6.12 b), `[Z, Z']_V = [Z_V, Z'_V]`, where the bracket of two +vector fields is (2.45), here `DZ'_V(Z_V) - DZ_V(Z'_V)` (`EvolutionSpace.vectorField_bracket`); +this is the usual Lie bracket of vector fields (Mathlib's `VectorField.lieBracket`). The matrices +(12.74) are not formalised; on them this bracket reads `[Z, Z'] = Z'Z - ZZ'`, as in (11.22 a), the +opposite of the usual matrix commutator. What is not formalised here: - the Galilean group itself, its action (12.73), (12.76) and its cocycle `θ₀` (12.126)-(12.128), - hence the passage from the algebra to the group used on p. 151 and in (12.136). The Galilean group - is `GalileanGroup` in `Physlib.SpaceAndTime.GalileanGroup.Basic`; this file works with its Lie - algebra in dimension `3`, in Souriau's parametrisation, and does not link the two; + hence the statement of p. 151 that `θ₀` is not a coboundary of the group (definition (11.19)), + used in (12.136). The algebra-level result of this file implies it, because the derivative of a + group coboundary `Δ(μ₀)` is `μ₀[Z, Z']` (p. 116, note (1)); this implication is not formalised. + Physlib has `GalileanGroup` in `Physlib.SpaceAndTime.GalileanGroup.Basic`, whose rotation part + ranges over the full orthogonal group; Souriau's group (12.73) takes `A ∈ SO(3)` and is + connected (p. 139). Both have the same Lie algebra, with which this file works in dimension `3`, + in Souriau's parametrisation; the file links it to neither group; - `GalileanAlgebra` has no vector space or `LieRing` structure here, only `Zero` and `Add`; the Jacobi identity is proved as an equation; +- that the vector field (12.119), taken as printed, is the derivative (6.11) of the action (12.76); +- the reading of (12.135) as the solution of the system (12.124), (12.134) for a general isolated + system (`B_j = 0`, `Σ_j E_j = 0`, `Σ_j r_j × E_j = 0`): for free points the explicit moment and + `m = Σ_j m_j` are verified, not derived; the uniqueness of `m` in (12.134) follows from + `lagrangeForm_vectorField` and `smul_cocycle_isCoboundary_iff` but is not stated; - the dimension `1` of (12.131), the second half of (12.136) (Hamilton's Lagrangian is not invariant), forces, the converse of (12.48), the invariance of `σ` (12.72), (12.76), and the uniqueness of the moment up to a constant (the constant in `E` is a choice); -- the evolution space is only presymplectic (`EvolutionSpace.lagrangeForm_motion`), so the setting - of `PhyslibAlpha.ClassicalMechanics.MomentMap` is not used; the moment and the cocycle are +- the evolution space is presymplectic, not symplectic (p. 148, (12.114)); + `EvolutionSpace.lagrangeForm_motion` shows that `σ` is degenerate, and `σ` depends on the point + `y` through the velocities. The setting of `PhyslibAlpha.ClassicalMechanics.MomentMap` (a constant + non-degenerate form on a vector space) therefore does not apply; the moment and the cocycle are computed explicitly. ## ii. Key results @@ -72,13 +87,15 @@ What is not formalised here: ## iv. References - J.-M. Souriau, Structure des systèmes dynamiques, Dunod, Paris, 1970: pp. 132-133 - (12.40)-(12.48), pp. 139-140 (12.72)-(12.76), pp. 150-153 (12.118)-(12.141); p. 50 (6.12 b) and - p. 113 (11.22 a) for the bracket; p. 116, note (1), for the coboundaries of the algebra. + (12.40)-(12.49), pp. 139-140 (12.72)-(12.76), p. 148 (12.114), pp. 150-153 (12.118)-(12.141); + p. 27 (2.45), p. 50 (6.12 b) and p. 113 (11.22 a) for the bracket; p. 50 (6.13 b), p. 109 + (11.16), p. 114 (11.24) and p. 116, note (1), for the coboundaries of the algebra. ## References * J.-M. Souriau, *Structure des systèmes dynamiques*, Maîtrises de mathématiques, Dunod, - Paris, 1970, chapter 12, pp. 132-153. The equation numbers refer to this edition. + Paris, 1970: chapter 12, pp. 132-153, and pp. 27, 50, 109, 113-116 for the conventions (2.45), + (6.12), (6.13), (11.16), (11.22), (11.24). The equation numbers refer to this edition. [ref: Souriau1970] -/ @@ -119,7 +136,7 @@ instance : Zero GalileanAlgebra := ⟨⟨0, 0, 0, 0⟩⟩ instance : Add GalileanAlgebra := ⟨fun Z Z' => ⟨Z.ω + Z'.ω, Z.β + Z'.β, Z.γ + Z'.γ, Z.ε + Z'.ε⟩⟩ /-- Souriau's bracket on the Galilean Lie algebra. It is the bracket of the vector fields (12.119) -in the convention (6.12 b), (11.22 a), see `EvolutionSpace.vectorField_bracket`. -/ +in the convention (6.12 b), (2.45), see `EvolutionSpace.vectorField_bracket`. -/ def bracket (Z Z' : GalileanAlgebra) : GalileanAlgebra := ⟨Z'.ω ⨯₃ Z.ω, Z'.ω ⨯₃ Z.β - Z.ω ⨯₃ Z'.β, Z'.ω ⨯₃ Z.γ - Z.ω ⨯₃ Z'.γ + Z.ε • Z'.β - Z'.ε • Z.β, 0⟩ @@ -223,8 +240,9 @@ lemma cocycle_boost_translation : rw [cocycle] simp -/-- `M f₀` is a coboundary of the algebra, `M f₀(Z)(Z') = μ₀[Z, Z']` for some torsor `μ₀` -(p. 116, note (1)), if and only if `M = 0`. -/ +/-- `M f₀` is a coboundary of the algebra, `M f₀(Z)(Z') = μ₀[Z, Z']` for some torsor `μ₀` ((11.24) +with `Z_{g*}(μ) = μ ∘ Ad(Z)` (11.16) and `Ad(Z)(Z') = [Z, Z']` (6.13 b); by p. 116, note (1), this +is also the derivative of the group coboundary `Δ(μ₀)` of (11.19)), if and only if `M = 0`. -/ lemma smul_cocycle_isCoboundary_iff (M : ℝ) : (∃ μ₀ : GalileanTorsor, ∀ Z Z' : GalileanAlgebra, M * cocycle Z Z' = μ₀.pair (bracket Z Z')) ↔ M = 0 := by @@ -288,7 +306,7 @@ def vectorField (Z : GalileanAlgebra) (y : EvolutionSpace N) : EvolutionSpace N def linearPart (Z : GalileanAlgebra) (w : EvolutionSpace N) : EvolutionSpace N := ⟨0, fun j => Z.ω ⨯₃ w.r j + w.t • Z.β, fun j => Z.ω ⨯₃ w.v j⟩ -/-- Souriau's bracket is the bracket of the vector fields in the convention (6.12 b), (11.22 a): +/-- Souriau's bracket is the bracket of the vector fields in the convention (6.12 b), (2.45): `[Z, Z']_V = DZ'_V(Z_V) - DZ_V(Z'_V)`. -/ lemma vectorField_bracket (Z Z' : GalileanAlgebra) (y : EvolutionSpace N) : vectorField (bracket Z Z') y @@ -329,7 +347,8 @@ lemma lagrangeForm_motion (m : Fin N → ℝ) (y δy : EvolutionSpace N) : -/ -/-- The moment of `N` free material points ((12.125) for one point, (12.135) for `N` points): +/-- The moment of `N` free material points ((12.125) for one point of unit mass; (12.135) for `N` +points, with `E_j = 0` in its last line and the additive constant of `E` chosen to be `0`): `l = Σ m_j r_j × v_j`, `g = Σ m_j (r_j - v_j t)`, `p = Σ m_j v_j`, `E = ½ Σ m_j ‖v_j‖²`. -/ def moment (m : Fin N → ℝ) (y : EvolutionSpace N) : GalileanTorsor := ⟨∑ j, m j • (y.r j ⨯₃ y.v j), ∑ j, m j • (y.r j - y.t • y.v j), ∑ j, m j • y.v j, @@ -413,7 +432,8 @@ lemma moment_motion (m : Fin N → ℝ) (y : EvolutionSpace N) (s : ℝ) : /-- The total mass `m = Σ_j m_j` (12.135). -/ def totalMass (m : Fin N → ℝ) : ℝ := ∑ j, m j -/-- The centre of gravity `R = (Σ_j m_j r_j) / m` of (12.141). -/ +/-- The centre of gravity `R = (Σ_j m_j r_j) / m`, named in (12.141) (the formula is the usual one, +not printed there); for `m = 0` the value is `0`, by the convention `0⁻¹ = 0`. -/ def centerOfMass (m : Fin N → ℝ) (y : EvolutionSpace N) : ℝ³ := (totalMass m)⁻¹ • ∑ j, m j • y.r j @@ -445,8 +465,9 @@ lemma moment_g (m : Fin N → ℝ) (hM : totalMass m ≠ 0) (y : EvolutionSpace congr! with i field_simp [hM] -/-- (12.141) for free material points: along a free motion the centre of gravity moves uniformly -with velocity `p / m`. -/ +/-- Along a free motion the centre of gravity moves uniformly with velocity `p / m` (p. 153, after +(12.141)). Souriau deduces this for any isolated system from the constancy of `g` and `p`; here it +is proved directly from the free motion. For `m = 0` both sides are `0`. -/ lemma centerOfMass_motion (m : Fin N → ℝ) (y : EvolutionSpace N) (s : ℝ) : centerOfMass m (motion y s) = centerOfMass m y + s • ((totalMass m)⁻¹ • (moment m y).p) := by simp [centerOfMass, motion, smul_smul] From ae21c037c3869b77d4764d5e4ae388904fdd0ab0 Mon Sep 17 00:00:00 2001 From: Philippe Kevorkian Date: Fri, 25 Sep 2026 11:30:24 +0200 Subject: [PATCH 3/3] refactor(PhyslibAlpha/ClassicalMechanics): move the moment map files into MomentMap/ As agreed in the review of this PR: MomentMap.lean becomes MomentMap/Basic.lean, MomentMapCohomology.lean becomes MomentMap/Cohomology.lean, and GalileanMass.lean moves to MomentMap/GalileanMass.lean. Only the imports and two docstring references to the module name change. Co-Authored-By: Claude Opus 5.5 --- PhyslibAlpha.lean | 6 +++--- .../{MomentMap.lean => MomentMap/Basic.lean} | 0 .../{MomentMapCohomology.lean => MomentMap/Cohomology.lean} | 4 ++-- .../ClassicalMechanics/{ => MomentMap}/GalileanMass.lean | 6 +++--- 4 files changed, 8 insertions(+), 8 deletions(-) rename PhyslibAlpha/ClassicalMechanics/{MomentMap.lean => MomentMap/Basic.lean} (100%) rename PhyslibAlpha/ClassicalMechanics/{MomentMapCohomology.lean => MomentMap/Cohomology.lean} (99%) rename PhyslibAlpha/ClassicalMechanics/{ => MomentMap}/GalileanMass.lean (99%) diff --git a/PhyslibAlpha.lean b/PhyslibAlpha.lean index c3a5ad605..4eb6c1447 100644 --- a/PhyslibAlpha.lean +++ b/PhyslibAlpha.lean @@ -27,9 +27,9 @@ public import PhyslibAlpha.SpaceAndTime.Space.Surfaces.SphericalCylinder public import PhyslibAlpha.SpaceAndTime.Space.Surfaces.SolidCylinder public import PhyslibAlpha.SpaceAndTime.Space.Surfaces.SolidSphere public import PhyslibAlpha.SpaceAndTime.Space.Surfaces.SphericalShell -public import PhyslibAlpha.ClassicalMechanics.GalileanMass -public import PhyslibAlpha.ClassicalMechanics.MomentMap -public import PhyslibAlpha.ClassicalMechanics.MomentMapCohomology +public import PhyslibAlpha.ClassicalMechanics.MomentMap.Basic +public import PhyslibAlpha.ClassicalMechanics.MomentMap.Cohomology +public import PhyslibAlpha.ClassicalMechanics.MomentMap.GalileanMass public import PhyslibAlpha.ClassicalMechanics.NortonDome.Basic public import PhyslibAlpha.ClassicalMechanics.NortonDome.Determinism public import PhyslibAlpha.ClassicalMechanics.NortonDome.NewtonianSystem diff --git a/PhyslibAlpha/ClassicalMechanics/MomentMap.lean b/PhyslibAlpha/ClassicalMechanics/MomentMap/Basic.lean similarity index 100% rename from PhyslibAlpha/ClassicalMechanics/MomentMap.lean rename to PhyslibAlpha/ClassicalMechanics/MomentMap/Basic.lean diff --git a/PhyslibAlpha/ClassicalMechanics/MomentMapCohomology.lean b/PhyslibAlpha/ClassicalMechanics/MomentMap/Cohomology.lean similarity index 99% rename from PhyslibAlpha/ClassicalMechanics/MomentMapCohomology.lean rename to PhyslibAlpha/ClassicalMechanics/MomentMap/Cohomology.lean index f8c53914c..34c0f3dba 100644 --- a/PhyslibAlpha/ClassicalMechanics/MomentMapCohomology.lean +++ b/PhyslibAlpha/ClassicalMechanics/MomentMap/Cohomology.lean @@ -5,7 +5,7 @@ Authors: Philippe Kevorkian -/ module -public import PhyslibAlpha.ClassicalMechanics.MomentMap +public import PhyslibAlpha.ClassicalMechanics.MomentMap.Basic public import Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree /-! @@ -25,7 +25,7 @@ group `Sp(E) ⋉ E` of a real symplectic vector space `E`, acting by `x ↦ B x `moment` of (11.7): the defect `θ(a)` does not depend on `x` and equals `μ(C)` (a computation here, not a consequence of connectedness), `θ` is a 1-cocycle of the coadjoint action, its derivative at the identity along a curve is the Lie algebra cocycle of -`PhyslibAlpha.ClassicalMechanics.MomentMap`, and its cohomology class is not zero. It does NOT +`PhyslibAlpha.ClassicalMechanics.MomentMap.Basic`, and its cohomology class is not zero. It does NOT prove (11.18), (11.20) or (11.21): by (11.21) the non-zero class means that no potential of `σ` is invariant under this group, but that implication is Souriau's and is not formalised here. diff --git a/PhyslibAlpha/ClassicalMechanics/GalileanMass.lean b/PhyslibAlpha/ClassicalMechanics/MomentMap/GalileanMass.lean similarity index 99% rename from PhyslibAlpha/ClassicalMechanics/GalileanMass.lean rename to PhyslibAlpha/ClassicalMechanics/MomentMap/GalileanMass.lean index cd848a8f5..50baaccfa 100644 --- a/PhyslibAlpha/ClassicalMechanics/GalileanMass.lean +++ b/PhyslibAlpha/ClassicalMechanics/MomentMap/GalileanMass.lean @@ -57,9 +57,9 @@ What is not formalised here: uniqueness of the moment up to a constant (the constant in `E` is a choice); - the evolution space is presymplectic, not symplectic (p. 148, (12.114)); `EvolutionSpace.lagrangeForm_motion` shows that `σ` is degenerate, and `σ` depends on the point - `y` through the velocities. The setting of `PhyslibAlpha.ClassicalMechanics.MomentMap` (a constant - non-degenerate form on a vector space) therefore does not apply; the moment and the cocycle are - computed explicitly. + `y` through the velocities. The setting of `PhyslibAlpha.ClassicalMechanics.MomentMap.Basic` + (a constant non-degenerate form on a vector space) therefore does not apply; the moment and the + cocycle are computed explicitly. ## ii. Key results