From 5327840e2d973c9547908d826bde8cf92d335d8c Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Tue, 24 Feb 2026 21:13:51 -0800
Subject: [PATCH 1/4] feat(Generalized): prove
 generalizedBoost_timeComponent_eq

---
 .../LorentzGroup/Boosts/Generalized.lean      | 26 ++++++++++---------
 1 file changed, 14 insertions(+), 12 deletions(-)

diff --git a/PhysLean/Relativity/LorentzGroup/Boosts/Generalized.lean b/PhysLean/Relativity/LorentzGroup/Boosts/Generalized.lean
index 92e1ea67b..7b0b1e359 100644
--- a/PhysLean/Relativity/LorentzGroup/Boosts/Generalized.lean
+++ b/PhysLean/Relativity/LorentzGroup/Boosts/Generalized.lean
@@ -451,25 +451,27 @@ lemma generalizedBoost_inv (u v : Velocity d) :
   · simp
   simp [minkowskiProduct_symm]
 
-/--
-The time component of a generalised boost is equal to
-```
-1 +
-    ‖u.1.timeComponent • v.1.spatialPart - v.1.timeComponent • u.1.spatialPart‖ / (1 + ⟪u.1, v.1⟫ₘ)
-```
+/-- The time component of a generalised boost.
 
 A proof of this result can be found at the below link:
 https://leanprover.zulipchat.com/#narrow/channel/479953-PhysLean/topic/Lorentz.20group/near/523249684
-
-Note that the declaration of this semiformal result will be similar once
-the TODO item `FXQ45` is completed.
 -/
-@[sorryful]
 lemma generalizedBoost_timeComponent_eq (u v : Velocity d) :
     (generalizedBoost u v).1 (Sum.inl 0) (Sum.inl 0) = 1 +
     ‖u.1.timeComponent • v.1.spatialPart -
-      v.1.timeComponent • u.1.spatialPart‖ / (1 + ⟪u.1, v.1⟫ₘ) := by
-  sorry
+      v.1.timeComponent • u.1.spatialPart‖ ^ 2 / (1 + ⟪u.1, v.1⟫ₘ) := by
+  rw [generalizedBoost_apply_eq_toCoord]
+  simp only [Matrix.one_apply_eq, inl_0_inl_0, one_mul]
+  have h1 := Velocity.one_add_minkowskiProduct_ne_zero u v
+  rw [norm_sub_sq_real, norm_smul, norm_smul, Real.norm_eq_abs, Real.norm_eq_abs,
+    Velocity.timeComponent_abs u, Velocity.timeComponent_abs v,
+    real_inner_smul_left, real_inner_smul_right]
+  simp only [timeComponent, minkowskiProduct_eq_timeComponent_spatialPart] at *
+  field_simp [h1]
+  nlinarith [mul_pow (u.1 (Sum.inl 0)) (‖v.1.spatialPart‖) 2,
+             mul_pow (v.1 (Sum.inl 0)) (‖u.1.spatialPart‖) 2,
+             Velocity.norm_spatialPart_sq_eq u, Velocity.norm_spatialPart_sq_eq v,
+             real_inner_comm (u.1.spatialPart) (v.1.spatialPart)]
 
 end LorentzGroup
 

From 8895c5003c2336d78ede4d328539e1ae656ff695 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Tue, 24 Feb 2026 23:41:25 -0800
Subject: [PATCH 2/4] Update Generalized.lean

Co-authored-by: Daniel Morrison <39346894+morrison-daniel@users.noreply.github.com>
---
 PhysLean/Relativity/LorentzGroup/Boosts/Generalized.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/PhysLean/Relativity/LorentzGroup/Boosts/Generalized.lean b/PhysLean/Relativity/LorentzGroup/Boosts/Generalized.lean
index 7b0b1e359..a4e96381f 100644
--- a/PhysLean/Relativity/LorentzGroup/Boosts/Generalized.lean
+++ b/PhysLean/Relativity/LorentzGroup/Boosts/Generalized.lean
@@ -462,12 +462,11 @@ lemma generalizedBoost_timeComponent_eq (u v : Velocity d) :
       v.1.timeComponent • u.1.spatialPart‖ ^ 2 / (1 + ⟪u.1, v.1⟫ₘ) := by
   rw [generalizedBoost_apply_eq_toCoord]
   simp only [Matrix.one_apply_eq, inl_0_inl_0, one_mul]
