From 2425c09e876d74bc37168a8287eea173202fe5bb Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sat, 8 Jun 2024 01:50:31 +0200 Subject: [PATCH 1/9] Update Basic.lean --- HepLean/AnomalyCancellation/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/HepLean/AnomalyCancellation/Basic.lean b/HepLean/AnomalyCancellation/Basic.lean index c609025..e49b345 100644 --- a/HepLean/AnomalyCancellation/Basic.lean +++ b/HepLean/AnomalyCancellation/Basic.lean @@ -87,7 +87,7 @@ lemma LinSols.ext {χ : ACCSystemLinear} {S T : χ.LinSols} (h : S.val = T.val) simp_all only /-- An instance providing the operations and properties for `LinSols` to form an - addative commutative monoid. -/ + additive commutative monoid. -/ @[simps!] instance linSolsAddCommMonoid (χ : ACCSystemLinear) : AddCommMonoid χ.LinSols where From 984e6f85d4110909b4284d535f41650ea1878205 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sat, 8 Jun 2024 01:50:33 +0200 Subject: [PATCH 2/9] Update LinearMaps.lean --- HepLean/AnomalyCancellation/LinearMaps.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/HepLean/AnomalyCancellation/LinearMaps.lean b/HepLean/AnomalyCancellation/LinearMaps.lean index f917b4c..3ed0bb8 100644 --- a/HepLean/AnomalyCancellation/LinearMaps.lean +++ b/HepLean/AnomalyCancellation/LinearMaps.lean @@ -9,7 +9,7 @@ import Mathlib.Algebra.BigOperators.Fin /-! # Linear maps -Some definitions and properites of linear, bilinear, and trilinear maps, along with homogeneous +Some definitions and properties of linear, bilinear, and trilinear maps, along with homogeneous quadratic and cubic equations. ## TODO @@ -62,7 +62,7 @@ instance instFun (V : Type) [AddCommMonoid V] [Module ℚ V] : cases g simp_all -/-- The construction of a symmetric bilinear map from smul and map_add in the first factor, +/-- The construction of a symmetric bilinear map from `smul` and `map_add` in the first factor, and swap. -/ @[simps!] def mk₂ (f : V × V → ℚ) (map_smul : ∀ a S T, f (a • S, T) = a * f (S, T)) @@ -196,7 +196,7 @@ instance instFun : FunLike (TriLinearSymm V) V (V →ₗ[ℚ] V →ₗ[ℚ] ℚ cases g simp_all -/-- The construction of a symmetric trilinear map from smul and map_add in the first factor, +/-- The construction of a symmetric trilinear map from `smul` and `map_add` in the first factor, and two swap. -/ @[simps!] def mk₃ (f : V × V × V→ ℚ) (map_smul : ∀ a S T L, f (a • S, T, L) = a * f (S, T, L)) From 6283d54e93d92453cad31f51179899fbbb48cf6c Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sat, 8 Jun 2024 01:50:34 +0200 Subject: [PATCH 3/9] Update B3.lean --- HepLean/AnomalyCancellation/MSSMNu/B3.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/HepLean/AnomalyCancellation/MSSMNu/B3.lean b/HepLean/AnomalyCancellation/MSSMNu/B3.lean index 378cd82..be921dd 100644 --- a/HepLean/AnomalyCancellation/MSSMNu/B3.lean +++ b/HepLean/AnomalyCancellation/MSSMNu/B3.lean @@ -7,7 +7,7 @@ import HepLean.AnomalyCancellation.MSSMNu.Basic /-! # The definition of the solution B₃ and properties thereof -We define $B_3$ and show that it is a double point of the cubic. +We define `B₃` and show that it is a double point of the cubic. # References @@ -24,7 +24,7 @@ open MSSMCharges open MSSMACCs open BigOperators -/-- $B_3$ is the charge which is $B-L$ in all families, but with the third +/-- `B₃` is the charge which is $B-L$ in all families, but with the third family of the opposite sign. -/ def B₃AsCharge : MSSMACC.charges := toSpecies.symm ⟨fun s => fun i => @@ -52,7 +52,7 @@ def B₃AsCharge : MSSMACC.charges := toSpecies.symm | 0 => -3 | 1 => 3⟩ -/-- $B_3$ as a solution. -/ +/-- `B₃` as a solution. -/ def B₃ : MSSMACC.Sols := MSSMACC.AnomalyFreeMk B₃AsCharge (by rfl) (by rfl) (by rfl) (by rfl) (by rfl) (by rfl) From 8190b8c044da1295611623f05e474b5d6990fbf3 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sat, 8 Jun 2024 01:50:36 +0200 Subject: [PATCH 4/9] Update PlaneWithY3B3.lean --- .../MSSMNu/OrthogY3B3/PlaneWithY3B3.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean index 85a5443..b8af7a9 100644 --- a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean +++ b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean @@ -27,8 +27,8 @@ open MSSMCharges open MSSMACCs open BigOperators -/-- The plane of linear solutions spanned by $Y_3$, $B_3$ and $R$, a point orthogonal -to $Y_3$ and $B_3$. -/ +/-- The plane of linear solutions spanned by `Y₃`, `B₃` and `R`, a point orthogonal +to `Y₃` and `B₃`. -/ def planeY₃B₃ (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) : MSSMACC.LinSols := a • Y₃.1.1 + b • B₃.1.1 + c • R.1 @@ -127,7 +127,7 @@ lemma planeY₃B₃_cubic (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) : rw [show (TriLinearSymm.toCubic cubeTriLin) R.val = cubeTriLin R.val R.val R.val by rfl] ring -/-- The line in the plane spanned by $Y_3$, $B_3$ and $R$ which is in the quadratic, +/-- The line in the plane spanned by `Y₃`, `B₃` and `R` which is in the quadratic, as `LinSols`. -/ def lineQuadAFL (R : MSSMACC.AnomalyFreePerp) (c1 c2 c3 : ℚ) : MSSMACC.LinSols := planeY₃B₃ R (c2 * quadBiLin R.val R.val - 2 * c3 * quadBiLin B₃.val R.val) @@ -141,7 +141,7 @@ lemma lineQuadAFL_quad (R : MSSMACC.AnomalyFreePerp) (c1 c2 c3 : ℚ) : apply Or.inr ring -/-- The line in the plane spanned by $Y_3$, $B_3$ and $R$ which is in the quadratic. -/ +/-- The line in the plane spanned by `Y₃`, `B₃` and `R` which is in the quadratic. -/ def lineQuad (R : MSSMACC.AnomalyFreePerp) (c1 c2 c3 : ℚ) : MSSMACC.QuadSols := AnomalyFreeQuadMk' (lineQuadAFL R c1 c2 c3) (lineQuadAFL_quad R c1 c2 c3) @@ -184,7 +184,7 @@ def α₁ (T : MSSMACC.AnomalyFreePerp) : ℚ := rw [planeY₃B₃_cubic, α₁, α₂, α₃] ring -/-- The line in the plane spanned by $Y_3$, $B_3$ and $R$ which is in the cubic. -/ +/-- The line in the plane spanned by `Y₃`, `B₃` and `R` which is in the cubic. -/ def lineCube (R : MSSMACC.AnomalyFreePerp) (a₁ a₂ a₃ : ℚ) : MSSMACC.LinSols := planeY₃B₃ R From 5c6a8b7a10ea71674e7512325d1780201998fd1b Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sat, 8 Jun 2024 01:50:38 +0200 Subject: [PATCH 5/9] Update ToSols.lean --- HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean index 2ab823f..2eab636 100644 --- a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean +++ b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean @@ -233,7 +233,7 @@ lemma toSolNSQuad_eq_planeY₃B₃_on_α (R : MSSMACC.AnomalyFreePerp) : ring_nf simp -/-- Given a `R ` perpendicular to $Y_3$, and $B_3$, a element of `Sols`. This map is +/-- Given a `R ` perpendicular to `Y₃` and `B₃`, an element of `Sols`. This map is not surjective. -/ def toSolNS : MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, a, _ , _) => a • AnomalyFreeMk'' (toSolNSQuad R) (toSolNSQuad_cube R) @@ -332,7 +332,6 @@ def inQuadProj (T : inQuadSol) : inQuad × ℚ × ℚ × ℚ := - cubeTriLin T.val.val T.val.val Y₃.val * (dot Y₃.val T.val.val - 2 * dot B₃.val T.val.val))) - lemma inQuadToSol_proj (T : inQuadSol) : inQuadToSol (inQuadProj T) = T.val := by rw [inQuadProj, inQuadToSol_smul] apply ACCSystem.Sols.ext @@ -371,7 +370,6 @@ lemma inQuadCubeToSol_smul (R : inQuadCube) (c₁ c₂ c₃ d : ℚ) : rw [planeY₃B₃_smul] rfl - /-- On elements of `inQuadCubeSol` a right-inverse to `inQuadCubeToSol`. -/ def inQuadCubeProj (T : inQuadCubeSol) : inQuadCube × ℚ × ℚ × ℚ := (⟨⟨⟨proj T.val.1.1, (linEqPropSol_iff_proj_linEqProp T.val).mp T.prop.1 ⟩, From c608d8c2896718b2a07d9c1b35c5c57ad010eb26 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sat, 8 Jun 2024 01:50:39 +0200 Subject: [PATCH 6/9] Update Basic.lean --- HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean b/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean index 1dd8e43..a9cdaa3 100644 --- a/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean +++ b/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean @@ -10,7 +10,7 @@ import HepLean.StandardModel.HiggsBoson.Basic The two Higgs doublet model is the standard model plus an additional Higgs doublet. -Currently this file contains the definition of the 2HDM optential. +Currently this file contains the definition of the 2HDM potential. -/ From e6bea536583d59e06675470ef19d64a5a6a71426 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sat, 8 Jun 2024 01:52:44 +0200 Subject: [PATCH 7/9] Update FourVelocity.lean --- HepLean/SpaceTime/FourVelocity.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/HepLean/SpaceTime/FourVelocity.lean b/HepLean/SpaceTime/FourVelocity.lean index 9b60b2d..24494eb 100644 --- a/HepLean/SpaceTime/FourVelocity.lean +++ b/HepLean/SpaceTime/FourVelocity.lean @@ -70,7 +70,7 @@ lemma zero_nonneg_iff (v : PreFourVelocity) : 0 ≤ v.1 0 ↔ 1 ≤ v.1 0 := by · intro h linarith -/-- A `PreFourVelocity` is a `FourVelocity` if its time componenet is non-negative. -/ +/-- A `PreFourVelocity` is a `FourVelocity` if its time component is non-negative. -/ def IsFourVelocity (v : PreFourVelocity) : Prop := 0 ≤ v.1 0 From 2a84c3b87eda41c60d5a84e0c1926beff1d55a7d Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sat, 8 Jun 2024 01:53:28 +0200 Subject: [PATCH 8/9] Update Boosts.lean --- HepLean/SpaceTime/LorentzGroup/Boosts.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/HepLean/SpaceTime/LorentzGroup/Boosts.lean b/HepLean/SpaceTime/LorentzGroup/Boosts.lean index 323e9d5..3ef1800 100644 --- a/HepLean/SpaceTime/LorentzGroup/Boosts.lean +++ b/HepLean/SpaceTime/LorentzGroup/Boosts.lean @@ -12,14 +12,14 @@ import Mathlib.Topology.Constructions This file defines those Lorentz which are boosts. -We first define generalised boosts, which are restricted lorentz transforamations taking -a four velocity `u` to a four velcoity `v`. +We first define generalised boosts, which are restricted lorentz transformations taking +a four velocity `u` to a four velocity `v`. -A boost is the speical case of a generalised boost when `u = stdBasis 0`. +A boost is the special case of a generalised boost when `u = stdBasis 0`. ## TODO -- Show that generalised boosts are in the restircted Lorentz group. +- Show that generalised boosts are in the restricted Lorentz group. - Define boosts. ## References @@ -35,7 +35,7 @@ namespace lorentzGroup open FourVelocity -/-- An auxillary linear map used in the definition of a genearlised boost. -/ +/-- An auxillary linear map used in the definition of a generalised boost. -/ def genBoostAux₁ (u v : FourVelocity) : spaceTime →ₗ[ℝ] spaceTime where toFun x := (2 * ηLin x u) • v.1.1 map_add' x y := by @@ -61,7 +61,7 @@ def genBoostAux₂ (u v : FourVelocity) : spaceTime →ₗ[ℝ] spaceTime where rw [mul_div_assoc, neg_mul_eq_mul_neg, smul_smul] rfl -/-- An genearlised boost. This is a Lorentz transformation which takes the four velocity `u` +/-- An generalised boost. This is a Lorentz transformation which takes the four velocity `u` to `v`. -/ def genBoost (u v : FourVelocity) : spaceTime →ₗ[ℝ] spaceTime := LinearMap.id + genBoostAux₁ u v + genBoostAux₂ u v From 699c38941c058c42688869823a1c92e7da02ad5b Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sat, 8 Jun 2024 01:54:20 +0200 Subject: [PATCH 9/9] Update Orthochronous.lean --- HepLean/SpaceTime/LorentzGroup/Orthochronous.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean b/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean index b553717..af1141f 100644 --- a/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean +++ b/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean @@ -171,7 +171,7 @@ lemma mul_not_othchron_of_not_othchron_othchron {Λ Λ' : lorentzGroup} (h : ¬ rw [zero_zero_mul] exact euclid_norm_not_IsFourVelocity_IsFourVelocity h h' -/-- The homomorphism from `lorentzGroup` to `ℤ₂` whose kernal are the Orthochronous elements. -/ +/-- The homomorphism from `lorentzGroup` to `ℤ₂` whose kernel are the Orthochronous elements. -/ def orthchroRep : lorentzGroup →* ℤ₂ where toFun := orthchroMap map_one' := by