The Euclidean Action and the Action of the Group of Rotations

[LibertasSpZ]

"Addresses item 5 of Issue #854 (the action of the group of rotations).

• Adds Physlib/SpaceAndTime/Space/Origin.lean (new file):
  -- instance : Zero (Space d), Space.zero_val, Space.zero_apply — the origin (the vector-space zero) and its projection lemmas, moved here from Module.lean.
  -- Space.chartEuclidean, Space.chartEuclidean_apply — the standard chart Space d ≃ᵃⁱ[ℝ] EuclideanSpace ℝ (Fin d), p ↦ p -ᵥ 0.

• Adds Physlib/SpaceAndTime/Space/EuclideanGroup/Action.lean (new file):
  -- Space.origin, Space.origin_apply — coordinate basepoint and its projection.
  -- instance : MulAction (EuclideanGroup d) (Space d) — the Euclidean action.
  -- EuclideanGroup.smul_apply — coordinate formula.
  -- EuclideanGroup.smul_vsub_smul — displacements transform by the linear part.
  -- EuclideanGroup.dist_smul — the action is by isometries.
  -- EuclideanGroup.rotation_smul_eq — restriction to RotationGroup action (r • p = ↑r • p).
  -- EuclideanGroup.rotation_smul_origin — rotations fix the 0.
  -- EuclideanGroup.rotation_smul_vsub_origin — rotations act about the origin 0 by their orthogonal part.
  -- EuclideanGroup.rotation_dist_smul — rotations preserve distance.
  -- EuclideanGroup.chartEuclidean_smul — the chart and the bridge to toAffineIsometryMulEquiv (optional; rest of file doesn't depend on it).

• Physlib/SpaceAndTime/Space/Module.lean (modified):
  -- Removed instance : Zero (Space d), Space.zero_val, Space.zero_apply — moved to Origin.lean; Module now sources them via its import …Origin.

Reading order: Part 1 (Euclidean action) → Part 2 (rotation specialization) → Part 3 (optional affine-isometry bridge), top to bottom.

Substantive AI usage (document setup, some statements, filling in some proofs; Claude Opus 4.8). All AI-generated content is human-reviewed and believed correct. No bibliographic references.

[github-actions]

Thank you for this PR, which will now be reviewed.
If submitting to ./Physlib or ./QuantumInfo, please
see our review guidelines
if you are not familiar with the process. You should expect a back and forth
with a reviewer before your PR is merged. See also that link for how to
add appropriate labels to your PR. The PR will also go through a number
of automated checks. You can learn more about these here,
including how to run them locally.

If you are submitting to ./PhyslibAlpha there will be a lighter review process,
though your PR must still pass the automated checks.

If you want to bring attention to this PR, please write a message on this
thread of the Lean Zulip.

[jstoobysmith]

Maybe it is worth doing the following here:

In Space.Module we have an instance of Zero on Space. This essentially defines the origin in the same way you have it defined here. However, I understand that we don't want to import the whole module structure on Space here. So should we make a file .../Space/Origin.lean which has that instance of a zero so we don't need to define it both here and there?

In it we could also include Space.chartEuclidean etc.

[LibertasSpZ]

Thanks, Joseph.

• Factored origin and chartEuclidean into Space/Origin.lean (imported by Space/EuclideanGroup/Action.lean).
• Kept the Module's Zero instance and added origin_eq_zero : Space.origin d = 0 (by rfl) in Module.lean, so the two are pinned definitionally equal.
• Updated the inventory above.

Happy to further edit if you'd prefer. Thanks!

[jstoobysmith]

I think I would get rid of origin completely. and in ./Space/Origin move the instance of the zero and just used zero in the Action.lean file. The idea of the zero is that it is a choice of origin, so the two concepts here are the same so it doesn't make sense (to me) to have two separate definitions for it.

[LibertasSpZ]

That makes sense. Done — moved the Zero instance (and zero_val/zero_apply) into Space/Origin.lean, dropped the separate origin, and Action.lean now uses 0 directly. Module sources its zero from the import Origin."

[jstoobysmith]

Would remove the The unification bridge from this, but otherwise this looks good.

[jstoobysmith]

Approved - this now looks good to me.