From 56486e53c2be6cac2d85c77bb5adc28eb5ecefbd Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Wed, 1 Jul 2026 14:42:19 +0100 Subject: [PATCH 1/2] auto-task(exists_boost_mul_rotation): prove restricted Lorentz elements are a boost times a rotation Co-authored-by: Claude --- Physlib/Relativity/LorentzGroup/Restricted/Basic.lean | 3 --- .../LorentzGroup/Restricted/FromBoostRotation.lean | 10 ++++++++++ 2 files changed, 10 insertions(+), 3 deletions(-) diff --git a/Physlib/Relativity/LorentzGroup/Restricted/Basic.lean b/Physlib/Relativity/LorentzGroup/Restricted/Basic.lean index f42a69c9a..4cd482383 100644 --- a/Physlib/Relativity/LorentzGroup/Restricted/Basic.lean +++ b/Physlib/Relativity/LorentzGroup/Restricted/Basic.lean @@ -16,9 +16,6 @@ This file is currently a stub. @[expose] public section -TODO "Prove that every member of the restricted Lorentz group is - combination of a boost and a rotation." - namespace LorentzGroup open Matrix diff --git a/Physlib/Relativity/LorentzGroup/Restricted/FromBoostRotation.lean b/Physlib/Relativity/LorentzGroup/Restricted/FromBoostRotation.lean index 83ca99d28..552aaf38f 100644 --- a/Physlib/Relativity/LorentzGroup/Restricted/FromBoostRotation.lean +++ b/Physlib/Relativity/LorentzGroup/Restricted/FromBoostRotation.lean @@ -102,6 +102,16 @@ def toBoostRotation {d} : LorentzGroup.restricted d ≃ₜ Lorentz.Velocity d × continuous_toFun := by fun_prop continuous_invFun := by fun_prop +/-- Every element of the restricted Lorentz group can be written as a product of a + generalized boost and a rotation. -/ +theorem exists_boost_mul_rotation {d} (Λ : LorentzGroup.restricted d) : + ∃ (v : Lorentz.Velocity d) (R : Rotations d), + (Λ : LorentzGroup d) = generalizedBoost 0 v * (R : LorentzGroup d) := by + refine ⟨toVelocity Λ, toRotation Λ, ?_⟩ + have h : (toRotation Λ : LorentzGroup d) = + (generalizedBoost 0 (toVelocity Λ))⁻¹ * (Λ : LorentzGroup d) := rfl + rw [h, mul_inv_cancel_left] + end LorentzGroup end From 99e81b3764d698a31850912c8ad7df05bd58f94e Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Fri, 3 Jul 2026 05:41:27 +0100 Subject: [PATCH 2/2] Update Physlib/Relativity/LorentzGroup/Restricted/FromBoostRotation.lean Co-authored-by: Gregory Loges --- .../LorentzGroup/Restricted/FromBoostRotation.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/Physlib/Relativity/LorentzGroup/Restricted/FromBoostRotation.lean b/Physlib/Relativity/LorentzGroup/Restricted/FromBoostRotation.lean index 552aaf38f..f9688ad8e 100644 --- a/Physlib/Relativity/LorentzGroup/Restricted/FromBoostRotation.lean +++ b/Physlib/Relativity/LorentzGroup/Restricted/FromBoostRotation.lean @@ -107,10 +107,8 @@ def toBoostRotation {d} : LorentzGroup.restricted d ≃ₜ Lorentz.Velocity d × theorem exists_boost_mul_rotation {d} (Λ : LorentzGroup.restricted d) : ∃ (v : Lorentz.Velocity d) (R : Rotations d), (Λ : LorentzGroup d) = generalizedBoost 0 v * (R : LorentzGroup d) := by - refine ⟨toVelocity Λ, toRotation Λ, ?_⟩ - have h : (toRotation Λ : LorentzGroup d) = - (generalizedBoost 0 (toVelocity Λ))⁻¹ * (Λ : LorentzGroup d) := rfl - rw [h, mul_inv_cancel_left] + have h : toRotation Λ = (generalizedBoost 0 (toVelocity Λ))⁻¹ * Λ := rfl + exact ⟨toVelocity Λ, toRotation Λ, by rw [h, mul_inv_cancel_left]⟩ end LorentzGroup