refactor: Large refactor of Lorentz vecs

2024-11-08 16:24:58 +00:00 · 2024-11-08 16:24:58 +00:00 · 3eb5da875f
commit 3eb5da875f
parent a69cf91919
8 changed files with 402 additions and 88 deletions
--- a/HepLean/SpaceTime/LorentzGroup/Basic.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Basic.lean
@ -85,28 +85,6 @@ lemma dual_mem (h : Λ ∈ LorentzGroup d) : dual Λ ∈ LorentzGroup d := by
  rw [mem_iff_dual_mul_self, dual_dual]
  exact mem_iff_self_mul_dual.mp h

-/-
-lemma mem_iff_norm : Λ ∈ LorentzGroup d ↔
-    ∀ (x : LorentzVector d), ⟪Λ *ᵥ x, Λ *ᵥ x⟫ₘ = ⟪x, x⟫ₘ := by
-  refine Iff.intro (fun h x => h x x) (fun h x y => ?_)
-  have hp := h (x + y)
-  have hn := h (x - y)
-  rw [mulVec_add] at hp
-  rw [mulVec_sub] at hn
-  simp only [map_add, LinearMap.add_apply, map_sub, LinearMap.sub_apply] at hp hn
-  rw [symm (Λ *ᵥ y) (Λ *ᵥ x), symm y x] at hp hn
-  linear_combination hp / 4 + -1 * hn / 4
-
-lemma mem_iff_on_right : Λ ∈ LorentzGroup d ↔
-    ∀ (x y : LorentzVector d), ⟪x, (dual Λ * Λ) *ᵥ y⟫ₘ = ⟪x, y⟫ₘ := by
-  refine Iff.intro (fun h x y ↦ ?_) (fun h x y ↦ ?_)
-  · have h1 := h x y
-    rw [← dual_mulVec_right, mulVec_mulVec] at h1
-    exact h1
-  · rw [← dual_mulVec_right, mulVec_mulVec]
-    exact h x y
-
-/

 end LorentzGroup

--- a/HepLean/SpaceTime/LorentzGroup/Boosts.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Boosts.lean
@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.SpaceTime.LorentzGroup.Proper
 import Mathlib.Topology.Constructions
-import HepLean.SpaceTime.LorentzVector.NormOne
+import HepLean.SpaceTime.LorentzVector.Real.NormOne
 /-!
 # Boosts

@ -27,41 +27,67 @@ noncomputable section

 namespace LorentzGroup

-open NormOneLorentzVector
-open minkowskiMetric
+open Lorentz.Contr.NormOne
+open Lorentz
+open TensorProduct

 variable {d : ℕ}

 /-- An auxillary linear map used in the definition of a generalised boost. -/
-def genBoostAux₁ (u v : FuturePointing d) : LorentzVector d →ₗ[ℝ] LorentzVector d where
-  toFun x := (2 * ⟪x, u⟫ₘ) • v.1.1
+def genBoostAux₁ (u v : FuturePointing d) : ContrMod d →ₗ[ℝ] ContrMod d where
+  toFun x := (2 * toField d ⟪x, u.val.val⟫ₘ) • v.1.1
  map_add' x y := by
-    simp only [map_add, LinearMap.add_apply]
-    rw [mul_add, add_smul]
+    simp [map_add, LinearMap.add_apply, tmul_add, add_tmul, mul_add, add_smul]
  map_smul' c x := by
-    simp only [LinearMapClass.map_smul, LinearMap.smul_apply, smul_eq_mul,
-      RingHom.id_apply]
+    simp only [toField, Action.instMonoidalCategory_tensorObj_V,
+      Action.instMonoidalCategory_tensorUnit_V, CategoryTheory.Equivalence.symm_inverse,
+      Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
+      smul_tmul, tmul_smul, map_smul, smul_eq_mul, RingHom.id_apply]
+    erw [LinearMap.id_apply]
    rw [← mul_assoc, mul_comm 2 c, mul_assoc, mul_smul]
+    rfl

 /-- An auxillary linear map used in the definition of a genearlised boost. -/
-def genBoostAux₂ (u v : FuturePointing d) : LorentzVector d →ₗ[ℝ] LorentzVector d where
-  toFun x := - (⟪x, u.1.1 + v⟫ₘ / (1 + ⟪u.1.1, v⟫ₘ)) • (u.1.1 + v)
+def genBoostAux₂ (u v : FuturePointing d) : ContrMod d →ₗ[ℝ] ContrMod d where
+  toFun x := - (toField d ⟪x, u.1.1 + v.1.1⟫ₘ / (1 + toField d ⟪u.1.1, v.1.1⟫ₘ)) • (u.1.1 + v.1.1)
  map_add' x y := by
    simp only
    rw [← add_smul]
    apply congrFun (congrArg _ _)
-    field_simp
+    field_simp [add_tmul]
    apply congrFun (congrArg _ _)
    ring
  map_smul' c x := by
-    simp only
-    rw [map_smul, show (c • minkowskiMetric x) (↑u + ↑v) = c * minkowskiMetric x (u+v) from rfl,
-      mul_div_assoc, neg_mul_eq_mul_neg, smul_smul]
+    simp only [smul_tmul, tmul_smul]
+    rw [map_smul]
+    conv =>
+      lhs; lhs; rhs; lhs
+      change (c * toField d (contrContrContract.hom (x ⊗ₜ[ℝ] (u.val.val + v.val.val))))
+    rw [mul_div_assoc, neg_mul_eq_mul_neg, smul_smul]
    rfl

