auto-task(exists_boost_mul_rotation): prove restricted Lorentz elements are a boost times a rotation

[jstoobysmith]

Summary

Completes the TODO in Physlib/Relativity/LorentzGroup/Restricted/Basic.lean:

TODO "Prove that every member of the restricted Lorentz group is combination of a boost and a rotation."

The homeomorphism LorentzGroup.toBoostRotation in
Physlib/Relativity/LorentzGroup/Restricted/FromBoostRotation.lean already
provides the boost–rotation decomposition; its file docstring states that the
inverse "writes elements of the restricted Lorentz group as a product of a
generalized boost and a rotation". This PR turns that into an explicit,
user-facing existence theorem and removes the now-satisfied TODO note.

Changes

• Added LorentzGroup.exists_boost_mul_rotation to FromBoostRotation.lean:
  for every Λ : LorentzGroup.restricted d there exist a velocity
  v : Lorentz.Velocity d and a rotation R : Rotations d with
  (Λ : LorentzGroup d) = generalizedBoost 0 v * (R : LorentzGroup d).
  The proof uses the existing toVelocity/toRotation maps and
  mul_inv_cancel_left.
• Removed the corresponding TODO "..." marker from
  Restricted/Basic.lean.

How to review

1. Read the new theorem exists_boost_mul_rotation; confirm its statement
   says every restricted Lorentz element equals a generalized boost times a
   rotation, and that it builds with no sorry.
2. Confirm the TODO "Prove that every member of the restricted Lorentz group is combination of a boost and a rotation." note is gone from
   Restricted/Basic.lean.
3. lake build (project builds green; the theorem depends only on
   propext, Classical.choice, Quot.sound — no new axioms).

[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.

Important: If a reviewer adds an awaiting-author label to your PR, once you have addressed the review comments, please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

[gloges]

Looks good to me. Just a minor suggested change to halve the proof length.