-  have h1 := Velocity.one_add_minkowskiProduct_ne_zero u v
   rw [norm_sub_sq_real, norm_smul, norm_smul, Real.norm_eq_abs, Real.norm_eq_abs,
     Velocity.timeComponent_abs u, Velocity.timeComponent_abs v,
     real_inner_smul_left, real_inner_smul_right]
   simp only [timeComponent, minkowskiProduct_eq_timeComponent_spatialPart] at *
-  field_simp [h1]
+  field_simp [Velocity.one_add_minkowskiProduct_ne_zero u v]
   nlinarith [mul_pow (u.1 (Sum.inl 0)) (‖v.1.spatialPart‖) 2,
              mul_pow (v.1 (Sum.inl 0)) (‖u.1.spatialPart‖) 2,
              Velocity.norm_spatialPart_sq_eq u, Velocity.norm_spatialPart_sq_eq v,

From 1e39cdbd735e9bd8cc68b1120bbe1b2a17621d8b Mon Sep 17 00:00:00 2001
From: Daniel Morrison <39346894+morrison-daniel@users.noreply.github.com>
Date: Fri, 27 Feb 2026 14:48:47 -0800
Subject: [PATCH 3/4] Fix what my suggestion broke

---
 PhysLean/Relativity/LorentzGroup/Boosts/Generalized.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/PhysLean/Relativity/LorentzGroup/Boosts/Generalized.lean b/PhysLean/Relativity/LorentzGroup/Boosts/Generalized.lean
index a4e96381f..8f07114ed 100644
--- a/PhysLean/Relativity/LorentzGroup/Boosts/Generalized.lean
+++ b/PhysLean/Relativity/LorentzGroup/Boosts/Generalized.lean
@@ -470,7 +470,8 @@ lemma generalizedBoost_timeComponent_eq (u v : Velocity d) :
   nlinarith [mul_pow (u.1 (Sum.inl 0)) (‖v.1.spatialPart‖) 2,
              mul_pow (v.1 (Sum.inl 0)) (‖u.1.spatialPart‖) 2,
              Velocity.norm_spatialPart_sq_eq u, Velocity.norm_spatialPart_sq_eq v,
-             real_inner_comm (u.1.spatialPart) (v.1.spatialPart)]
+             real_inner_comm (u.1.spatialPart) (v.1.spatialPart),
+             Velocity.one_add_minkowskiProduct_ne_zero u v]
 
 end LorentzGroup
 

From 0b106c5de823fee857becbfd327ad2080c234133 Mon Sep 17 00:00:00 2001
From: Daniel Morrison <39346894+morrison-daniel@users.noreply.github.com>
Date: Fri, 27 Feb 2026 15:25:45 -0800
Subject: [PATCH 4/4] Revert changes

---
 PhysLean/Relativity/LorentzGroup/Boosts/Generalized.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/PhysLean/Relativity/LorentzGroup/Boosts/Generalized.lean b/PhysLean/Relativity/LorentzGroup/Boosts/Generalized.lean
index 8f07114ed..193ce93b3 100644
--- a/PhysLean/Relativity/LorentzGroup/Boosts/Generalized.lean
+++ b/PhysLean/Relativity/LorentzGroup/Boosts/Generalized.lean
@@ -462,16 +462,16 @@ lemma generalizedBoost_timeComponent_eq (u v : Velocity d) :
       v.1.timeComponent • u.1.spatialPart‖ ^ 2 / (1 + ⟪u.1, v.1⟫ₘ) := by
   rw [generalizedBoost_apply_eq_toCoord]
   simp only [Matrix.one_apply_eq, inl_0_inl_0, one_mul]
+  have h := Velocity.one_add_minkowskiProduct_ne_zero u v
   rw [norm_sub_sq_real, norm_smul, norm_smul, Real.norm_eq_abs, Real.norm_eq_abs,
     Velocity.timeComponent_abs u, Velocity.timeComponent_abs v,
     real_inner_smul_left, real_inner_smul_right]
   simp only [timeComponent, minkowskiProduct_eq_timeComponent_spatialPart] at *
-  field_simp [Velocity.one_add_minkowskiProduct_ne_zero u v]
+  field_simp [h]
   nlinarith [mul_pow (u.1 (Sum.inl 0)) (‖v.1.spatialPart‖) 2,
              mul_pow (v.1 (Sum.inl 0)) (‖u.1.spatialPart‖) 2,
              Velocity.norm_spatialPart_sq_eq u, Velocity.norm_spatialPart_sq_eq v,
-             real_inner_comm (u.1.spatialPart) (v.1.spatialPart),
-             Velocity.one_add_minkowskiProduct_ne_zero u v]
+             real_inner_comm (u.1.spatialPart) (v.1.spatialPart)]
 
 end LorentzGroup