Incorrect documentation for Galilean action on space in `actSpace`

⚠️ Found by a local LLM, not a human. This was flagged by an automated documentation-mistake finder (qwen3:14b) and passed 10/10 independent verification runs before filing, but it has not been reviewed by a person. Please check it's a genuine error before acting on it.

Summary

The documentation in Physlib/SpaceAndTime/GalileanGroup/Basic.lean (around line 161) is incorrect.

Current text

-- The Galilean action on space at a fixed time.

Why this is wrong

The docstring for actSpace claims the Galilean action operates "on space at a fixed time," but this is incorrect. The function actSpace explicitly takes a t : Time parameter, indicating the transformation depends on the specified time. This aligns with the active convention (t, x) ↦ (t + b, R x + v t + a) defined in the module's documentation.

The error arises because the docstring contradicts the function's actual implementation, which uses t to compute the spatial component of the transformation. The correction accurately reflects that the action depends on the provided time parameter t, as seen in the definition of actSpace. This ensures the documentation matches the mathematical behavior of Galilean transformations.

Suggested correction

-- The Galilean action on space, which depends on the given time `t`.

Open Physlib/SpaceAndTime/GalileanGroup/Basic.lean around line 161 and inspect the actSpace definition alongside its docstring. Confirm how the given time parameter affects the spatial action, then update the documentation so it matches that behavior. Done when the docstring no longer says the action is at a fixed time.