+lemma genBoostAux₂_self (u : FuturePointing d) : genBoostAux₂ u u = - genBoostAux₁ u u := by
+  ext1 x
+  simp only [genBoostAux₂, LinearMap.coe_mk, AddHom.coe_mk, genBoostAux₁, LinearMap.neg_apply]
+  rw [neg_smul]
+  apply congrArg
+  conv => lhs; rhs; rw [← (two_smul ℝ u.val.val)]
+  rw [smul_smul]
+  congr 1
+  rw [u.1.2]
+  simp [toField]
+  conv => lhs; lhs; rhs; rhs; change 1
+  rw [show 1 + (1 : ℝ) = (2 : ℝ ) by ring]
+  simp only [isUnit_iff_ne_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true,
+    IsUnit.div_mul_cancel]
+  rw [← (two_smul ℝ u.val.val)]
+  simp only [tmul_smul, map_smul, smul_eq_mul]
+  rfl
+
+
 /-- An generalised boost. This is a Lorentz transformation which takes the four velocity `u`
 to `v`. -/
-def genBoost (u v : FuturePointing d) : LorentzVector d →ₗ[ℝ] LorentzVector d :=
+def genBoost (u v : FuturePointing d) : ContrMod d →ₗ[ℝ] ContrMod d :=
  LinearMap.id + genBoostAux₁ u v + genBoostAux₂ u v

 namespace genBoost
@ -73,26 +99,26 @@ namespace genBoost
 lemma self (u : FuturePointing d) : genBoost u u = LinearMap.id := by
  ext x
  simp only [genBoost, LinearMap.add_apply, LinearMap.id_coe, id_eq]
-  rw [add_assoc, add_right_eq_self, add_eq_zero_iff_eq_neg, genBoostAux₁, genBoostAux₂]
-  simp only [LinearMap.coe_mk, AddHom.coe_mk, map_add, smul_add, neg_smul, neg_add_rev, neg_neg]
-  rw [← add_smul]
-  apply congrFun (congrArg _ _)
-  rw [u.1.2]
-  ring
+  rw [genBoostAux₂_self]
+  simp only [LinearMap.neg_apply, add_neg_cancel_right]

 /-- A generalised boost as a matrix. -/
 def toMatrix (u v : FuturePointing d) : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ :=
-  LinearMap.toMatrix LorentzVector.stdBasis LorentzVector.stdBasis (genBoost u v)
+  LinearMap.toMatrix ContrMod.stdBasis ContrMod.stdBasis (genBoost u v)

-lemma toMatrix_mulVec (u v : FuturePointing d) (x : LorentzVector d) :
-    (toMatrix u v).mulVec x = genBoost u v x :=
-  LinearMap.toMatrix_mulVec_repr LorentzVector.stdBasis LorentzVector.stdBasis (genBoost u v) x
+lemma toMatrix_mulVec (u v : FuturePointing d) (x : Contr d) :
+    (toMatrix u v) *ᵥ x = genBoost u v x :=
+  ContrMod.ext (LinearMap.toMatrix_mulVec_repr ContrMod.stdBasis ContrMod.stdBasis (genBoost u v) x)

 open minkowskiMatrix LorentzVector in
@[simp]
 lemma toMatrix_apply (u v : FuturePointing d) (μ ν : Fin 1 ⊕ Fin d) :
-    (toMatrix u v) μ ν = η μ μ * (⟪e μ, e ν⟫ₘ + 2 * ⟪e ν, u⟫ₘ * ⟪e μ, v⟫ₘ
-    - ⟪e μ, u + v⟫ₘ * ⟪e ν, u + v⟫ₘ / (1 + ⟪u, v.1.1⟫ₘ)) := by
+    (toMatrix u v) μ ν = η μ μ * (toField d ⟪ContrMod.stdBasis μ, ContrMod.stdBasis ν⟫ₘ + 2 *
+     toField d ⟪ContrMod.stdBasis ν, u.val.val⟫ₘ * toField d  ⟪ContrMod.stdBasis μ, v.val.val⟫ₘ
+    - toField d  ⟪ContrMod.stdBasis μ, u.val.val + v.val.val⟫ₘ *
+    toField d  ⟪ContrMod.stdBasis ν, u.val.val + v.val.val⟫ₘ /
+    (1 + toField d  ⟪u.val.val, v.val.val⟫ₘ)) := by
+  sorry
  rw [matrix_apply_stdBasis (toMatrix u v) μ ν, toMatrix_mulVec]
  simp only [genBoost, genBoostAux₁, genBoostAux₂, map_add, smul_add, neg_smul, LinearMap.add_apply,
    LinearMap.id_apply, LinearMap.coe_mk, AddHom.coe_mk, basis_left, map_smul, smul_eq_mul, map_neg,
--- a/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean
@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.SpaceTime.LorentzVector.NormOne
+import HepLean.SpaceTime.LorentzVector.Real.NormOne
 import HepLean.SpaceTime.LorentzGroup.Proper
 /-!
 # The Orthochronous Lorentz Group
@ -25,45 +25,35 @@ namespace LorentzGroup
 variable {d : ℕ}
 variable (Λ : LorentzGroup d)
 open LorentzVector
-open minkowskiMetric
+open Lorentz.Contr

 /-- A Lorentz transformation is `orthochronous` if its `0 0` element is non-negative. -/
-def IsOrthochronous : Prop := 0 ≤ timeComp Λ
+def IsOrthochronous : Prop := 0 ≤ Λ.1 (Sum.inl 0) (Sum.inl 0)

 lemma IsOrthochronous_iff_futurePointing :
-    IsOrthochronous Λ ↔ (toNormOneLorentzVector Λ) ∈ NormOneLorentzVector.FuturePointing d := by
-  simp only [IsOrthochronous, timeComp_eq_toNormOneLorentzVector]
-  rw [NormOneLorentzVector.FuturePointing.mem_iff_time_nonneg]
+    IsOrthochronous Λ ↔ toNormOne Λ ∈ NormOne.FuturePointing d := by
+  simp only [IsOrthochronous]
+  rw [NormOne.FuturePointing.mem_iff_inl_nonneg, toNormOne_inl]

 lemma IsOrthochronous_iff_transpose :
    IsOrthochronous Λ ↔ IsOrthochronous (transpose Λ) := by rfl

 lemma IsOrthochronous_iff_ge_one :
-    IsOrthochronous Λ ↔ 1 ≤ timeComp Λ := by
-  rw [IsOrthochronous_iff_futurePointing, NormOneLorentzVector.FuturePointing.mem_iff,
-    NormOneLorentzVector.time_pos_iff]
-  simp only [time, toNormOneLorentzVector, timeVec, Fin.isValue]
-  erw [Pi.basisFun_apply, Matrix.mulVec_single_one]
-  rfl
+    IsOrthochronous Λ ↔ 1 ≤ Λ.1 (Sum.inl 0) (Sum.inl 0) := by
+  rw [IsOrthochronous_iff_futurePointing, NormOne.FuturePointing.mem_iff_inl_one_le_inl,
+    toNormOne_inl]

 lemma not_orthochronous_iff_le_neg_one :
-    ¬ IsOrthochronous Λ ↔ timeComp Λ ≤ -1 := by
-  rw [timeComp, IsOrthochronous_iff_futurePointing, NormOneLorentzVector.FuturePointing.not_mem_iff,
-    NormOneLorentzVector.time_nonpos_iff]
-  simp only [time, toNormOneLorentzVector, timeVec, Fin.isValue]
-  erw [Pi.basisFun_apply, Matrix.mulVec_single_one]
-  rfl
+    ¬ IsOrthochronous Λ ↔ Λ.1 (Sum.inl 0) (Sum.inl 0) ≤ -1 := by
+  rw [IsOrthochronous_iff_futurePointing, NormOne.FuturePointing.not_mem_iff_inl_le_neg_one,
+    toNormOne_inl]

-lemma not_orthochronous_iff_le_zero :
-    ¬ IsOrthochronous Λ ↔ timeComp Λ ≤ 0 := by
-  refine Iff.intro (fun h => ?_) (fun h => ?_)
-  · rw [not_orthochronous_iff_le_neg_one] at h
-    linarith
-  · rw [IsOrthochronous_iff_ge_one]
-    linarith
+lemma not_orthochronous_iff_le_zero : ¬ IsOrthochronous Λ ↔ Λ.1 (Sum.inl 0) (Sum.inl 0) ≤ 0 := by
+  rw [IsOrthochronous_iff_futurePointing, NormOne.FuturePointing.not_mem_iff_inl_le_zero,
+    toNormOne_inl]

 /-- The continuous map taking a Lorentz transformation to its `0 0` element. -/
-def timeCompCont : C(LorentzGroup d, ℝ) := ⟨fun Λ => timeComp Λ,
+def timeCompCont : C(LorentzGroup d, ℝ) := ⟨fun Λ => Λ.1 (Sum.inl 0) (Sum.inl 0),
    Continuous.matrix_elem (continuous_iff_le_induced.mpr fun _ a => a) (Sum.inl 0) (Sum.inl 0)⟩

 /-- An auxillary function used in the definition of `orthchroMapReal`. -/
@ -89,7 +79,7 @@ def orthchroMapReal : C(LorentzGroup d, ℝ) := ContinuousMap.comp

 lemma orthchroMapReal_on_IsOrthochronous {Λ : LorentzGroup d} (h : IsOrthochronous Λ) :
    orthchroMapReal Λ = 1 := by
-  rw [IsOrthochronous_iff_ge_one, timeComp] at h
+  rw [IsOrthochronous_iff_ge_one] at h
  change stepFunction (Λ.1 _ _) = 1
  rw [stepFunction, if_pos h, if_neg]
  linarith
@ -97,8 +87,9 @@ lemma orthchroMapReal_on_IsOrthochronous {Λ : LorentzGroup d} (h : IsOrthochron
 lemma orthchroMapReal_on_not_IsOrthochronous {Λ : LorentzGroup d} (h : ¬ IsOrthochronous Λ) :
    orthchroMapReal Λ = - 1 := by
  rw [not_orthochronous_iff_le_neg_one] at h
-  change stepFunction (timeComp _)= - 1
-  rw [stepFunction, if_pos h]
+  change stepFunction (_)= - 1
+  rw [stepFunction, if_pos]
+  exact h

 lemma orthchroMapReal_minus_one_or_one (Λ : LorentzGroup d) :
    orthchroMapReal Λ = -1 ∨ orthchroMapReal Λ = 1 := by
@ -130,29 +121,29 @@ lemma mul_othchron_of_othchron_othchron {Λ Λ' : LorentzGroup d} (h : IsOrthoch
    (h' : IsOrthochronous Λ') : IsOrthochronous (Λ * Λ') := by
  rw [IsOrthochronous_iff_transpose] at h
  rw [IsOrthochronous_iff_futurePointing] at h h'
-  rw [IsOrthochronous, timeComp_mul]
-  exact NormOneLorentzVector.FuturePointing.metric_reflect_mem_mem h h'
+  rw [IsOrthochronous, LorentzGroup.inl_inl_mul]
+  exact NormOne.FuturePointing.metric_reflect_mem_mem h h'

 lemma mul_othchron_of_not_othchron_not_othchron {Λ Λ' : LorentzGroup d} (h : ¬ IsOrthochronous Λ)
    (h' : ¬ IsOrthochronous Λ') : IsOrthochronous (Λ * Λ') := by
  rw [IsOrthochronous_iff_transpose] at h
  rw [IsOrthochronous_iff_futurePointing] at h h'
-  rw [IsOrthochronous, timeComp_mul]
-  exact NormOneLorentzVector.FuturePointing.metric_reflect_not_mem_not_mem h h'
+  rw [IsOrthochronous, LorentzGroup.inl_inl_mul]
+  exact NormOne.FuturePointing.metric_reflect_not_mem_not_mem h h'

 lemma mul_not_othchron_of_othchron_not_othchron {Λ Λ' : LorentzGroup d} (h : IsOrthochronous Λ)
    (h' : ¬ IsOrthochronous Λ') : ¬ IsOrthochronous (Λ * Λ') := by
-  rw [not_orthochronous_iff_le_zero, timeComp_mul]
+  rw [not_orthochronous_iff_le_zero, LorentzGroup.inl_inl_mul]
  rw [IsOrthochronous_iff_transpose] at h
  rw [IsOrthochronous_iff_futurePointing] at h h'
-  exact NormOneLorentzVector.FuturePointing.metric_reflect_mem_not_mem h h'
+  exact NormOne.FuturePointing.metric_reflect_mem_not_mem h h'

 lemma mul_not_othchron_of_not_othchron_othchron {Λ Λ' : LorentzGroup d} (h : ¬ IsOrthochronous Λ)
    (h' : IsOrthochronous Λ') : ¬ IsOrthochronous (Λ * Λ') := by
-  rw [not_orthochronous_iff_le_zero, timeComp_mul]
+  rw [not_orthochronous_iff_le_zero, LorentzGroup.inl_inl_mul]
  rw [IsOrthochronous_iff_transpose] at h
  rw [IsOrthochronous_iff_futurePointing] at h h'
-  exact NormOneLorentzVector.FuturePointing.metric_reflect_not_mem_mem h h'
+  exact NormOne.FuturePointing.metric_reflect_not_mem_mem h h'

 /-- The homomorphism from `LorentzGroup` to `ℤ₂` whose kernel are the Orthochronous elements. -/
 def orthchroRep : LorentzGroup d →* ℤ₂ where
--- a/HepLean/SpaceTime/LorentzVector/Real/Basic.lean
+++ b/HepLean/SpaceTime/LorentzVector/Real/Basic.lean
@ -30,10 +30,18 @@ open minkowskiMatrix
  Lorentz vectors. In index notation these have an up index `ψⁱ`. -/
 def Contr (d : ℕ) : Rep ℝ (LorentzGroup d) := Rep.of ContrMod.rep

+instance : TopologicalSpace (Contr d) :=
+  haveI : NormedAddCommGroup (Contr d) := ContrMod.norm
+  UniformSpace.toTopologicalSpace
+
 /-- The representation of `LorentzGroup d` on real vectors corresponding to covariant
  Lorentz vectors. In index notation these have an up index `ψⁱ`. -/
 def Co (d : ℕ) : Rep ℝ (LorentzGroup d) := Rep.of CoMod.rep

+open CategoryTheory.MonoidalCategory
+
+def toField (d : ℕ) : (𝟙_ (Rep ℝ ↑(LorentzGroup d))) →ₗ[ℝ] ℝ := LinearMap.id
+
 /-!

 ## Isomorphism between contravariant and covariant Lorentz vectors
--- a/HepLean/SpaceTime/LorentzVector/Real/Contraction.lean
+++ b/HepLean/SpaceTime/LorentzVector/Real/Contraction.lean
@ -183,6 +183,17 @@ namespace contrContrContract

 variable (x y : Contr d)

+@[simp]
+lemma action_tmul (g : LorentzGroup d) : ⟪(Contr d).ρ g x, (Contr d).ρ g y⟫ₘ = ⟪x, y⟫ₘ := by
+  conv =>
+    lhs
+    change (CategoryTheory.CategoryStruct.comp
+      ((CategoryTheory.MonoidalCategory.tensorObj (Contr d) (Contr d)).ρ g)
+      contrContrContract.hom) (x ⊗ₜ[ℝ] y)
+    arg 1
+    apply contrContrContract.comm g
+  rfl
+
 lemma as_sum : ⟪x, y⟫ₘ = x.val (Sum.inl 0) * y.val (Sum.inl 0) -
      ∑ i, x.val (Sum.inr i) * y.val (Sum.inr i)  := by
  rw [contrContrContract_hom_tmul]
@ -191,6 +202,26 @@ lemma as_sum : ⟪x, y⟫ₘ = x.val (Sum.inl 0) * y.val (Sum.inl 0) -
    one_mul, Finset.sum_singleton, Sum.elim_inr, neg_mul, mul_neg, Finset.sum_neg_distrib]
  rfl

+open InnerProductSpace
+
+lemma as_sum_toSpace : ⟪x, y⟫ₘ = x.val (Sum.inl 0) * y.val (Sum.inl 0) -
+    ⟪x.toSpace, y.toSpace⟫_ℝ := by
+  rw [as_sum]
+  rfl
+
+@[simp]
+lemma stdBasis_inl {d : ℕ} :
+    ⟪@ContrMod.stdBasis d (Sum.inl 0), ContrMod.stdBasis (Sum.inl 0)⟫ₘ = (1 : ℝ) := by
+  rw [as_sum]
+  trans (1 : ℝ) - (0 : ℝ)
+  congr
+  · rw [ContrMod.stdBasis_apply_same]
+    simp
+  · rw [Fintype.sum_eq_zero]
+    intro a
+    simp
+  · ring
+
 lemma symm : ⟪x, y⟫ₘ = ⟪y, x⟫ₘ := by
  rw [as_sum, as_sum]
  congr 1
@ -316,6 +347,39 @@ lemma _root_.LorentzGroup.mem_iff_norm : Λ ∈ LorentzGroup d ↔
    Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
    Action.FunctorCategoryEquivalence.functor_obj_obj, add_sub_cancel, neg_add_cancel, e]

+/-!
+
+## Some equalities and inequalities
+
+-/
+
+lemma inl_sq_eq (v : Contr d) : v.val (Sum.inl 0) ^ 2 =
+    (toField d ⟪v, v⟫ₘ) + ∑ i, v.val (Sum.inr i) ^ 2:= by
+  rw [as_sum]
+  apply sub_eq_iff_eq_add.mp
+  congr
+  · exact pow_two (v.val (Sum.inl 0))
+  · funext i
+    exact pow_two (v.val (Sum.inr i))
+
+lemma le_inl_sq (v : Contr d) : toField d ⟪v, v⟫ₘ ≤ v.val (Sum.inl 0) ^ 2 := by
+  rw [inl_sq_eq]
+  apply (le_add_iff_nonneg_right _).mpr
+  refine Fintype.sum_nonneg ?hf
+  exact fun i => pow_two_nonneg (v.val (Sum.inr i))
+
+
+lemma ge_abs_inner_product (v w : Contr d) : v.val (Sum.inl 0)  * w.val (Sum.inl 0)  -
+    ‖⟪v.toSpace, w.toSpace⟫_ℝ‖ ≤ ⟪v, w⟫ₘ := by
+  rw [as_sum_toSpace, sub_le_sub_iff_left]
+  exact Real.le_norm_self ⟪v.toSpace, w.toSpace⟫_ℝ
+
+lemma ge_sub_norm  (v w : Contr d) : v.val (Sum.inl 0)  * w.val (Sum.inl 0) -
+    ‖v.toSpace‖ * ‖w.toSpace‖ ≤ ⟪v, w⟫ₘ := by
+  apply le_trans _ (ge_abs_inner_product v w)
+  rw [sub_le_sub_iff_left]
+  exact norm_inner_le_norm v.toSpace w.toSpace
+
 end contrContrContract

 end Lorentz
--- a/HepLean/SpaceTime/LorentzVector/Real/Modules.lean
+++ b/HepLean/SpaceTime/LorentzVector/Real/Modules.lean
@ -93,6 +93,10 @@ lemma stdBasis_toFin1dℝEquiv_apply_same (μ : Fin 1 ⊕ Fin d) :
  rw [@LinearEquiv.apply_symm_apply]
  exact Pi.single_eq_same μ 1

+@[simp]
+lemma stdBasis_apply_same (μ : Fin 1 ⊕ Fin d) : (stdBasis μ).val μ = 1 :=
+  stdBasis_toFin1dℝEquiv_apply_same μ
+
 lemma stdBasis_toFin1dℝEquiv_apply_ne {μ ν : Fin 1 ⊕ Fin d} (h : μ ≠ ν) :
    toFin1dℝEquiv (stdBasis μ) ν = 0 := by
  simp only [stdBasis, Basis.ofEquivFun, Basis.coe_ofRepr, LinearEquiv.trans_symm,
@ -100,6 +104,11 @@ lemma stdBasis_toFin1dℝEquiv_apply_ne {μ ν : Fin 1 ⊕ Fin d} (h : μ ≠ ν
  rw [@LinearEquiv.apply_symm_apply]
  exact Pi.single_eq_of_ne' h 1

+@[simp]
+lemma stdBasis_inl_apply_inr (i : Fin d) : (stdBasis (Sum.inl 0)).val (Sum.inr i) = 0 := by
+  refine stdBasis_toFin1dℝEquiv_apply_ne ?_
+  simp
+
 /-- Decomposition of a contrvariant Lorentz vector into the standard basis. -/
 lemma stdBasis_decomp (v : ContrMod d) : v = ∑ i, v.toFin1dℝ i • stdBasis i := by
  apply toFin1dℝEquiv.injective
@ -151,6 +160,22 @@ lemma mulVec_mulVec (M N : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ) (v :

 /-!

+## The norm
+
+(Not the Minkowski norm, but the norm of a vector in `ContrℝModule d`.)
+-/
+
+def norm : NormedAddCommGroup (ContrMod d) where
+  norm v := ‖v.val‖₊
+  dist_self x := Pi.normedAddCommGroup.dist_self x.val
+  dist_triangle x y z := Pi.normedAddCommGroup.dist_triangle x.val y.val z.val
+  dist_comm x y := Pi.normedAddCommGroup.dist_comm x.val y.val
+  eq_of_dist_eq_zero {x y} := fun h => ext (MetricSpace.eq_of_dist_eq_zero h)
+
+def toSpace (v : ContrMod d) : EuclideanSpace ℝ (Fin d) := v.val ∘ Sum.inr
+
+/-!
+
 ## The representation.

 -/
@ -230,6 +255,10 @@ lemma stdBasis_toFin1dℝEquiv_apply_same (μ : Fin 1 ⊕ Fin d) :
  rw [@LinearEquiv.apply_symm_apply]
  exact Pi.single_eq_same μ 1

+@[simp]
+lemma stdBasis_apply_same (μ : Fin 1 ⊕ Fin d) : (stdBasis μ).val μ = 1 :=
+  stdBasis_toFin1dℝEquiv_apply_same μ
+
 lemma stdBasis_toFin1dℝEquiv_apply_ne {μ ν : Fin 1 ⊕ Fin d} (h : μ ≠ ν) :
    toFin1dℝEquiv (stdBasis μ) ν = 0 := by
  simp only [stdBasis, Basis.ofEquivFun, Basis.coe_ofRepr, LinearEquiv.trans_symm,
--- a/HepLean/SpaceTime/LorentzVector/Real/NormOne.lean
+++ b/HepLean/SpaceTime/LorentzVector/Real/NormOne.lean
@ -0,0 +1,218 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.SpaceTime.LorentzVector.Real.Contraction
+import Mathlib.GroupTheory.GroupAction.Blocks
+/-!
+
+# Lorentz vectors with norm one
+
+-/
+
+open TensorProduct
+
+namespace Lorentz
+
+namespace Contr
+
+variable {d : ℕ}
+
+/-- The set of Lorentz vectors with norm 1. -/
+def NormOne (d : ℕ) : Set (Contr d) := fun v => ⟪v, v⟫ₘ = (1 : ℝ)
+
+noncomputable  section
+
+namespace NormOne
+
+lemma mem_iff {v : Contr d} : v ∈ NormOne d ↔ ⟪v, v⟫ₘ = (1 : ℝ) := by
+  rfl
+
+lemma mem_mulAction (g : LorentzGroup d) (v : Contr d) :
+    v ∈ NormOne d ↔ (Contr d).ρ g v ∈ NormOne d := by
+  rw [mem_iff, mem_iff, contrContrContract.action_tmul]
+
+instance : TopologicalSpace (NormOne d) := instTopologicalSpaceSubtype
+
+variable (v w : NormOne d)
+
+/-- The negative of a `NormOne` as a `NormOne`. -/
+def neg : NormOne d := ⟨- v, by
+  rw [mem_iff]
+  simp only [Action.instMonoidalCategory_tensorUnit_V, Action.instMonoidalCategory_tensorObj_V,
+    CategoryTheory.Equivalence.symm_inverse, Action.functorCategoryEquivalence_functor,
+    Action.FunctorCategoryEquivalence.functor_obj_obj, tmul_neg, neg_tmul, neg_neg]
+  exact v.2⟩
+
+/-- The first column of a Lorentz matrix as a `NormOneLorentzVector`. -/
+@[simps!]
+def _root_.LorentzGroup.toNormOne (Λ : LorentzGroup d) : NormOne d :=
+  ⟨(Contr d).ρ Λ (ContrMod.stdBasis (Sum.inl 0)), by
+    rw [mem_iff, contrContrContract.action_tmul, contrContrContract.stdBasis_inl]⟩
+
+lemma _root_.LorentzGroup.toNormOne_inl (Λ : LorentzGroup d) :
+    (LorentzGroup.toNormOne Λ).val.val (Sum.inl 0) = Λ.1 (Sum.inl 0) (Sum.inl 0) := by
+  simp only [Fin.isValue, LorentzGroup.toNormOne_coe_val, Finsupp.single, one_ne_zero, ↓reduceIte,
+    Finsupp.coe_mk, Matrix.mulVec_single, mul_one]
+
+lemma _root_.LorentzGroup.toNormOne_inr (Λ : LorentzGroup d) (i : Fin d) :
+    (LorentzGroup.toNormOne Λ).val.val (Sum.inr i) = Λ.1 (Sum.inr i) (Sum.inl 0) := by
+  simp only [LorentzGroup.toNormOne_coe_val, Finsupp.single, one_ne_zero, ↓reduceIte, Fin.isValue,
+    Finsupp.coe_mk, Matrix.mulVec_single, mul_one]
+
+lemma _root_.LorentzGroup.inl_inl_mul (Λ Λ' : LorentzGroup d) : (Λ * Λ').1 (Sum.inl 0) (Sum.inl 0) =
+    ⟪(LorentzGroup.toNormOne (LorentzGroup.transpose Λ)).1,
+      (Contr d).ρ LorentzGroup.parity (LorentzGroup.toNormOne Λ').1⟫ₘ := by
+  rw [contrContrContract.right_parity]
+  simp  only [Fin.isValue, lorentzGroupIsGroup_mul_coe, Matrix.mul_apply, Fintype.sum_sum_type,
+    Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton,
+    LorentzGroup.transpose, PiLp.inner_apply, Function.comp_apply,
+    RCLike.inner_apply, conj_trivial]
+  congr
+  · rw [LorentzGroup.toNormOne_inl]
+    rfl
+  · rw [LorentzGroup.toNormOne_inl]
+  · funext x
+    rw [LorentzGroup.toNormOne_inr, LorentzGroup.toNormOne_inr]
+    rfl
+
+lemma inl_sq : v.val.val (Sum.inl 0) ^ 2 = 1 + ‖ContrMod.toSpace v.val‖ ^ 2  := by
+  rw [contrContrContract.inl_sq_eq, v.2]
+  congr
+  rw [← real_inner_self_eq_norm_sq]
+  simp only [PiLp.inner_apply, RCLike.inner_apply, conj_trivial]
+  congr
+  funext x
+  exact pow_two ((v.val).val (Sum.inr x))
+
+lemma one_le_abs_inl : 1 ≤ |v.val.val (Sum.inl 0)| := by
+  have h1 := contrContrContract.le_inl_sq v.val
+  rw [v.2] at h1
+  exact (one_le_sq_iff_one_le_abs _).mp h1
+
+lemma inl_le_neg_one_or_one_le_inl : v.val.val (Sum.inl 0) ≤ -1 ∨ 1 ≤ v.val.val (Sum.inl 0) :=
+  le_abs'.mp (one_le_abs_inl v)
+
+lemma norm_space_le_abs_inl : ‖v.1.toSpace‖ < |v.val.val (Sum.inl 0)| := by
+  rw [(abs_norm _).symm, ← @sq_lt_sq, inl_sq]
+  change  ‖ContrMod.toSpace v.val‖ ^ 2 < 1 + ‖ContrMod.toSpace v.val‖ ^ 2
+  exact lt_one_add (‖(v.1).toSpace‖ ^ 2)
+
+lemma norm_space_leq_abs_inl : ‖v.1.toSpace‖ ≤ |v.val.val (Sum.inl 0)| :=
+  le_of_lt (norm_space_le_abs_inl v)
+
+lemma inl_abs_sub_space_norm :
+    0 ≤ |v.val.val (Sum.inl 0)| * |w.val.val (Sum.inl 0)| - ‖v.1.toSpace‖  * ‖w.1.toSpace‖ := by
+  apply sub_nonneg.mpr
+  apply mul_le_mul (norm_space_leq_abs_inl v) (norm_space_leq_abs_inl w) ?_ ?_
+  · exact norm_nonneg _
+  · exact abs_nonneg _
+
+/-!
+
+# Future pointing norm one Lorentz vectors
+
+-/
+
+/-- The future pointing Lorentz vectors with Norm one. -/
+def FuturePointing (d : ℕ) : Set (NormOne d) :=
+  fun x => 0 < x.val.val (Sum.inl 0)
+
+namespace FuturePointing
+
+lemma mem_iff : v ∈ FuturePointing d ↔ 0 < v.val.val (Sum.inl 0) := by
+  rfl
+
+lemma mem_iff_inl_nonneg : v ∈ FuturePointing d ↔ 0 ≤ v.val.val (Sum.inl 0) := by
+  refine Iff.intro (fun h => le_of_lt h) (fun h => ?_)
+  rw [mem_iff]
+  rcases inl_le_neg_one_or_one_le_inl v with (h | h)
+  · linarith
+  · linarith
+
+lemma mem_iff_inl_one_le_inl : v ∈ FuturePointing d ↔ 1 ≤ v.val.val (Sum.inl 0) := by
+  rw [mem_iff_inl_nonneg]
+  refine Iff.intro (fun h => ?_) (fun h => ?_)
+  · rcases inl_le_neg_one_or_one_le_inl v with (h | h)
+    · linarith
+    · linarith
+  · linarith
+
+lemma mem_iff_parity_mem : v ∈ FuturePointing d ↔ ⟨(Contr d).ρ LorentzGroup.parity v.1,
+    (NormOne.mem_mulAction _ _).mp v.2⟩ ∈ FuturePointing d := by
+  rw [mem_iff, mem_iff]
+  change _ ↔ 0 < (minkowskiMatrix.mulVec v.val.val) (Sum.inl 0)
+  simp only [Fin.isValue, minkowskiMatrix.mulVec_inl_0]
+
+
+lemma not_mem_iff_inl_le_zero : v ∉ FuturePointing d ↔ v.val.val (Sum.inl 0) ≤ 0 := by
+  rw [mem_iff]
+  simp
+
+lemma not_mem_iff_inl_lt_zero : v ∉ FuturePointing d ↔ v.val.val (Sum.inl 0) < 0 := by
+  rw [mem_iff_inl_nonneg]
+  simp
+
+lemma not_mem_iff_inl_le_neg_one : v ∉ FuturePointing d ↔ v.val.val (Sum.inl 0) ≤ -1 := by
+  rw [not_mem_iff_inl_le_zero]
+  refine Iff.intro (fun h => ?_) (fun h => ?_)
+  · rcases inl_le_neg_one_or_one_le_inl v with (h | h)
+    · linarith
+    · linarith
+  · linarith
+
+lemma not_mem_iff_neg : v ∉ FuturePointing d ↔ neg v ∈ FuturePointing d := by
+  rw [not_mem_iff_inl_le_zero, mem_iff_inl_nonneg]
+  simp only [Fin.isValue, neg]
+  change (v).val.val (Sum.inl 0) ≤ 0 ↔ 0 ≤ - (v.val).val (Sum.inl 0)
+  simp
+
+variable (f f' : FuturePointing d)
+
+lemma inl_nonneg : 0 ≤ f.val.val.val (Sum.inl 0):= le_of_lt f.2
+
+lemma abs_inl : |f.val.val.val (Sum.inl 0)| = f.val.val.val (Sum.inl 0) :=
+  abs_of_nonneg (inl_nonneg f)
+
+open InnerProductSpace
+lemma metric_nonneg : 0 ≤ toField d ⟪f.1.1, f'.1.1⟫ₘ := by
+  apply le_trans (inl_abs_sub_space_norm f f'.1)
+  rw [abs_inl f, abs_inl f']
+  exact contrContrContract.ge_sub_norm f.1.1 f'.1.1
+
+variable {v w : NormOne d}
+
+lemma metric_reflect_mem_mem (h : v ∈ FuturePointing d) (hw : w ∈ FuturePointing d) :
+    0 ≤ toField d ⟪v.val, (Contr d).ρ LorentzGroup.parity w.1⟫ₘ :=
+  metric_nonneg ⟨v, h⟩ ⟨⟨(Contr d).ρ LorentzGroup.parity w.1,
+    (NormOne.mem_mulAction _ _).mp w.2⟩, (mem_iff_parity_mem w).mp hw⟩
+
+lemma metric_reflect_not_mem_not_mem (h : v ∉ FuturePointing d) (hw : w ∉ FuturePointing d) :
+    0 ≤ toField d ⟪v.val, (Contr d).ρ LorentzGroup.parity w.1⟫ₘ := by
+  have h1 := metric_reflect_mem_mem ((not_mem_iff_neg v).mp h) ((not_mem_iff_neg w).mp hw)
+  apply le_of_le_of_eq h1 ?_
+  simp [neg, neg_tmul, tmul_neg]
+
+lemma metric_reflect_mem_not_mem (h : v ∈ FuturePointing d) (hw : w ∉ FuturePointing d) :
+   toField d ⟪v.val, (Contr d).ρ LorentzGroup.parity w.1⟫ₘ ≤ 0 := by
+  rw [show (0 : ℝ) = - 0 from zero_eq_neg.mpr rfl, le_neg]
+  have h1 := metric_reflect_mem_mem h ((not_mem_iff_neg w).mp hw)
+  apply le_of_le_of_eq h1 ?_
+  simp [neg, neg_tmul, tmul_neg]
+
+lemma metric_reflect_not_mem_mem (h : v ∉ FuturePointing d) (hw : w ∈ FuturePointing d) :
+    toField d ⟪v.val, (Contr d).ρ LorentzGroup.parity w.1⟫ₘ ≤ 0 := by
+  rw [show (0 : ℝ) = - 0 from zero_eq_neg.mpr rfl, le_neg]
+  have h1 := metric_reflect_mem_mem ((not_mem_iff_neg v).mp h) hw
+  apply le_of_le_of_eq h1 ?_
+  simp [neg, neg_tmul, tmul_neg]
+
+end FuturePointing
+
+end NormOne
+
+end
+
+end Contr
+end Lorentz
--- a/HepLean/SpaceTime/MinkowskiMetric.lean
+++ b/HepLean/SpaceTime/MinkowskiMetric.lean
@ -178,7 +178,7 @@ lemma dual_mulVec_left : ⟪(dual Λ) *ᵥ x, y⟫ₘ = ⟪x, Λ *ᵥ y⟫ₘ :=
 lemma matrix_apply_eq_iff_sub : ⟪v, Λ *ᵥ w⟫ₘ = ⟪v, Λ' *ᵥ w⟫ₘ ↔ ⟪v, (Λ - Λ') *ᵥ w⟫ₘ = 0 := by
  rw [← sub_eq_zero, ← LinearMap.map_sub, sub_mulVec]

-lemma matrix_eq_iff_eq_forall' : (∀ v, Λ *ᵥ v= Λ' *ᵥ v) ↔ ∀ w v, ⟪v, Λ *ᵥ w⟫ₘ = ⟪v, Λ' *ᵥ w⟫ₘ := by
+lemma matrix_eq_iff_eq_forall' : (∀ v, Λ *ᵥ v = Λ' *ᵥ v) ↔ ∀ w v, ⟪v, Λ *ᵥ w⟫ₘ = ⟪v, Λ' *ᵥ w⟫ₘ := by
  refine Iff.intro (fun h ↦ fun w v ↦ ?_) (fun h ↦ fun v ↦ ?_)
  · rw [h w]
  · simp only [matrix_apply_eq_iff_sub] at h