DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Merge pull request #72 from HEPLean/Update-versions

Browse source 
chore: Remove double empty lines
This commit is contained in:
Joseph Tooby-Smith 2024-07-03 08:30:58 -04:00 • committed by GitHub
commit 67e3c47ae9
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
65 changed files with 75 additions and 249 deletions
Download patch file Download diff file Expand all files Collapse all files

5
HepLean/AnomalyCancellation/MSSMNu/Basic.lean
View file

@ -22,7 +22,6 @@ universe v u
open Nat open Nat
open BigOperators open BigOperators
/-- The vector space of charges corresponding to the MSSM fermions. -/ /-- The vector space of charges corresponding to the MSSM fermions. -/
@[simps!] @[simps!]
def MSSMCharges : ACCSystemCharges := ACCSystemChargesMk 20 def MSSMCharges : ACCSystemCharges := ACCSystemChargesMk 20
@ -314,7 +313,6 @@ def quadBiLin : BiLinearSymm MSSMCharges.Charges := BiLinearSymm.mk₂ (
ring ring
ring) ring)
/-- The quadratic ACC. -/ /-- The quadratic ACC. -/
@[simp] @[simp]
def accQuad : HomogeneousQuadratic MSSMCharges.Charges := quadBiLin.toHomogeneousQuad def accQuad : HomogeneousQuadratic MSSMCharges.Charges := quadBiLin.toHomogeneousQuad
@ -335,7 +333,6 @@ lemma accQuad_ext {S T : (MSSMCharges).Charges}
repeat rw [h1] repeat rw [h1]
rw [hd, hu] rw [hd, hu]
/-- The function underlying the symmetric trilinear form used to define the cubic ACC. -/ /-- The function underlying the symmetric trilinear form used to define the cubic ACC. -/
@[simp] @[simp]
def cubeTriLinToFun def cubeTriLinToFun
@ -363,7 +360,6 @@ lemma cubeTriLinToFun_map_smul₁ (a : ℚ) (S T R : MSSMCharges.Charges) :
simp only [map_smul, Hd_apply, Fin.reduceFinMk, Fin.isValue, smul_eq_mul, Hu_apply] simp only [map_smul, Hd_apply, Fin.reduceFinMk, Fin.isValue, smul_eq_mul, Hu_apply]
ring ring
lemma cubeTriLinToFun_map_add₁ (S T R L : MSSMCharges.Charges) : lemma cubeTriLinToFun_map_add₁ (S T R L : MSSMCharges.Charges) :
cubeTriLinToFun (S + T, R, L) = cubeTriLinToFun (S, R, L) + cubeTriLinToFun (T, R, L) := by cubeTriLinToFun (S + T, R, L) = cubeTriLinToFun (S, R, L) + cubeTriLinToFun (T, R, L) := by
simp only [cubeTriLinToFun] simp only [cubeTriLinToFun]
@ -382,7 +378,6 @@ lemma cubeTriLinToFun_map_add₁ (S T R L : MSSMCharges.Charges) :
rw [Hd.map_add, Hu.map_add] rw [Hd.map_add, Hu.map_add]
ring ring
lemma cubeTriLinToFun_swap1 (S T R : MSSMCharges.Charges) : lemma cubeTriLinToFun_swap1 (S T R : MSSMCharges.Charges) :
cubeTriLinToFun (S, T, R) = cubeTriLinToFun (T, S, R) := by cubeTriLinToFun (S, T, R) = cubeTriLinToFun (T, S, R) := by
simp only [cubeTriLinToFun, MSSMSpecies_numberCharges, toSMSpecies_apply, Fin.isValue, Hd_apply, simp only [cubeTriLinToFun, MSSMSpecies_numberCharges, toSMSpecies_apply, Fin.isValue, Hd_apply,

1
HepLean/AnomalyCancellation/MSSMNu/HyperCharge.lean
View file

@ -50,5 +50,4 @@ def YAsCharge : MSSMACC.Charges := toSpecies.invFun
def Y : MSSMACC.Sols := def Y : MSSMACC.Sols :=
MSSMACC.AnomalyFreeMk YAsCharge (by rfl) (by rfl) (by rfl) (by rfl) (by rfl) (by rfl) MSSMACC.AnomalyFreeMk YAsCharge (by rfl) (by rfl) (by rfl) (by rfl) (by rfl) (by rfl)
end MSSMACC end MSSMACC

5
HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/Basic.lean
View file

@ -78,8 +78,6 @@ lemma Y₃_plus_B₃_plus_proj (T : MSSMACC.LinSols) (a b c : ℚ) :
funext i funext i
linarith linarith
lemma quad_Y₃_proj (T : MSSMACC.LinSols) : lemma quad_Y₃_proj (T : MSSMACC.LinSols) :
quadBiLin Y₃.val (proj T).val = dot Y₃.val B₃.val * quadBiLin Y₃.val T.val := by quadBiLin Y₃.val (proj T).val = dot Y₃.val B₃.val * quadBiLin Y₃.val T.val := by
rw [proj_val] rw [proj_val]
@ -119,7 +117,6 @@ lemma quad_proj (T : MSSMACC.Sols) :
rw [quad_Y₃_proj, quad_B₃_proj, quad_self_proj] rw [quad_Y₃_proj, quad_B₃_proj, quad_self_proj]
ring ring
lemma cube_proj_proj_Y₃ (T : MSSMACC.LinSols) : lemma cube_proj_proj_Y₃ (T : MSSMACC.LinSols) :
cubeTriLin (proj T).val (proj T).val Y₃.val = cubeTriLin (proj T).val (proj T).val Y₃.val =
(dot Y₃.val B₃.val)^2 * cubeTriLin T.val T.val Y₃.val := by (dot Y₃.val B₃.val)^2 * cubeTriLin T.val T.val Y₃.val := by
@ -186,6 +183,4 @@ lemma cube_proj (T : MSSMACC.Sols) :
rw [cube_proj_proj_Y₃, cube_proj_proj_B₃, cube_proj_proj_self] rw [cube_proj_proj_Y₃, cube_proj_proj_B₃, cube_proj_proj_self]
ring ring
end MSSMACC end MSSMACC

6
HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean
View file

@ -18,8 +18,6 @@ The plane spanned by Y₃, B₃ and third orthogonal point.
-/ -/
universe v u universe v u
namespace MSSMACC namespace MSSMACC
@ -44,7 +42,6 @@ lemma planeY₃B₃_smul (R : MSSMACC.AnomalyFreePerp) (a b c d : ℚ) :
rw [smul_add, smul_add] rw [smul_add, smul_add]
rw [smul_smul, smul_smul, smul_smul] rw [smul_smul, smul_smul, smul_smul]
lemma planeY₃B₃_eq (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) (h : a = a' ∧ b = b' ∧ c = c') : lemma planeY₃B₃_eq (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) (h : a = a' ∧ b = b' ∧ c = c') :
(planeY₃B₃ R a b c) = (planeY₃B₃ R a' b' c') := by (planeY₃B₃ R a b c) = (planeY₃B₃ R a' b' c') := by
rw [h.1, h.2.1, h.2.2] rw [h.1, h.2.1, h.2.2]
@ -94,7 +91,6 @@ lemma planeY₃B₃_val_eq' (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) (hR' : R
rw [ha, hb, hc] rw [ha, hb, hc]
simp simp
lemma planeY₃B₃_quad (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) : lemma planeY₃B₃_quad (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) :
accQuad (planeY₃B₃ R a b c).val = c * (2 * a * quadBiLin Y₃.val R.val accQuad (planeY₃B₃ R a b c).val = c * (2 * a * quadBiLin Y₃.val R.val
+ 2 * b * quadBiLin B₃.val R.val + c * quadBiLin R.val R.val) := by + 2 * b * quadBiLin B₃.val R.val + c * quadBiLin R.val R.val) := by
@ -185,7 +181,6 @@ def lineCube (R : MSSMACC.AnomalyFreePerp) (a₁ a₂ a₃ : ℚ) :
(3 * a₃ * cubeTriLin R.val R.val Y₃.val - a₁ * cubeTriLin R.val R.val R.val) (3 * a₃ * cubeTriLin R.val R.val Y₃.val - a₁ * cubeTriLin R.val R.val R.val)
(3 * (a₁ * cubeTriLin R.val R.val B₃.val - a₂ * cubeTriLin R.val R.val Y₃.val)) (3 * (a₁ * cubeTriLin R.val R.val B₃.val - a₂ * cubeTriLin R.val R.val Y₃.val))
lemma lineCube_smul (R : MSSMACC.AnomalyFreePerp) (a b c d : ℚ) : lemma lineCube_smul (R : MSSMACC.AnomalyFreePerp) (a b c d : ℚ) :
lineCube R (d * a) (d * b) (d * c) = d • lineCube R a b c := by lineCube R (d * a) (d * b) (d * c) = d • lineCube R a b c := by
apply ACCSystemLinear.LinSols.ext apply ACCSystemLinear.LinSols.ext
@ -242,5 +237,4 @@ lemma α₂_proj_zero (T : MSSMACC.Sols) (h1 : α₃ (proj T.1.1) = 0) :
end proj end proj
end MSSMACC end MSSMACC

5
HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
View file

@ -18,7 +18,6 @@ To define `toSols` we define a series of other maps from various subtypes of
`MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ` to `MSSMACC.Sols`. And show that these maps form a `MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ` to `MSSMACC.Sols`. And show that these maps form a
surjection on certain subtypes of `MSSMACC.Sols`. surjection on certain subtypes of `MSSMACC.Sols`.
# References # References
The main reference for the material in this file is: The main reference for the material in this file is:
@ -78,7 +77,6 @@ lemma linEqPropSol_iff_proj_linEqProp (R : MSSMACC.Sols) :
rw [h.2.2] rw [h.2.2]
simp simp
/-- A condition which is satisfied if the plane spanned by `R`, `Y₃` and `B₃` lies /-- A condition which is satisfied if the plane spanned by `R`, `Y₃` and `B₃` lies
entirely in the quadratic surface. -/ entirely in the quadratic surface. -/
def InQuadProp (R : MSSMACC.AnomalyFreePerp) : Prop := def InQuadProp (R : MSSMACC.AnomalyFreePerp) : Prop :=
@ -137,7 +135,6 @@ def InCubeProp (R : MSSMACC.AnomalyFreePerp) : Prop :=
cubeTriLin R.val R.val R.val = 0 ∧ cubeTriLin R.val R.val B₃.val = 0 ∧ cubeTriLin R.val R.val R.val = 0 ∧ cubeTriLin R.val R.val B₃.val = 0 ∧
cubeTriLin R.val R.val Y₃.val = 0 cubeTriLin R.val R.val Y₃.val = 0
instance (R : MSSMACC.AnomalyFreePerp) : Decidable (InCubeProp R) := by instance (R : MSSMACC.AnomalyFreePerp) : Decidable (InCubeProp R) := by
apply And.decidable apply And.decidable
@ -238,7 +235,6 @@ not surjective. -/
def toSolNS : MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, a, _ , _) => def toSolNS : MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, a, _ , _) =>
a • AnomalyFreeMk'' (toSolNSQuad R) (toSolNSQuad_cube R) a • AnomalyFreeMk'' (toSolNSQuad R) (toSolNSQuad_cube R)
/-- A map from `Sols` to `MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ` which on elements of /-- A map from `Sols` to `MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ` which on elements of
`notInLineEqSol` will produce a right inverse to `toSolNS`. -/ `notInLineEqSol` will produce a right inverse to `toSolNS`. -/
def toSolNSProj (T : MSSMACC.Sols) : MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ := def toSolNSProj (T : MSSMACC.Sols) : MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ :=
@ -458,7 +454,6 @@ theorem toSol_surjective : Function.Surjective toSol := by
simp at h₃ simp at h₃
exact toSol_inQuadCube ⟨T, And.intro h₁ (And.intro h₂ h₃)⟩ exact toSol_inQuadCube ⟨T, And.intro h₁ (And.intro h₂ h₃)⟩
end AnomalyFreePerp end AnomalyFreePerp
end MSSMACC end MSSMACC

7
HepLean/AnomalyCancellation/PureU1/Basic.lean
View file

@ -16,7 +16,6 @@ We define the anomaly cancellation conditions for a pure U(1) gauge theory with
universe v u universe v u
open Nat open Nat
open Finset open Finset
namespace PureU1 namespace PureU1
@ -35,7 +34,6 @@ def accGrav (n : ℕ) : ((PureU1Charges n).Charges →ₗ[ℚ] ℚ) where
simp [HSMul.hSMul, SMul.smul] simp [HSMul.hSMul, SMul.smul]
rw [← Finset.mul_sum] rw [← Finset.mul_sum]
/-- The symmetric trilinear form used to define the cubic anomaly. -/ /-- The symmetric trilinear form used to define the cubic anomaly. -/
@[simps!] @[simps!]
def accCubeTriLinSymm {n : ℕ} : TriLinearSymm (PureU1Charges n).Charges := TriLinearSymm.mk₃ def accCubeTriLinSymm {n : ℕ} : TriLinearSymm (PureU1Charges n).Charges := TriLinearSymm.mk₃
@ -70,14 +68,11 @@ def accCubeTriLinSymm {n : ℕ} : TriLinearSymm (PureU1Charges n).Charges := Tri
ring ring
) )
/-- The cubic anomaly equation. -/ /-- The cubic anomaly equation. -/
@[simp] @[simp]
def accCube (n : ℕ) : HomogeneousCubic ((PureU1Charges n).Charges) := def accCube (n : ℕ) : HomogeneousCubic ((PureU1Charges n).Charges) :=
(accCubeTriLinSymm).toCubic (accCubeTriLinSymm).toCubic
lemma accCube_explicit (n : ℕ) (S : (PureU1Charges n).Charges) : lemma accCube_explicit (n : ℕ) (S : (PureU1Charges n).Charges) :
accCube n S = ∑ i : Fin n, S i ^ 3:= by accCube n S = ∑ i : Fin n, S i ^ 3:= by
rw [accCube, TriLinearSymm.toCubic] rw [accCube, TriLinearSymm.toCubic]
@ -165,7 +160,6 @@ lemma sum_of_charges {n : ℕ} (f : Fin k → (PureU1 n).Charges) (j : Fin n) :
erw [← hlt] erw [← hlt]
simp simp
lemma sum_of_anomaly_free_linear {n : ℕ} (f : Fin k → (PureU1 n).LinSols) (j : Fin n) : lemma sum_of_anomaly_free_linear {n : ℕ} (f : Fin k → (PureU1 n).LinSols) (j : Fin n) :
(∑ i : Fin k, (f i)).1 j = (∑ i : Fin k, (f i).1 j) := by (∑ i : Fin k, (f i)).1 j = (∑ i : Fin k, (f i).1 j) := by
induction k induction k
@ -177,5 +171,4 @@ lemma sum_of_anomaly_free_linear {n : ℕ} (f : Fin k → (PureU1 n).LinSols) (j
erw [← hlt] erw [← hlt]
simp simp
end PureU1 end PureU1

2
HepLean/AnomalyCancellation/PureU1/BasisLinear.lean
View file

@ -75,7 +75,6 @@ def asLinSols (j : Fin n) : (PureU1 n.succ).LinSols :=
intro hk intro hk
simp at hk⟩ simp at hk⟩
lemma sum_of_vectors {n : ℕ} (f : Fin k → (PureU1 n).LinSols) (j : Fin n) : lemma sum_of_vectors {n : ℕ} (f : Fin k → (PureU1 n).LinSols) (j : Fin n) :
(∑ i : Fin k, (f i)).1 j = (∑ i : Fin k, (f i).1 j) := (∑ i : Fin k, (f i)).1 j = (∑ i : Fin k, (f i).1 j) :=
sum_of_anomaly_free_linear (fun i => f i) j sum_of_anomaly_free_linear (fun i => f i) j
@ -134,5 +133,4 @@ lemma finrank_AnomalyFreeLinear :
end BasisLinear end BasisLinear
end PureU1 end PureU1

5
HepLean/AnomalyCancellation/PureU1/ConstAbs.lean
View file

@ -120,7 +120,6 @@ lemma boundary_accGrav' (k : Fin n) : accGrav n.succ S =
intro i intro i
simp simp
lemma boundary_accGrav'' (k : Fin n) (hk : Boundary S k) : lemma boundary_accGrav'' (k : Fin n) (hk : Boundary S k) :
accGrav n.succ S = (2 * ↑↑k + 1 - ↑n) * S (0 : Fin n.succ) := by accGrav n.succ S = (2 * ↑↑k + 1 - ↑n) * S (0 : Fin n.succ) := by
rw [boundary_accGrav' k] rw [boundary_accGrav' k]
@ -165,7 +164,6 @@ lemma not_hasBoundary_grav (hnot : ¬ (HasBoundary S)) :
accGrav n.succ S = n.succ * S (0 : Fin n.succ) := by accGrav n.succ S = n.succ * S (0 : Fin n.succ) := by
simp [accGrav, ← not_hasBoundry_zero hS hnot] simp [accGrav, ← not_hasBoundry_zero hS hnot]
lemma AFL_hasBoundary (h : A.val (0 : Fin n.succ) ≠ 0) : HasBoundary A.val := by lemma AFL_hasBoundary (h : A.val (0 : Fin n.succ) ≠ 0) : HasBoundary A.val := by
by_contra hn by_contra hn
have h0 := not_hasBoundary_grav hA hn have h0 := not_hasBoundary_grav hA hn
@ -253,12 +251,10 @@ lemma AFL_even_above (A : (PureU1 (2 * n.succ)).LinSols) (h : ConstAbsSorted A.v
rfl rfl
exact AFL_even_above' h hA i exact AFL_even_above' h hA i
end charges end charges
end ConstAbsSorted end ConstAbsSorted
namespace ConstAbs namespace ConstAbs
theorem boundary_value_odd (S : (PureU1 (2 * n + 1)).LinSols) (hs : ConstAbs S.val) : theorem boundary_value_odd (S : (PureU1 (2 * n + 1)).LinSols) (hs : ConstAbs S.val) :
@ -266,7 +262,6 @@ theorem boundary_value_odd (S : (PureU1 (2 * n + 1)).LinSols) (hs : ConstAbs S.v
have hS := And.intro (constAbs_sort hs) (sort_sorted S.val) have hS := And.intro (constAbs_sort hs) (sort_sorted S.val)
sortAFL_zero S (ConstAbsSorted.AFL_odd (sortAFL S) hS) sortAFL_zero S (ConstAbsSorted.AFL_odd (sortAFL S) hS)
theorem boundary_value_even (S : (PureU1 (2 * n.succ)).LinSols) (hs : ConstAbs S.val) : theorem boundary_value_even (S : (PureU1 (2 * n.succ)).LinSols) (hs : ConstAbs S.val) :
VectorLikeEven S.val := by VectorLikeEven S.val := by
have hS := And.intro (constAbs_sort hs) (sort_sorted S.val) have hS := And.intro (constAbs_sort hs) (sort_sorted S.val)

5
HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
View file

@ -190,7 +190,6 @@ lemma basis!_on_other {k : Fin n} {j : Fin (2 * n.succ)} (h1 : j ≠ δ!₁ k)
simp [basis!AsCharges] simp [basis!AsCharges]
simp_all only [ne_eq, ↓reduceIte] simp_all only [ne_eq, ↓reduceIte]
lemma basis!_on_δ!₁_other {k j : Fin n} (h : k ≠ j) : lemma basis!_on_δ!₁_other {k j : Fin n} (h : k ≠ j) :
basis!AsCharges k (δ!₁ j) = 0 := by basis!AsCharges k (δ!₁ j) = 0 := by
simp [basis!AsCharges] simp [basis!AsCharges]
@ -310,7 +309,6 @@ lemma basis!_accCube (j : Fin n) :
simp [basis!_δ!₂_eq_minus_δ!₁] simp [basis!_δ!₂_eq_minus_δ!₁]
ring ring
/-- The first part of the basis as `LinSols`. -/ /-- The first part of the basis as `LinSols`. -/
@[simps!] @[simps!]
def basis (j : Fin n.succ) : (PureU1 (2 * n.succ)).LinSols := def basis (j : Fin n.succ) : (PureU1 (2 * n.succ)).LinSols :=
@ -587,7 +585,6 @@ theorem basis!_linear_independent : LinearIndependent ℚ (@basis! n) := by
rw [P!'_val] at h1 rw [P!'_val] at h1
exact P!_zero f h1 exact P!_zero f h1
theorem basisa_linear_independent : LinearIndependent ℚ (@basisa n) := by theorem basisa_linear_independent : LinearIndependent ℚ (@basisa n) := by
apply Fintype.linearIndependent_iff.mpr apply Fintype.linearIndependent_iff.mpr
intro f h intro f h
@ -663,7 +660,6 @@ lemma Pa_eq (g g' : Fin n.succ → ℚ) (f f' : Fin n → ℚ) :
rw [← join_ext] rw [← join_ext]
exact Pa'_eq _ _ exact Pa'_eq _ _
lemma basisa_card : Fintype.card ((Fin n.succ) ⊕ (Fin n)) = lemma basisa_card : Fintype.card ((Fin n.succ) ⊕ (Fin n)) =
FiniteDimensional.finrank ℚ (PureU1 (2 * n.succ)).LinSols := by FiniteDimensional.finrank ℚ (PureU1 (2 * n.succ)).LinSols := by
erw [BasisLinear.finrank_AnomalyFreeLinear] erw [BasisLinear.finrank_AnomalyFreeLinear]
@ -675,7 +671,6 @@ noncomputable def basisaAsBasis :
Basis (Fin (succ n) ⊕ Fin n) ℚ (PureU1 (2 * succ n)).LinSols := Basis (Fin (succ n) ⊕ Fin n) ℚ (PureU1 (2 * succ n)).LinSols :=
basisOfLinearIndependentOfCardEqFinrank (@basisa_linear_independent n) basisa_card basisOfLinearIndependentOfCardEqFinrank (@basisa_linear_independent n) basisa_card
lemma span_basis (S : (PureU1 (2 * n.succ)).LinSols) : lemma span_basis (S : (PureU1 (2 * n.succ)).LinSols) :
∃ (g : Fin n.succ → ℚ) (f : Fin n → ℚ), S.val = P g + P! f := by ∃ (g : Fin n.succ → ℚ) (f : Fin n → ℚ), S.val = P g + P! f := by
have h := (mem_span_range_iff_exists_fun ℚ).mp (Basis.mem_span basisaAsBasis S) have h := (mem_span_range_iff_exists_fun ℚ).mp (Basis.mem_span basisaAsBasis S)

3
HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean
View file

@ -134,7 +134,6 @@ theorem generic_case {S : (PureU1 (2 * n.succ)).Sols} (h : GenericCase S) :
simp at h simp at h
exact h exact h
lemma special_case_lineInCubic {S : (PureU1 (2 * n.succ)).Sols} lemma special_case_lineInCubic {S : (PureU1 (2 * n.succ)).Sols}
(h : SpecialCase S) : LineInCubic S.1.1 := by (h : SpecialCase S) : LineInCubic S.1.1 := by
intro g f hS a b intro g f hS a b
@ -152,7 +151,6 @@ lemma special_case_lineInCubic {S : (PureU1 (2 * n.succ)).Sols}
erw [h] erw [h]
simp simp
lemma special_case_lineInCubic_perm {S : (PureU1 (2 * n.succ)).Sols} lemma special_case_lineInCubic_perm {S : (PureU1 (2 * n.succ)).Sols}
(h : ∀ (M : (FamilyPermutations (2 * n.succ)).group), (h : ∀ (M : (FamilyPermutations (2 * n.succ)).group),
SpecialCase ((FamilyPermutations (2 * n.succ)).solAction.toFun S M)) : SpecialCase ((FamilyPermutations (2 * n.succ)).solAction.toFun S M)) :
@ -160,7 +158,6 @@ lemma special_case_lineInCubic_perm {S : (PureU1 (2 * n.succ)).Sols}
intro M intro M
exact special_case_lineInCubic (h M) exact special_case_lineInCubic (h M)
theorem special_case {S : (PureU1 (2 * n.succ.succ)).Sols} theorem special_case {S : (PureU1 (2 * n.succ.succ)).Sols}
(h : ∀ (M : (FamilyPermutations (2 * n.succ.succ)).group), (h : ∀ (M : (FamilyPermutations (2 * n.succ.succ)).group),
SpecialCase ((FamilyPermutations (2 * n.succ.succ)).solAction.toFun S M)) : SpecialCase ((FamilyPermutations (2 * n.succ.succ)).solAction.toFun S M)) :

5
HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean
View file

@ -26,7 +26,6 @@ We will show that `n ≥ 4` the `line in plane` condition on solutions implies t
-/ -/
namespace PureU1 namespace PureU1
open BigOperators open BigOperators
@ -52,7 +51,6 @@ lemma lineInPlaneCond_perm {S : (PureU1 (n)).LinSols} (hS : LineInPlaneCond S)
all_goals simp_all only [ne_eq, Equiv.invFun_as_coe, EmbeddingLike.apply_eq_iff_eq, all_goals simp_all only [ne_eq, Equiv.invFun_as_coe, EmbeddingLike.apply_eq_iff_eq,
not_false_eq_true] not_false_eq_true]
lemma lineInPlaneCond_eq_last' {S : (PureU1 (n.succ.succ)).LinSols} (hS : LineInPlaneCond S) lemma lineInPlaneCond_eq_last' {S : (PureU1 (n.succ.succ)).LinSols} (hS : LineInPlaneCond S)
(h : ¬ (S.val ((Fin.last n).castSucc))^2 = (S.val ((Fin.last n).succ))^2 ) : (h : ¬ (S.val ((Fin.last n).castSucc))^2 = (S.val ((Fin.last n).succ))^2 ) :
(2 - n) * S.val (Fin.last (n + 1)) = (2 - n) * S.val (Fin.last (n + 1)) =
@ -157,7 +155,6 @@ lemma linesInPlane_four (S : (PureU1 4).Sols) (hS : LineInPlaneCond S.1.1) :
simp at h6 simp at h6
simp_all simp_all
lemma linesInPlane_eq_sq_four {S : (PureU1 4).Sols} lemma linesInPlane_eq_sq_four {S : (PureU1 4).Sols}
(hS : LineInPlaneCond S.1.1) : ∀ (i j : Fin 4) (_ : i ≠ j), (hS : LineInPlaneCond S.1.1) : ∀ (i j : Fin 4) (_ : i ≠ j),
ConstAbsProp (S.val i, S.val j) := by ConstAbsProp (S.val i, S.val j) := by
@ -168,7 +165,6 @@ lemma linesInPlane_eq_sq_four {S : (PureU1 4).Sols}
(lineInPlaneCond_perm hS M) (lineInPlaneCond_perm hS M)
exact linesInPlane_four S' hS' exact linesInPlane_four S' hS'
lemma linesInPlane_constAbs_four (S : (PureU1 4).Sols) lemma linesInPlane_constAbs_four (S : (PureU1 4).Sols)
(hS : LineInPlaneCond S.1.1) : ConstAbs S.val := by (hS : LineInPlaneCond S.1.1) : ConstAbs S.val := by
intro i j intro i j
@ -183,5 +179,4 @@ theorem linesInPlane_constAbs_AF (S : (PureU1 (n.succ.succ.succ.succ)).Sols)
exact linesInPlane_constAbs_four S hS exact linesInPlane_constAbs_four S hS
exact linesInPlane_constAbs hS exact linesInPlane_constAbs hS
end PureU1 end PureU1

1
HepLean/AnomalyCancellation/PureU1/LowDim/Three.lean
View file

@ -50,7 +50,6 @@ def solOfLinear (S : (PureU1 3).LinSols)
⟨⟨S, by intro i; simp at i; exact Fin.elim0 i⟩, ⟨⟨S, by intro i; simp at i; exact Fin.elim0 i⟩,
(cube_for_linSol S).mp hS⟩ (cube_for_linSol S).mp hS⟩
theorem solOfLinear_surjects (S : (PureU1 3).Sols) : theorem solOfLinear_surjects (S : (PureU1 3).Sols) :
∃ (T : (PureU1 3).LinSols) (hT : T.val (0 : Fin 3) = 0 ∨ T.val (1 : Fin 3) = 0 ∃ (T : (PureU1 3).LinSols) (hT : T.val (0 : Fin 3) = 0 ∨ T.val (1 : Fin 3) = 0
∨ T.val (2 : Fin 3) = 0), solOfLinear T hT = S := by ∨ T.val (2 : Fin 3) = 0), solOfLinear T hT = S := by

7
HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
View file

@ -23,7 +23,6 @@ namespace PureU1
variable {n : ℕ} variable {n : ℕ}
namespace VectorLikeOddPlane namespace VectorLikeOddPlane
lemma split_odd! (n : ℕ) : (1 + n) + n = 2 * n +1 := by lemma split_odd! (n : ℕ) : (1 + n) + n = 2 * n +1 := by
@ -484,7 +483,6 @@ lemma P_P_P!_accCube (g : Fin n → ℚ) (j : Fin n) :
simp only [mul_zero, add_zero] simp only [mul_zero, add_zero]
simp simp
lemma P_zero (f : Fin n → ℚ) (h : P f = 0) : ∀ i, f i = 0 := by lemma P_zero (f : Fin n → ℚ) (h : P f = 0) : ∀ i, f i = 0 := by
intro i intro i
erw [← P_δ₁ f] erw [← P_δ₁ f]
@ -572,7 +570,6 @@ theorem basis!_linear_independent : LinearIndependent ℚ (@basis! n) := by
rw [P!'_val] at h1 rw [P!'_val] at h1
exact P!_zero f h1 exact P!_zero f h1
theorem basisa_linear_independent : LinearIndependent ℚ (@basisa n.succ) := by theorem basisa_linear_independent : LinearIndependent ℚ (@basisa n.succ) := by
apply Fintype.linearIndependent_iff.mpr apply Fintype.linearIndependent_iff.mpr
intro f h intro f h
@ -648,8 +645,6 @@ lemma Pa_eq (g g' : Fin n.succ → ℚ) (f f' : Fin n.succ → ℚ) :
rw [← join_ext] rw [← join_ext]
exact Pa'_eq _ _ exact Pa'_eq _ _
lemma basisa_card : Fintype.card ((Fin n.succ) ⊕ (Fin n.succ)) = lemma basisa_card : Fintype.card ((Fin n.succ) ⊕ (Fin n.succ)) =
FiniteDimensional.finrank ℚ (PureU1 (2 * n.succ + 1)).LinSols := by FiniteDimensional.finrank ℚ (PureU1 (2 * n.succ + 1)).LinSols := by
erw [BasisLinear.finrank_AnomalyFreeLinear] erw [BasisLinear.finrank_AnomalyFreeLinear]
@ -706,8 +701,6 @@ lemma span_basis_swap! {S : (PureU1 (2 * n.succ + 1)).LinSols} (j : Fin n.succ)
apply swap!_as_add at hS apply swap!_as_add at hS
exact hS exact hS
end VectorLikeOddPlane end VectorLikeOddPlane
end PureU1 end PureU1

4
HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
View file

@ -54,7 +54,6 @@ lemma lineInCubic_expand {S : (PureU1 (2 * n + 1)).LinSols} (h : LineInCubic S)
rw [← h1] rw [← h1]
ring ring
lemma line_in_cubic_P_P_P! {S : (PureU1 (2 * n + 1)).LinSols} (h : LineInCubic S) : lemma line_in_cubic_P_P_P! {S : (PureU1 (2 * n + 1)).LinSols} (h : LineInCubic S) :
∀ (g : Fin n → ℚ) (f : Fin n → ℚ) (_ : S.val = P g + P! f), ∀ (g : Fin n → ℚ) (f : Fin n → ℚ) (_ : S.val = P g + P! f),
accCubeTriLinSymm (P g) (P g) (P! f) = 0 := by accCubeTriLinSymm (P g) (P g) (P! f) = 0 := by
@ -62,8 +61,6 @@ lemma line_in_cubic_P_P_P! {S : (PureU1 (2 * n + 1)).LinSols} (h : LineInCubic S
linear_combination 2 / 3 * (lineInCubic_expand h g f hS 1 1 ) - linear_combination 2 / 3 * (lineInCubic_expand h g f hS 1 1 ) -
(lineInCubic_expand h g f hS 1 2 ) / 6 (lineInCubic_expand h g f hS 1 2 ) / 6
/-- We say a `LinSol` satisfies `lineInCubicPerm` if all its permutations satisfy `lineInCubic`. -/ /-- We say a `LinSol` satisfies `lineInCubicPerm` if all its permutations satisfy `lineInCubic`. -/
def LineInCubicPerm (S : (PureU1 (2 * n + 1)).LinSols) : Prop := def LineInCubicPerm (S : (PureU1 (2 * n + 1)).LinSols) : Prop :=
∀ (M : (FamilyPermutations (2 * n + 1)).group ), ∀ (M : (FamilyPermutations (2 * n + 1)).group ),
@ -86,7 +83,6 @@ lemma lineInCubicPerm_permute {S : (PureU1 (2 * n + 1)).LinSols}
rw [ht] rw [ht]
exact hS (M * M') exact hS (M * M')
lemma lineInCubicPerm_swap {S : (PureU1 (2 * n.succ + 1)).LinSols} lemma lineInCubicPerm_swap {S : (PureU1 (2 * n.succ + 1)).LinSols}
(LIC : LineInCubicPerm S) : (LIC : LineInCubicPerm S) :
∀ (j : Fin n.succ) (g f : Fin n.succ → ℚ) (_ : S.val = Pa g f) , ∀ (j : Fin n.succ) (g f : Fin n.succ → ℚ) (_ : S.val = Pa g f) ,

1
HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean
View file

@ -133,7 +133,6 @@ theorem generic_case {S : (PureU1 (2 * n.succ + 1)).Sols} (h : GenericCase S) :
simp at h simp at h
exact h exact h
lemma special_case_lineInCubic {S : (PureU1 (2 * n.succ + 1)).Sols} lemma special_case_lineInCubic {S : (PureU1 (2 * n.succ + 1)).Sols}
(h : SpecialCase S) : (h : SpecialCase S) :
LineInCubic S.1.1 := by LineInCubic S.1.1 := by

4
HepLean/AnomalyCancellation/PureU1/Permutations.lean
View file

@ -96,7 +96,6 @@ def FamilyPermutations (n : ℕ) : ACCSystemGroupAction (PureU1 n) where
exact Fin.elim0 i exact Fin.elim0 i
cubicInvariant := accCube_invariant cubicInvariant := accCube_invariant
lemma FamilyPermutations_charges_apply (S : (PureU1 n).Charges) lemma FamilyPermutations_charges_apply (S : (PureU1 n).Charges)
(i : Fin n) (f : (FamilyPermutations n).group) : (i : Fin n) (f : (FamilyPermutations n).group) :
((FamilyPermutations n).rep f S) i = S (f.invFun i) := by ((FamilyPermutations n).rep f S) i = S (f.invFun i) := by
@ -107,7 +106,6 @@ lemma FamilyPermutations_anomalyFreeLinear_apply (S : (PureU1 n).LinSols)
((FamilyPermutations n).linSolRep f S).val i = S.val (f.invFun i) := by ((FamilyPermutations n).linSolRep f S).val i = S.val (f.invFun i) := by
rfl rfl
/-- The permutation which swaps i and j. TODO: Replace with: `Equiv.swap`. -/ /-- The permutation which swaps i and j. TODO: Replace with: `Equiv.swap`. -/
def pairSwap {n : ℕ} (i j : Fin n) : (FamilyPermutations n).group where def pairSwap {n : ℕ} (i j : Fin n) : (FamilyPermutations n).group where
toFun s := toFun s :=
@ -247,7 +245,6 @@ lemma permThreeInj_fst_apply :
⟨i, permThreeInj_fst hij hjk hik⟩ = 0 := by ⟨i, permThreeInj_fst hij hjk hik⟩ = 0 := by
exact (Equiv.symm_apply_eq (Function.Embedding.toEquivRange (permThreeInj hij hjk hik))).mpr rfl exact (Equiv.symm_apply_eq (Function.Embedding.toEquivRange (permThreeInj hij hjk hik))).mpr rfl
lemma permThreeInj_snd : j ∈ Set.range ⇑(permThreeInj hij hjk hik) := by lemma permThreeInj_snd : j ∈ Set.range ⇑(permThreeInj hij hjk hik) := by
simp only [Set.mem_range] simp only [Set.mem_range]
use 1 use 1
@ -338,5 +335,4 @@ lemma Prop_three (P : ℚ × ℚ × ℚ → Prop) {S : (PureU1 n).LinSols}
erw [permThree_fst,permThree_snd, permThree_thd] at h1 erw [permThree_fst,permThree_snd, permThree_thd] at h1
exact h1 exact h1
end PureU1 end PureU1

1
HepLean/AnomalyCancellation/PureU1/Sort.lean
View file

@ -67,7 +67,6 @@ def sortAFL {n : ℕ} (S : (PureU1 n).LinSols) : (PureU1 n).LinSols :=
lemma sortAFL_val {n : ℕ} (S : (PureU1 n).LinSols) : (sortAFL S).val = sort S.val := by lemma sortAFL_val {n : ℕ} (S : (PureU1 n).LinSols) : (sortAFL S).val = sort S.val := by
rfl rfl
lemma sortAFL_zero {n : ℕ} (S : (PureU1 n).LinSols) (hS : sortAFL S = 0) : S = 0 := by lemma sortAFL_zero {n : ℕ} (S : (PureU1 n).LinSols) (hS : sortAFL S = 0) : S = 0 := by
apply ACCSystemLinear.LinSols.ext apply ACCSystemLinear.LinSols.ext
have h1 : sort S.val = 0 := by have h1 : sort S.val = 0 := by

2
HepLean/AnomalyCancellation/PureU1/VectorLike.lean
View file

@ -30,7 +30,6 @@ variable {n : ℕ}
-/ -/
lemma split_equal (n : ℕ) : n + n = 2 * n := (Nat.two_mul n).symm lemma split_equal (n : ℕ) : n + n = 2 * n := (Nat.two_mul n).symm
lemma split_odd (n : ℕ) : n + 1 + n = 2 * n + 1 := by omega lemma split_odd (n : ℕ) : n + 1 + n = 2 * n + 1 := by omega
/-- A charge configuration for n even is vector like if when sorted the `i`th element /-- A charge configuration for n even is vector like if when sorted the `i`th element
@ -40,5 +39,4 @@ def VectorLikeEven (S : (PureU1 (2 * n)).Charges) : Prop :=
∀ (i : Fin n), (sort S) (Fin.cast (split_equal n) (Fin.castAdd n i)) ∀ (i : Fin n), (sort S) (Fin.cast (split_equal n) (Fin.castAdd n i))
= - (sort S) (Fin.cast (split_equal n) (Fin.natAdd n i)) = - (sort S) (Fin.cast (split_equal n) (Fin.natAdd n i))
end PureU1 end PureU1

1
HepLean/AnomalyCancellation/SM/Basic.lean
View file

@ -319,5 +319,4 @@ lemma accCube_ext {S T : (SMCharges n).Charges}
rfl rfl
repeat rw [h1] repeat rw [h1]
end SMACCs end SMACCs

4
HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean
View file

@ -24,7 +24,6 @@ open SMCharges
open SMACCs open SMACCs
open BigOperators open BigOperators
lemma E_zero_iff_Q_zero {S : (SMNoGrav 1).Sols} : Q S.val (0 : Fin 1) = 0 ↔ lemma E_zero_iff_Q_zero {S : (SMNoGrav 1).Sols} : Q S.val (0 : Fin 1) = 0 ↔
E S.val (0 : Fin 1) = 0 := by E S.val (0 : Fin 1) = 0 := by
let S' := linearParameters.bijection.symm S.1.1 let S' := linearParameters.bijection.symm S.1.1
@ -38,8 +37,6 @@ lemma E_zero_iff_Q_zero {S : (SMNoGrav 1).Sols} : Q S.val (0 : Fin 1) = 0 ↔
intro hE intro hE
exact S'.cubic_zero_E'_zero hC hE exact S'.cubic_zero_E'_zero hC hE
lemma accGrav_Q_zero {S : (SMNoGrav 1).Sols} (hQ : Q S.val (0 : Fin 1) = 0) : lemma accGrav_Q_zero {S : (SMNoGrav 1).Sols} (hQ : Q S.val (0 : Fin 1) = 0) :
accGrav S.val = 0 := by accGrav S.val = 0 := by
rw [accGrav] rw [accGrav]
@ -74,7 +71,6 @@ theorem accGravSatisfied {S : (SMNoGrav 1).Sols} (FLTThree : FermatLastTheoremWi
exact accGrav_Q_zero hQ exact accGrav_Q_zero hQ
exact accGrav_Q_neq_zero hQ FLTThree exact accGrav_Q_neq_zero hQ FLTThree
end One end One
end SMNoGrav end SMNoGrav
end SM end SM

3
HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
View file

@ -183,7 +183,6 @@ lemma grav (S : linearParameters) :
end linearParameters end linearParameters
/-- The parameters for solutions to the linear ACCs with the condition that Q and E are non-zero.-/ /-- The parameters for solutions to the linear ACCs with the condition that Q and E are non-zero.-/
structure linearParametersQENeqZero where structure linearParametersQENeqZero where
/-- The parameter `x`. -/ /-- The parameter `x`. -/
@ -280,7 +279,6 @@ lemma cubic (S : linearParametersQENeqZero) :
simp_all simp_all
exact add_eq_zero_iff_eq_neg exact add_eq_zero_iff_eq_neg
lemma cubic_v_or_w_zero (S : linearParametersQENeqZero) (h : accCube (bijection S).1.val = 0) lemma cubic_v_or_w_zero (S : linearParametersQENeqZero) (h : accCube (bijection S).1.val = 0)
(FLTThree : FermatLastTheoremWith ℚ 3) : (FLTThree : FermatLastTheoremWith ℚ 3) :
S.v = 0 ∨ S.w = 0 := by S.v = 0 ∨ S.w = 0 := by
@ -364,7 +362,6 @@ lemma grav_of_cubic (S : linearParametersQENeqZero) (h : accCube (bijection S).1
end linearParametersQENeqZero end linearParametersQENeqZero
end One end One
end SMNoGrav end SMNoGrav
end SM end SM

6
HepLean/AnomalyCancellation/SM/Permutations.lean
View file

@ -33,7 +33,6 @@ variable {n : ℕ}
@[simp] @[simp]
instance : Group (PermGroup n) := Pi.group instance : Group (PermGroup n) := Pi.group
/-- The image of an element of `permGroup n` under the representation on charges. -/ /-- The image of an element of `permGroup n` under the representation on charges. -/
@[simps!] @[simps!]
def chargeMap (f : PermGroup n) : (SMCharges n).Charges →ₗ[ℚ] (SMCharges n).Charges where def chargeMap (f : PermGroup n) : (SMCharges n).Charges →ₗ[ℚ] (SMCharges n).Charges where
@ -66,7 +65,6 @@ lemma repCharges_toSpecies (f : PermGroup n) (S : (SMCharges n).Charges) (j : Fi
toSpecies j (repCharges f S) = toSpecies j S ∘ f⁻¹ j := by toSpecies j (repCharges f S) = toSpecies j S ∘ f⁻¹ j := by
erw [toSMSpecies_toSpecies_inv] erw [toSMSpecies_toSpecies_inv]
lemma toSpecies_sum_invariant (m : ℕ) (f : PermGroup n) (S : (SMCharges n).Charges) (j : Fin 5) : lemma toSpecies_sum_invariant (m : ℕ) (f : PermGroup n) (S : (SMCharges n).Charges) (j : Fin 5) :
∑ i, ((fun a => a ^ m) ∘ toSpecies j (repCharges f S)) i = ∑ i, ((fun a => a ^ m) ∘ toSpecies j (repCharges f S)) i =
∑ i, ((fun a => a ^ m) ∘ toSpecies j S) i := by ∑ i, ((fun a => a ^ m) ∘ toSpecies j S) i := by
@ -74,20 +72,16 @@ lemma toSpecies_sum_invariant (m : ℕ) (f : PermGroup n) (S : (SMCharges n).Cha
exact Fintype.sum_equiv (f⁻¹ j) (fun x => ((fun a => a ^ m) ∘ (toSpecies j) S ∘ ⇑(f⁻¹ j)) x) exact Fintype.sum_equiv (f⁻¹ j) (fun x => ((fun a => a ^ m) ∘ (toSpecies j) S ∘ ⇑(f⁻¹ j)) x)
(fun x => ((fun a => a ^ m) ∘ (toSpecies j) S) x) (congrFun rfl) (fun x => ((fun a => a ^ m) ∘ (toSpecies j) S) x) (congrFun rfl)
lemma accGrav_invariant (f : PermGroup n) (S : (SMCharges n).Charges) : lemma accGrav_invariant (f : PermGroup n) (S : (SMCharges n).Charges) :
accGrav (repCharges f S) = accGrav S := accGrav (repCharges f S) = accGrav S :=
accGrav_ext accGrav_ext
(by simpa using toSpecies_sum_invariant 1 f S) (by simpa using toSpecies_sum_invariant 1 f S)
lemma accSU2_invariant (f : PermGroup n) (S : (SMCharges n).Charges) : lemma accSU2_invariant (f : PermGroup n) (S : (SMCharges n).Charges) :
accSU2 (repCharges f S) = accSU2 S := accSU2 (repCharges f S) = accSU2 S :=
accSU2_ext accSU2_ext
(by simpa using toSpecies_sum_invariant 1 f S) (by simpa using toSpecies_sum_invariant 1 f S)
lemma accSU3_invariant (f : PermGroup n) (S : (SMCharges n).Charges) : lemma accSU3_invariant (f : PermGroup n) (S : (SMCharges n).Charges) :
accSU3 (repCharges f S) = accSU3 S := accSU3 (repCharges f S) = accSU3 S :=
accSU3_ext accSU3_ext

5
HepLean/AnomalyCancellation/SMNu/Basic.lean
View file

@ -14,7 +14,6 @@ import Mathlib.Logic.Equiv.Fin
# Anomaly cancellation conditions for n family SM. # Anomaly cancellation conditions for n family SM.
-/ -/
universe v u universe v u
open Nat open Nat
open BigOperators open BigOperators
@ -83,7 +82,6 @@ abbrev E := @toSpecies n 4
/-- The `N` charges as a map `Fin n → ℚ`. -/ /-- The `N` charges as a map `Fin n → ℚ`. -/
abbrev N := @toSpecies n 5 abbrev N := @toSpecies n 5
end SMνCharges end SMνCharges
namespace SMνACCs namespace SMνACCs
@ -111,7 +109,6 @@ def accGrav : (SMνCharges n).Charges →ₗ[ℚ] ℚ where
-- rw [show Rat.cast a = a from rfl] -- rw [show Rat.cast a = a from rfl]
ring ring
lemma accGrav_decomp (S : (SMνCharges n).Charges) : lemma accGrav_decomp (S : (SMνCharges n).Charges) :
accGrav S = 6 * ∑ i, Q S i + 3 * ∑ i, U S i + 3 * ∑ i, D S i + 2 * ∑ i, L S i + ∑ i, E S i + accGrav S = 6 * ∑ i, Q S i + 3 * ∑ i, U S i + 3 * ∑ i, D S i + 2 * ∑ i, L S i + ∑ i, E S i +
∑ i, N S i := by ∑ i, N S i := by
@ -127,7 +124,6 @@ lemma accGrav_ext {S T : (SMνCharges n).Charges}
rw [accGrav_decomp, accGrav_decomp] rw [accGrav_decomp, accGrav_decomp]
repeat erw [hj] repeat erw [hj]
/-- The `SU(2)` anomaly equation. -/ /-- The `SU(2)` anomaly equation. -/
@[simp] @[simp]
def accSU2 : (SMνCharges n).Charges →ₗ[ℚ] ℚ where def accSU2 : (SMνCharges n).Charges →ₗ[ℚ] ℚ where
@ -344,7 +340,6 @@ lemma cubeTriLin_decomp (S T R : (SMνCharges n).Charges) :
repeat erw [Finset.sum_add_distrib] repeat erw [Finset.sum_add_distrib]
repeat erw [← Finset.mul_sum] repeat erw [← Finset.mul_sum]
/-- The cubic ACC. -/ /-- The cubic ACC. -/
@[simp] @[simp]
def accCube : HomogeneousCubic (SMνCharges n).Charges := cubeTriLin.toCubic def accCube : HomogeneousCubic (SMνCharges n).Charges := cubeTriLin.toCubic

1
HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean
View file

@ -79,7 +79,6 @@ def speciesEmbed (m n : ℕ) :
erw [dif_neg hi, dif_neg hi] erw [dif_neg hi, dif_neg hi]
exact Eq.symm (Rat.mul_zero a) exact Eq.symm (Rat.mul_zero a)
/-- The embedding of the `m`-family charges onto the `n`-family charges, with all /-- The embedding of the `m`-family charges onto the `n`-family charges, with all
other charges zero. -/ other charges zero. -/
def familyEmbedding (m n : ℕ) : (SMνCharges m).Charges →ₗ[ℚ] (SMνCharges n).Charges := def familyEmbedding (m n : ℕ) : (SMνCharges m).Charges →ₗ[ℚ] (SMνCharges n).Charges :=

1
HepLean/AnomalyCancellation/SMNu/NoGrav/Basic.lean
View file

@ -110,7 +110,6 @@ def perm (n : ℕ) : ACCSystemGroupAction (SMNoGrav n) where
exact Fin.elim0 i exact Fin.elim0 i
cubicInvariant := accCube_invariant cubicInvariant := accCube_invariant
end SMNoGrav end SMNoGrav
end SMRHN end SMRHN

2
HepLean/AnomalyCancellation/SMNu/Ordinary/Basic.lean
View file

@ -37,7 +37,6 @@ def SM (n : ℕ) : ACCSystem where
namespace SM namespace SM
variable {n : ℕ} variable {n : ℕ}
lemma gravSol (S : (SM n).LinSols) : accGrav S.val = 0 := by lemma gravSol (S : (SM n).LinSols) : accGrav S.val = 0 := by
@ -119,7 +118,6 @@ def perm (n : ℕ) : ACCSystemGroupAction (SM n) where
exact Fin.elim0 i exact Fin.elim0 i
cubicInvariant := accCube_invariant cubicInvariant := accCube_invariant
end SM end SM
end SMRHN end SMRHN

3
HepLean/AnomalyCancellation/SMNu/Ordinary/DimSevenPlane.lean
View file

@ -137,7 +137,6 @@ lemma B₀_Bi_cubic {i : Fin 7} (hi : 0 ≠ i) (S : (SM 3).Charges) :
simp at hi <;> simp at hi <;>
simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv] simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
lemma B₁_Bi_cubic {i : Fin 7} (hi : 1 ≠ i) (S : (SM 3).Charges) : lemma B₁_Bi_cubic {i : Fin 7} (hi : 1 ≠ i) (S : (SM 3).Charges) :
cubeTriLin (B 1) (B i) S = 0 := by cubeTriLin (B 1) (B i) S = 0 := by
change cubeTriLin B₁ (B i) S = 0 change cubeTriLin B₁ (B i) S = 0
@ -246,7 +245,6 @@ lemma B₆_B₆_Bi_cubic {i : Fin 7} :
fin_cases i <;> fin_cases i <;>
simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv] simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
lemma Bi_Bi_Bj_cubic (i j : Fin 7) : lemma Bi_Bi_Bj_cubic (i j : Fin 7) :
cubeTriLin (B i) (B i) (B j) = 0 := by cubeTriLin (B i) (B i) (B j) = 0 := by
fin_cases i fin_cases i
@ -344,6 +342,5 @@ theorem seven_dim_plane_exists : ∃ (B : Fin 7 → (SM 3).Charges),
exact PlaneSeven.basis_linear_independent exact PlaneSeven.basis_linear_independent
exact PlaneSeven.B_sum_is_sol exact PlaneSeven.B_sum_is_sol
end SM end SM
end SMRHN end SMRHN

7
HepLean/AnomalyCancellation/SMNu/Permutations.lean
View file

@ -65,7 +65,6 @@ lemma repCharges_toSpecies (f : PermGroup n) (S : (SMνCharges n).Charges) (j :
toSpecies j (repCharges f S) = toSpecies j S ∘ f⁻¹ j := by toSpecies j (repCharges f S) = toSpecies j S ∘ f⁻¹ j := by
erw [toSMSpecies_toSpecies_inv] erw [toSMSpecies_toSpecies_inv]
lemma toSpecies_sum_invariant (m : ℕ) (f : PermGroup n) (S : (SMνCharges n).Charges) (j : Fin 6) : lemma toSpecies_sum_invariant (m : ℕ) (f : PermGroup n) (S : (SMνCharges n).Charges) (j : Fin 6) :
∑ i, ((fun a => a ^ m) ∘ toSpecies j (repCharges f S)) i = ∑ i, ((fun a => a ^ m) ∘ toSpecies j (repCharges f S)) i =
∑ i, ((fun a => a ^ m) ∘ toSpecies j S) i := by ∑ i, ((fun a => a ^ m) ∘ toSpecies j S) i := by
@ -74,19 +73,16 @@ lemma toSpecies_sum_invariant (m : ℕ) (f : PermGroup n) (S : (SMνCharges n).C
refine Equiv.Perm.sum_comp _ _ _ ?_ refine Equiv.Perm.sum_comp _ _ _ ?_
simp only [PermGroup, Fin.isValue, Pi.inv_apply, ne_eq, coe_univ, Set.subset_univ] simp only [PermGroup, Fin.isValue, Pi.inv_apply, ne_eq, coe_univ, Set.subset_univ]
lemma accGrav_invariant (f : PermGroup n) (S : (SMνCharges n).Charges) : lemma accGrav_invariant (f : PermGroup n) (S : (SMνCharges n).Charges) :
accGrav (repCharges f S) = accGrav S := accGrav (repCharges f S) = accGrav S :=
accGrav_ext accGrav_ext
(by simpa using toSpecies_sum_invariant 1 f S) (by simpa using toSpecies_sum_invariant 1 f S)
lemma accSU2_invariant (f : PermGroup n) (S : (SMνCharges n).Charges) : lemma accSU2_invariant (f : PermGroup n) (S : (SMνCharges n).Charges) :
accSU2 (repCharges f S) = accSU2 S := accSU2 (repCharges f S) = accSU2 S :=
accSU2_ext accSU2_ext
(by simpa using toSpecies_sum_invariant 1 f S) (by simpa using toSpecies_sum_invariant 1 f S)
lemma accSU3_invariant (f : PermGroup n) (S : (SMνCharges n).Charges) : lemma accSU3_invariant (f : PermGroup n) (S : (SMνCharges n).Charges) :
accSU3 (repCharges f S) = accSU3 S := accSU3 (repCharges f S) = accSU3 S :=
accSU3_ext accSU3_ext
@ -97,7 +93,6 @@ lemma accYY_invariant (f : PermGroup n) (S : (SMνCharges n).Charges) :
accYY_ext accYY_ext
(by simpa using toSpecies_sum_invariant 1 f S) (by simpa using toSpecies_sum_invariant 1 f S)
lemma accQuad_invariant (f : PermGroup n) (S : (SMνCharges n).Charges) : lemma accQuad_invariant (f : PermGroup n) (S : (SMνCharges n).Charges) :
accQuad (repCharges f S) = accQuad S := accQuad (repCharges f S) = accQuad S :=
accQuad_ext accQuad_ext
@ -108,6 +103,4 @@ lemma accCube_invariant (f : PermGroup n) (S : (SMνCharges n).Charges) :
accCube_ext accCube_ext
(by simpa using toSpecies_sum_invariant 3 f S) (by simpa using toSpecies_sum_invariant 3 f S)
end SMRHN end SMRHN

1
HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean
View file

@ -114,7 +114,6 @@ lemma add_AFL_cube (S : (PlusU1 n).LinSols) (a b : ℚ) :
add_zero, BL_val, mul_zero] add_zero, BL_val, mul_zero]
ring ring
end BL end BL
end PlusU1 end PlusU1
end SMRHN end SMRHN

1
HepLean/AnomalyCancellation/SMNu/PlusU1/Basic.lean
View file

@ -37,7 +37,6 @@ def PlusU1 (n : ℕ) : ACCSystem where
namespace PlusU1 namespace PlusU1
variable {n : ℕ} variable {n : ℕ}
lemma gravSol (S : (PlusU1 n).LinSols) : accGrav S.val = 0 := by lemma gravSol (S : (PlusU1 n).LinSols) : accGrav S.val = 0 := by

2
HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean
View file

@ -58,7 +58,6 @@ lemma exists_plane_exists_basis {n : ℕ} (hE : ExistsPlane n) :
| Sum.inl i => exact h3 i | Sum.inl i => exact h3 i
| Sum.inr i => exact h4 i | Sum.inr i => exact h4 i
theorem plane_exists_dim_le_7 {n : ℕ} (hn : ExistsPlane n) : n ≤ 7 := by theorem plane_exists_dim_le_7 {n : ℕ} (hn : ExistsPlane n) : n ≤ 7 := by
obtain ⟨B, hB⟩ := exists_plane_exists_basis hn obtain ⟨B, hB⟩ := exists_plane_exists_basis hn
have h1 := LinearIndependent.fintype_card_le_finrank hB have h1 := LinearIndependent.fintype_card_le_finrank hB
@ -67,6 +66,5 @@ theorem plane_exists_dim_le_7 {n : ℕ} (hn : ExistsPlane n) : n ≤ 7 := by
FiniteDimensional.finrank_fin_fun ℚ] at h1 FiniteDimensional.finrank_fin_fun ℚ] at h1
exact Nat.le_of_add_le_add_left h1 exact Nat.le_of_add_le_add_left h1
end PlusU1 end PlusU1
end SMRHN end SMRHN

2
HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean
View file

@ -68,7 +68,6 @@ lemma on_quadBiLin_AFL (S : (PlusU1 n).LinSols) : quadBiLin (Y n).val S.val = 0
rw [on_quadBiLin] rw [on_quadBiLin]
rw [YYsol S] rw [YYsol S]
lemma add_AFL_quad (S : (PlusU1 n).LinSols) (a b : ℚ) : lemma add_AFL_quad (S : (PlusU1 n).LinSols) (a b : ℚ) :
accQuad (a • S.val + b • (Y n).val) = a ^ 2 * accQuad S.val := by accQuad (a • S.val + b • (Y n).val) = a ^ 2 * accQuad S.val := by
erw [BiLinearSymm.toHomogeneousQuad_add, quadSol (b • (Y n)).1] erw [BiLinearSymm.toHomogeneousQuad_add, quadSol (b • (Y n)).1]
@ -144,7 +143,6 @@ lemma add_AF_cube (S : (PlusU1 n).Sols) (a b : ℚ) :
def addCube (S : (PlusU1 n).Sols) (a b : ℚ) : (PlusU1 n).Sols := def addCube (S : (PlusU1 n).Sols) (a b : ℚ) : (PlusU1 n).Sols :=
quadToAF (addQuad S.1 a b) (add_AF_cube S a b) quadToAF (addQuad S.1 a b) (add_AF_cube S a b)
end Y end Y
end PlusU1 end PlusU1
end SMRHN end SMRHN

3
HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean
View file

@ -104,7 +104,6 @@ lemma on_accQuad (f : Fin 11 → ℚ) :
rw [quadBiLin.map_smul₁, Bi_sum_quad, quadCoeff_eq_bilinear] rw [quadBiLin.map_smul₁, Bi_sum_quad, quadCoeff_eq_bilinear]
ring ring
lemma isSolution_quadCoeff_f_sq_zero (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i • B i)) lemma isSolution_quadCoeff_f_sq_zero (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i • B i))
(k : Fin 11) : quadCoeff k * (f k)^2 = 0 := by (k : Fin 11) : quadCoeff k * (f k)^2 = 0 := by
obtain ⟨S, hS⟩ := hS obtain ⟨S, hS⟩ := hS
@ -231,7 +230,6 @@ lemma isSolution_f_zero (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i,
exact isSolution_f9 f hS exact isSolution_f9 f hS
exact isSolution_f10 f hS exact isSolution_f10 f hS
lemma isSolution_only_if_zero (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i • B i)) : lemma isSolution_only_if_zero (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i • B i)) :
∑ i, f i • B i = 0 := by ∑ i, f i • B i = 0 := by
rw [isSolution_sum_part f hS] rw [isSolution_sum_part f hS]
@ -239,7 +237,6 @@ lemma isSolution_only_if_zero (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (
rw [isSolution_f9 f hS] rw [isSolution_f9 f hS]
simp simp
theorem basis_linear_independent : LinearIndependent ℚ B := by theorem basis_linear_independent : LinearIndependent ℚ B := by
apply Fintype.linearIndependent_iff.mpr apply Fintype.linearIndependent_iff.mpr
intro f h intro f h

1
HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSol.lean
View file

@ -74,7 +74,6 @@ lemma genericToQuad_neq_zero (S : (PlusU1 n).QuadSols) (h : α₁ C S.1 ≠ 0) :
(α₁ C S.1)⁻¹ • genericToQuad C S.1 = S := by (α₁ C S.1)⁻¹ • genericToQuad C S.1 = S := by
rw [genericToQuad_on_quad, smul_smul, inv_mul_cancel h, one_smul] rw [genericToQuad_on_quad, smul_smul, inv_mul_cancel h, one_smul]
/-- The construction of a `QuadSol` from a `LinSols` in the special case when `α₁ C S = 0` and /-- The construction of a `QuadSol` from a `LinSols` in the special case when `α₁ C S = 0` and
`α₂ S = 0`. -/ `α₂ S = 0`. -/
def specialToQuad (S : (PlusU1 n).LinSols) (a b : ℚ) (h1 : α₁ C S = 0) def specialToQuad (S : (PlusU1 n).LinSols) (a b : ℚ) (h1 : α₁ C S = 0)

2
HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean
View file

@ -78,10 +78,8 @@ lemma special_on_AF (S : (PlusU1 n).Sols) (h1 : α₁ S.1 = 0) :
rw [BL.addQuad_zero] rw [BL.addQuad_zero]
simp simp
end QuadSolToSol end QuadSolToSol
open QuadSolToSol open QuadSolToSol
/-- A map from `QuadSols × ℚ × ℚ` to `Sols` taking account of the special and generic cases. /-- A map from `QuadSols × ℚ × ℚ` to `Sols` taking account of the special and generic cases.
We will show that this map is a surjection. -/ We will show that this map is a surjection. -/

10
HepLean/FeynmanDiagrams/Basic.lean
View file

@ -22,7 +22,6 @@ import Mathlib.SetTheory.Cardinal.Basic
Feynman diagrams are a graphical representation of the terms in the perturbation expansion of Feynman diagrams are a graphical representation of the terms in the perturbation expansion of
a quantum field theory. a quantum field theory.
-/ -/
open CategoryTheory open CategoryTheory
@ -106,7 +105,6 @@ def preimageEdge {𝓔 𝓥 : Type} (v : 𝓔) :
map {f g} F := Over.homMk ((P.toEdge ⋙ preimageType' v).map F) map {f g} F := Over.homMk ((P.toEdge ⋙ preimageType' v).map F)
(funext <| fun x => congrArg Prod.fst <| congrFun F.w x.1) (funext <| fun x => congrArg Prod.fst <| congrFun F.w x.1)
/-! /-!
## Finitness of pre-Feynman rules ## Finitness of pre-Feynman rules
@ -304,7 +302,6 @@ instance diagramEdgePropDecidable
(fun _ => P.preFeynmanRuleDecEq𝓱𝓔) _ _ _)) _ ) _) (fun _ => P.preFeynmanRuleDecEq𝓱𝓔) _ _ _)) _ ) _)
(P.diagramEdgeProp_iff F f).symm (P.diagramEdgeProp_iff F f).symm
end PreFeynmanRule end PreFeynmanRule
/-! /-!
@ -378,7 +375,6 @@ instance CondDecidable [IsFinitePreFeynmanRule P] {𝓔 𝓥 𝓱𝓔 : Type} (
(@diagramEdgePropDecidable P _ _ _ _ _ (Over.mk 𝓱𝓔To𝓔𝓥) _ h 𝓔𝓞) (@diagramEdgePropDecidable P _ _ _ _ _ (Over.mk 𝓱𝓔To𝓔𝓥) _ h 𝓔𝓞)
(@diagramVertexPropDecidable P _ _ _ _ _ (Over.mk 𝓱𝓔To𝓔𝓥) _ h 𝓥𝓞) (@diagramVertexPropDecidable P _ _ _ _ _ (Over.mk 𝓱𝓔To𝓔𝓥) _ h 𝓥𝓞)
/-- Making a Feynman diagram from maps of edges, vertices and half-edges. -/ /-- Making a Feynman diagram from maps of edges, vertices and half-edges. -/
def mk' {𝓔 𝓥 𝓱𝓔 : Type} (𝓔𝓞 : 𝓔 → P.EdgeLabel) (𝓥𝓞 : 𝓥 → P.VertexLabel) def mk' {𝓔 𝓥 𝓱𝓔 : Type} (𝓔𝓞 : 𝓔 → P.EdgeLabel) (𝓥𝓞 : 𝓥 → P.VertexLabel)
(𝓱𝓔To𝓔𝓥 : 𝓱𝓔 → P.HalfEdgeLabel × 𝓔 × 𝓥) (𝓱𝓔To𝓔𝓥 : 𝓱𝓔 → P.HalfEdgeLabel × 𝓔 × 𝓥)
@ -491,7 +487,6 @@ structure Hom (F G : FeynmanDiagram P) where
/-- The morphism of half-edge objects. -/ /-- The morphism of half-edge objects. -/
𝓱𝓔To𝓔𝓥 : (edgeVertexFunc 𝓔𝓞.left 𝓥𝓞.left).obj F.𝓱𝓔To𝓔𝓥 ⟶ G.𝓱𝓔To𝓔𝓥 𝓱𝓔To𝓔𝓥 : (edgeVertexFunc 𝓔𝓞.left 𝓥𝓞.left).obj F.𝓱𝓔To𝓔𝓥 ⟶ G.𝓱𝓔To𝓔𝓥
namespace Hom namespace Hom
variable {F G : FeynmanDiagram P} variable {F G : FeynmanDiagram P}
variable (f : Hom F G) variable (f : Hom F G)
@ -508,12 +503,10 @@ def 𝓥 : F.𝓥 → G.𝓥 := f.𝓥𝓞.left
@[simp] @[simp]
def 𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔 := f.𝓱𝓔To𝓔𝓥.left def 𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔 := f.𝓱𝓔To𝓔𝓥.left
/-- The morphism `F.𝓱𝓔𝓞 ⟶ G.𝓱𝓔𝓞` induced by a homomorphism of Feynman diagrams. -/ /-- The morphism `F.𝓱𝓔𝓞 ⟶ G.𝓱𝓔𝓞` induced by a homomorphism of Feynman diagrams. -/
@[simp] @[simp]
def 𝓱𝓔𝓞 : F.𝓱𝓔𝓞 ⟶ G.𝓱𝓔𝓞 := P.toHalfEdge.map f.𝓱𝓔To𝓔𝓥 def 𝓱𝓔𝓞 : F.𝓱𝓔𝓞 ⟶ G.𝓱𝓔𝓞 := P.toHalfEdge.map f.𝓱𝓔To𝓔𝓥
/-- The identity morphism for a Feynman diagram. -/ /-- The identity morphism for a Feynman diagram. -/
def id (F : FeynmanDiagram P) : Hom F F where def id (F : FeynmanDiagram P) : Hom F F where
𝓔𝓞 := 𝟙 F.𝓔𝓞 𝓔𝓞 := 𝟙 F.𝓔𝓞
@ -579,7 +572,6 @@ instance {F G : FeynmanDiagram P} [IsFiniteDiagram F] [IsFiniteDiagram G] [IsFin
(𝓔 : F.𝓔 → G.𝓔) (𝓥 : F.𝓥 → G.𝓥) (𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔) : Decidable (Cond 𝓔 𝓥 𝓱𝓔) := (𝓔 : F.𝓔 → G.𝓔) (𝓥 : F.𝓥 → G.𝓥) (𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔) : Decidable (Cond 𝓔 𝓥 𝓱𝓔) :=
And.decidable And.decidable
/-- Making a Feynman diagram from maps of edges, vertices and half-edges. -/ /-- Making a Feynman diagram from maps of edges, vertices and half-edges. -/
@[simps! 𝓔𝓞_left 𝓥𝓞_left 𝓱𝓔To𝓔𝓥_left] @[simps! 𝓔𝓞_left 𝓥𝓞_left 𝓱𝓔To𝓔𝓥_left]
def mk' {F G : FeynmanDiagram P} (𝓔 : F.𝓔 → G.𝓔) (𝓥 : F.𝓥 → G.𝓥) (𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔) def mk' {F G : FeynmanDiagram P} (𝓔 : F.𝓔 → G.𝓔) (𝓥 : F.𝓥 → G.𝓥) (𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔)
@ -667,7 +659,6 @@ We show that the symmetry factor for a finite Feynman diagram is finite.
/-- The type of isomorphisms of a Feynman diagram. -/ /-- The type of isomorphisms of a Feynman diagram. -/
def SymmetryType : Type := F ≅ F def SymmetryType : Type := F ≅ F
/-- An equivalence between `SymmetryType` and permutation of edges, vertices and half-edges /-- An equivalence between `SymmetryType` and permutation of edges, vertices and half-edges
satisfying `Hom.Cond`. -/ satisfying `Hom.Cond`. -/
def symmetryTypeEquiv : def symmetryTypeEquiv :
@ -728,7 +719,6 @@ instance [IsFiniteDiagram F] : DecidableRel F.AdjRelation := fun _ _ =>
@And.decidable _ _ (instDecidableEq𝓥OfIsFiniteDiagram _ _) @And.decidable _ _ (instDecidableEq𝓥OfIsFiniteDiagram _ _)
(instDecidableEq𝓥OfIsFiniteDiagram _ _)) _ ) _ (instDecidableEq𝓥OfIsFiniteDiagram _ _)) _ ) _
/-- From a Feynman diagram the simple graph showing those vertices which are connected. -/ /-- From a Feynman diagram the simple graph showing those vertices which are connected. -/
def toSimpleGraph : SimpleGraph F.𝓥 where def toSimpleGraph : SimpleGraph F.𝓥 where
Adj := AdjRelation F Adj := AdjRelation F

6
HepLean/FeynmanDiagrams/Instances/ComplexScalar.lean
View file

@ -7,11 +7,8 @@ import HepLean.FeynmanDiagrams.Basic
/-! /-!
# Feynman diagrams in a complex scalar field theory # Feynman diagrams in a complex scalar field theory
-/ -/
namespace PhiFour namespace PhiFour
open CategoryTheory open CategoryTheory
open FeynmanDiagram open FeynmanDiagram
@ -65,7 +62,4 @@ instance : IsFinitePreFeynmanRule complexScalarFeynmanRules where
match v with match v with
| 0 => instDecidableEqFin _ | 0 => instDecidableEqFin _
end PhiFour end PhiFour

4
HepLean/FeynmanDiagrams/Instances/Phi4.lean
View file

@ -10,10 +10,8 @@ import HepLean.FeynmanDiagrams.Basic
The aim of this file is to start building up the theory of Feynman diagrams in the context of The aim of this file is to start building up the theory of Feynman diagrams in the context of
Phi^4 theory. Phi^4 theory.
-/ -/
namespace PhiFour namespace PhiFour
open CategoryTheory open CategoryTheory
open FeynmanDiagram open FeynmanDiagram
@ -45,7 +43,6 @@ instance (a : ℕ) : OfNat phi4PreFeynmanRules.HalfEdgeLabel a where
instance (a : ℕ) : OfNat phi4PreFeynmanRules.VertexLabel a where instance (a : ℕ) : OfNat phi4PreFeynmanRules.VertexLabel a where
ofNat := (a : Fin _) ofNat := (a : Fin _)
instance : IsFinitePreFeynmanRule phi4PreFeynmanRules where instance : IsFinitePreFeynmanRule phi4PreFeynmanRules where
edgeLabelDecidable := instDecidableEqFin _ edgeLabelDecidable := instDecidableEqFin _
vertexLabelDecidable := instDecidableEqFin _ vertexLabelDecidable := instDecidableEqFin _
@ -92,5 +89,4 @@ lemma figureEight_symmetryFactor : symmetryFactor figureEight = 8 := by decide
end Example end Example
end PhiFour end PhiFour

6
HepLean/FeynmanDiagrams/Momentum.lean
View file

@ -26,7 +26,6 @@ vector space.
This section is non-computable as we depend on the norm on `F.HalfEdgeMomenta`. This section is non-computable as we depend on the norm on `F.HalfEdgeMomenta`.
-/ -/
namespace FeynmanDiagram namespace FeynmanDiagram
open CategoryTheory open CategoryTheory
@ -78,7 +77,6 @@ def euclidInner : F.HalfEdgeMomenta →ₗ[ℝ] F.HalfEdgeMomenta →ₗ[ℝ]
simp only [euclidInnerAux_symm, LinearMapClass.map_smul, smul_eq_mul, RingHom.id_apply, simp only [euclidInnerAux_symm, LinearMapClass.map_smul, smul_eq_mul, RingHom.id_apply,
LinearMap.smul_apply] LinearMap.smul_apply]
/-- The type which assocaites to each ege a `1`-dimensional vector space. /-- The type which assocaites to each ege a `1`-dimensional vector space.
Corresponding to that spanned by its total outflowing momentum. -/ Corresponding to that spanned by its total outflowing momentum. -/
def EdgeMomenta : Type := F.𝓔 → ℝ def EdgeMomenta : Type := F.𝓔 → ℝ
@ -87,7 +85,6 @@ instance : AddCommGroup F.EdgeMomenta := Pi.addCommGroup
instance : Module ℝ F.EdgeMomenta := Pi.module _ _ _ instance : Module ℝ F.EdgeMomenta := Pi.module _ _ _
/-- The type which assocaites to each ege a `1`-dimensional vector space. /-- The type which assocaites to each ege a `1`-dimensional vector space.
Corresponding to that spanned by its total inflowing momentum. -/ Corresponding to that spanned by its total inflowing momentum. -/
def VertexMomenta : Type := F.𝓥 → ℝ def VertexMomenta : Type := F.𝓥 → ℝ
@ -119,7 +116,6 @@ instance : AddCommGroup F.EdgeVertexMomenta := DirectSum.instAddCommGroup _
instance : Module ℝ F.EdgeVertexMomenta := DirectSum.instModule instance : Module ℝ F.EdgeVertexMomenta := DirectSum.instModule
/-! /-!
## Linear maps between the vector spaces. ## Linear maps between the vector spaces.
@ -199,7 +195,6 @@ for specific Feynman diagrams.
- Complete this section. - Complete this section.
-/ -/
/-! /-!
@ -210,7 +205,6 @@ for specific Feynman diagrams.
- Complete this section. - Complete this section.
-/ -/
end FeynmanDiagram end FeynmanDiagram

7
HepLean/FlavorPhysics/CKMMatrix/Basic.lean
View file

@ -17,12 +17,10 @@ related by phase shifts.
The notation `[V]ud` etc can be used for the elements of a CKM matrix, and The notation `[V]ud` etc can be used for the elements of a CKM matrix, and
`[V]ud|us` etc for the ratios of elements. `[V]ud|us` etc for the ratios of elements.
-/ -/
open Matrix Complex open Matrix Complex
noncomputable section noncomputable section
/-- Given three real numbers `a b c` the complex matrix with `exp (I * a)` etc on the /-- Given three real numbers `a b c` the complex matrix with `exp (I * a)` etc on the
@ -107,7 +105,6 @@ lemma phaseShiftRelation_trans {U V W : unitaryGroup (Fin 3) ℂ} :
rw [phaseShiftMatrix_mul] rw [phaseShiftMatrix_mul]
rw [add_comm k e, add_comm l f, add_comm m g] rw [add_comm k e, add_comm l f, add_comm m g]
lemma phaseShiftRelation_equiv : Equivalence PhaseShiftRelation where lemma phaseShiftRelation_equiv : Equivalence PhaseShiftRelation where
refl := phaseShiftRelation_refl refl := phaseShiftRelation_refl
symm := phaseShiftRelation_symm symm := phaseShiftRelation_symm
@ -270,7 +267,6 @@ lemma tb (V : CKMMatrix) (a b c d e f : ℝ) :
end phaseShiftApply end phaseShiftApply
/-- The aboslute value of the `(i,j)`th element of `V`. -/ /-- The aboslute value of the `(i,j)`th element of `V`. -/
@[simp] @[simp]
def VAbs' (V : unitaryGroup (Fin 3) ℂ) (i j : Fin 3) : ℝ := Complex.abs (V i j) def VAbs' (V : unitaryGroup (Fin 3) ℂ) (i j : Fin 3) : ℝ := Complex.abs (V i j)
@ -341,11 +337,9 @@ abbrev VtsAbs := VAbs 2 1
@[simp] @[simp]
abbrev VtbAbs := VAbs 2 2 abbrev VtbAbs := VAbs 2 2
namespace CKMMatrix namespace CKMMatrix
open ComplexConjugate open ComplexConjugate
section ratios section ratios
/-- The ratio of the `ub` and `ud` elements of a CKM matrix. -/ /-- The ratio of the `ub` and `ud` elements of a CKM matrix. -/
@ -394,7 +388,6 @@ lemma Rcscb_mul_cb {V : CKMMatrix} (h : [V]cb ≠ 0): [V]cs = Rcscb V * [V]cb :=
end ratios end ratios
end CKMMatrix end CKMMatrix
end end

4
HepLean/FlavorPhysics/CKMMatrix/Invariants.lean
View file

@ -15,17 +15,14 @@ this equivalence.
Of note, this file defines the complex jarlskog invariant. Of note, this file defines the complex jarlskog invariant.
-/ -/
open Matrix Complex open Matrix Complex
open ComplexConjugate open ComplexConjugate
open CKMMatrix open CKMMatrix
noncomputable section noncomputable section
namespace Invariant namespace Invariant
/-- The complex jarlskog invariant for a CKM matrix. -/ /-- The complex jarlskog invariant for a CKM matrix. -/
@[simps!] @[simps!]
def jarlskogℂCKM (V : CKMMatrix) : ℂ := def jarlskogℂCKM (V : CKMMatrix) : ℂ :=
@ -62,6 +59,5 @@ standard parameterization. -/
def mulExpδ₁₃ (V : Quotient CKMMatrixSetoid) : ℂ := def mulExpδ₁₃ (V : Quotient CKMMatrixSetoid) : ℂ :=
jarlskogℂ V + VusVubVcdSq V jarlskogℂ V + VusVubVcdSq V
end Invariant end Invariant
end end

3
HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean
View file

@ -19,11 +19,9 @@ In this file we define two sets of conditions on the CKM matrices
and `ubOnePhaseCond` which we show can be satisfied by any CKM matrix up to equivalence as long as and `ubOnePhaseCond` which we show can be satisfied by any CKM matrix up to equivalence as long as
the ub element as absolute value 1. the ub element as absolute value 1.
-/ -/
open Matrix Complex open Matrix Complex
noncomputable section noncomputable section
namespace CKMMatrix namespace CKMMatrix
open ComplexConjugate open ComplexConjugate
@ -260,7 +258,6 @@ lemma fstRowThdColRealCond_holds_up_to_equiv (V : CKMMatrix) :
apply shift_cross_product_phase_zero _ _ _ _ _ _ hτ.symm apply shift_cross_product_phase_zero _ _ _ _ _ _ hτ.symm
ring ring
lemma ubOnePhaseCond_hold_up_to_equiv_of_ub_one {V : CKMMatrix} (hb : ¬ ([V]ud ≠ 0 ∨ [V]us ≠ 0)) lemma ubOnePhaseCond_hold_up_to_equiv_of_ub_one {V : CKMMatrix} (hb : ¬ ([V]ud ≠ 0 ∨ [V]us ≠ 0))
(hV : FstRowThdColRealCond V) : (hV : FstRowThdColRealCond V) :
∃ (U : CKMMatrix), V ≈ U ∧ ubOnePhaseCond U:= by ∃ (U : CKMMatrix), V ≈ U ∧ ubOnePhaseCond U:= by

13
HepLean/FlavorPhysics/CKMMatrix/Relations.lean
View file

@ -16,7 +16,6 @@ matrix.
open Matrix Complex open Matrix Complex
noncomputable section noncomputable section
namespace CKMMatrix namespace CKMMatrix
@ -121,9 +120,6 @@ lemma VAbsub_neq_zero_sqrt_Vud_Vus_neq_zero {V : Quotient CKMMatrixSetoid}
rw [← ud_us_neq_zero_iff_ub_neq_one V] at hV rw [← ud_us_neq_zero_iff_ub_neq_one V] at hV
simpa [← Complex.sq_abs] using (normSq_Vud_plus_normSq_Vus_neq_zero_ℝ hV) simpa [← Complex.sq_abs] using (normSq_Vud_plus_normSq_Vus_neq_zero_ℝ hV)
lemma normSq_Vud_plus_normSq_Vus_neq_zero_ℂ {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) : lemma normSq_Vud_plus_normSq_Vus_neq_zero_ℂ {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) :
(normSq [V]ud : ℂ) + normSq [V]us ≠ 0 := by (normSq [V]ud : ℂ) + normSq [V]us ≠ 0 := by
have h1 := normSq_Vud_plus_normSq_Vus_neq_zero_ℝ hb have h1 := normSq_Vud_plus_normSq_Vus_neq_zero_ℝ hb
@ -131,7 +127,6 @@ lemma normSq_Vud_plus_normSq_Vus_neq_zero_ℂ {V : CKMMatrix} (hb : [V]ud ≠ 0
rw [← ofReal_inj] at h1 rw [← ofReal_inj] at h1
simp_all simp_all
lemma Vabs_sq_add_neq_zero {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) : lemma Vabs_sq_add_neq_zero {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) :
((VudAbs ⟦V⟧ : ℂ) * ↑(VudAbs ⟦V⟧) + ↑(VusAbs ⟦V⟧) * ↑(VusAbs ⟦V⟧)) ≠ 0 := by ((VudAbs ⟦V⟧ : ℂ) * ↑(VudAbs ⟦V⟧) + ↑(VusAbs ⟦V⟧) * ↑(VusAbs ⟦V⟧)) ≠ 0 := by
have h1 := normSq_Vud_plus_normSq_Vus_neq_zero_ℂ hb have h1 := normSq_Vud_plus_normSq_Vus_neq_zero_ℂ hb
@ -230,7 +225,6 @@ lemma conj_Vtb_mul_Vus {V : CKMMatrix} {τ : ℝ}
simp only [Fin.isValue, neg_mul] simp only [Fin.isValue, neg_mul]
ring ring
lemma cs_of_ud_us_ub_cb_tb {V : CKMMatrix} (h : [V]ud ≠ 0 ∨ [V]us ≠ 0) lemma cs_of_ud_us_ub_cb_tb {V : CKMMatrix} (h : [V]ud ≠ 0 ∨ [V]us ≠ 0)
{τ : ℝ} (hτ : [V]t = cexp (τ * I) • (conj ([V]u) ×₃ conj ([V]c))) : {τ : ℝ} (hτ : [V]t = cexp (τ * I) • (conj ([V]u) ×₃ conj ([V]c))) :
[V]cs = (- conj [V]ub * [V]us * [V]cb + [V]cs = (- conj [V]ub * [V]us * [V]cb +
@ -249,10 +243,8 @@ lemma cd_of_ud_us_ub_cb_tb {V : CKMMatrix} (h : [V]ud ≠ 0 ∨ [V]us ≠ 0)
field_simp field_simp
ring ring
end rows end rows
section individual section individual
lemma VAbs_ge_zero (i j : Fin 3) (V : Quotient CKMMatrixSetoid) : 0 ≤ VAbs i j V := by lemma VAbs_ge_zero (i j : Fin 3) (V : Quotient CKMMatrixSetoid) : 0 ≤ VAbs i j V := by
@ -270,12 +262,10 @@ lemma VAbs_leq_one (i j : Fin 3) (V : Quotient CKMMatrixSetoid) : VAbs i j V ≤
change VAbs i 2 V ≤ 1 change VAbs i 2 V ≤ 1
nlinarith nlinarith
end individual end individual
section columns section columns
lemma VAbs_sum_sq_col_eq_one (V : Quotient CKMMatrixSetoid) (i : Fin 3) : lemma VAbs_sum_sq_col_eq_one (V : Quotient CKMMatrixSetoid) (i : Fin 3) :
(VAbs 0 i V) ^ 2 + (VAbs 1 i V) ^ 2 + (VAbs 2 i V) ^ 2 = 1 := by (VAbs 0 i V) ^ 2 + (VAbs 1 i V) ^ 2 + (VAbs 2 i V) ^ 2 = 1 := by
obtain ⟨V, hV⟩ := Quot.exists_rep V obtain ⟨V, hV⟩ := Quot.exists_rep V
@ -312,7 +302,6 @@ lemma cb_eq_zero_of_ud_us_zero {V : CKMMatrix} (h : [V]ud = 0 ∧ [V]us = 0) :
simp at h1 simp at h1
exact h1.1 exact h1.1
lemma cs_of_ud_us_zero {V : CKMMatrix} (ha : ¬ ([V]ud ≠ 0 ∨ [V]us ≠ 0)) : lemma cs_of_ud_us_zero {V : CKMMatrix} (ha : ¬ ([V]ud ≠ 0 ∨ [V]us ≠ 0)) :
VcsAbs ⟦V⟧ = √(1 - VcdAbs ⟦V⟧ ^ 2) := by VcsAbs ⟦V⟧ = √(1 - VcdAbs ⟦V⟧ ^ 2) := by
have h1 := snd_row_normalized_abs V have h1 := snd_row_normalized_abs V
@ -336,8 +325,6 @@ lemma VcbAbs_sq_add_VtbAbs_sq (V : Quotient CKMMatrixSetoid) :
VcbAbs V ^ 2 + VtbAbs V ^ 2 = 1 - VubAbs V ^2 := by VcbAbs V ^ 2 + VtbAbs V ^ 2 = 1 - VubAbs V ^2 := by
linear_combination (VAbs_sum_sq_col_eq_one V 2) linear_combination (VAbs_sum_sq_col_eq_one V 2)
lemma cb_tb_neq_zero_iff_ub_neq_one (V : CKMMatrix) : lemma cb_tb_neq_zero_iff_ub_neq_one (V : CKMMatrix) :
[V]cb ≠ 0 ∨ [V]tb ≠ 0 ↔ abs [V]ub ≠ 1 := by [V]cb ≠ 0 ∨ [V]tb ≠ 0 ↔ abs [V]ub ≠ 1 := by
have h2 := V.thd_col_normalized_abs have h2 := V.thd_col_normalized_abs

2
HepLean/FlavorPhysics/CKMMatrix/Rows.lean
View file

@ -14,7 +14,6 @@ proves some properties between them.
The first row can be extracted as `[V]u` for a CKM matrix `V`. The first row can be extracted as `[V]u` for a CKM matrix `V`.
-/ -/
open Matrix Complex open Matrix Complex
@ -24,7 +23,6 @@ noncomputable section
namespace CKMMatrix namespace CKMMatrix
/-- The `u`th row of the CKM matrix. -/ /-- The `u`th row of the CKM matrix. -/
def uRow (V : CKMMatrix) : Fin 3 → ℂ := ![[V]ud, [V]us, [V]ub] def uRow (V : CKMMatrix) : Fin 3 → ℂ := ![[V]ud, [V]us, [V]ub]

3
HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean
View file

@ -16,7 +16,6 @@ four real numbers `θ₁₂`, `θ₁₃`, `θ₂₃` and `δ₁₃`.
We will show that every CKM matrix can be written within this standard parameterization We will show that every CKM matrix can be written within this standard parameterization
in the file `FlavorPhysics.CKMMatrix.StandardParameters`. in the file `FlavorPhysics.CKMMatrix.StandardParameters`.
-/ -/
open Matrix Complex open Matrix Complex
open ComplexConjugate open ComplexConjugate
@ -194,7 +193,5 @@ lemma mulExpδ₁₃_eq (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) (h1 : 0 ≤
have h1 : cexp (I * δ₁₃) ≠ 0 := exp_ne_zero _ have h1 : cexp (I * δ₁₃) ≠ 0 := exp_ne_zero _
field_simp field_simp
end standParam end standParam
end end

16
HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean
View file

@ -18,7 +18,6 @@ These, when used in the standard parameterization return `V` up to equivalence.
This leads to the theorem `standParam.exists_for_CKMatrix` which says that up to equivalence every This leads to the theorem `standParam.exists_for_CKMatrix` which says that up to equivalence every
CKM matrix can be written using the standard parameterization. CKM matrix can be written using the standard parameterization.
-/ -/
open Matrix Complex open Matrix Complex
open ComplexConjugate open ComplexConjugate
@ -333,7 +332,6 @@ lemma Vs_zero_iff_cos_sin_zero (V : CKMMatrix) :
end VAbs end VAbs
namespace standParam namespace standParam
open Invariant open Invariant
@ -409,7 +407,6 @@ lemma on_param_cos_θ₁₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.c
rfl rfl
rfl rfl
lemma on_param_cos_θ₁₂_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.cos (θ₁₂ ⟦V⟧) = 0) : lemma on_param_cos_θ₁₂_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.cos (θ₁₂ ⟦V⟧) = 0) :
standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by
use 0, δ₁₃, δ₁₃, -δ₁₃, 0, - δ₁₃ use 0, δ₁₃, δ₁₃, -δ₁₃, 0, - δ₁₃
@ -434,7 +431,6 @@ lemma on_param_cos_θ₁₂_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.c
ring_nf ring_nf
field_simp field_simp
lemma on_param_cos_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.cos (θ₂₃ ⟦V⟧) = 0) : lemma on_param_cos_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.cos (θ₂₃ ⟦V⟧) = 0) :
standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by
use 0, δ₁₃, 0, 0, 0, - δ₁₃ use 0, δ₁₃, 0, 0, 0, - δ₁₃
@ -451,7 +447,6 @@ lemma on_param_cos_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.c
ring ring
field_simp field_simp
lemma on_param_sin_θ₁₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.sin (θ₁₃ ⟦V⟧) = 0) : lemma on_param_sin_θ₁₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.sin (θ₁₃ ⟦V⟧) = 0) :
standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by
use 0, 0, 0, 0, 0, 0 use 0, 0, 0, 0, 0, 0
@ -488,8 +483,6 @@ lemma on_param_sin_θ₁₂_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.s
ring_nf ring_nf
field_simp field_simp
lemma on_param_sin_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.sin (θ₂₃ ⟦V⟧) = 0) : lemma on_param_sin_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.sin (θ₂₃ ⟦V⟧) = 0) :
standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by
use 0, 0, δ₁₃, 0, 0, - δ₁₃ use 0, 0, δ₁₃, 0, 0, - δ₁₃
@ -506,9 +499,6 @@ lemma on_param_sin_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.s
ring ring
field_simp field_simp
lemma eq_standParam_of_fstRowThdColRealCond {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0) lemma eq_standParam_of_fstRowThdColRealCond {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0)
(hV : FstRowThdColRealCond V) : V = standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) (- arg [V]ub) := by (hV : FstRowThdColRealCond V) : V = standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) (- arg [V]ub) := by
have hb' : VubAbs ⟦V⟧ ≠ 1 := by have hb' : VubAbs ⟦V⟧ ≠ 1 := by
@ -565,7 +555,6 @@ lemma eq_standParam_of_fstRowThdColRealCond {V : CKMMatrix} (hb : [V]ud ≠ 0
rw [VcbAbs_eq_S₂₃_mul_C₁₃ ⟦V⟧, S₂₃_eq_ℂsin_θ₂₃ ⟦V⟧, C₁₃] rw [VcbAbs_eq_S₂₃_mul_C₁₃ ⟦V⟧, S₂₃_eq_ℂsin_θ₂₃ ⟦V⟧, C₁₃]
simp simp
lemma eq_standParam_of_ubOnePhaseCond {V : CKMMatrix} (hV : ubOnePhaseCond V) : lemma eq_standParam_of_ubOnePhaseCond {V : CKMMatrix} (hV : ubOnePhaseCond V) :
V = standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by V = standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by
have h1 : VubAbs ⟦V⟧ = 1 := by have h1 : VubAbs ⟦V⟧ = 1 := by
@ -610,7 +599,6 @@ lemma eq_standParam_of_ubOnePhaseCond {V : CKMMatrix} (hV : ubOnePhaseCond V) :
rw [C₁₃_eq_ℂcos_θ₁₃ ⟦V⟧, C₁₃_of_Vub_eq_one h1, hV.2.2.1] rw [C₁₃_eq_ℂcos_θ₁₃ ⟦V⟧, C₁₃_of_Vub_eq_one h1, hV.2.2.1]
simp simp
theorem exists_δ₁₃ (V : CKMMatrix) : theorem exists_δ₁₃ (V : CKMMatrix) :
∃ (δ₃ : ℝ), V ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₃ := by ∃ (δ₃ : ℝ), V ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₃ := by
obtain ⟨U, hU⟩ := fstRowThdColRealCond_holds_up_to_equiv V obtain ⟨U, hU⟩ := fstRowThdColRealCond_holds_up_to_equiv V
@ -670,7 +658,6 @@ theorem eq_standardParameterization_δ₃ (V : CKMMatrix) :
exact on_param_sin_θ₁₃_eq_zero δ₁₃' h exact on_param_sin_θ₁₃_eq_zero δ₁₃' h
exact on_param_sin_θ₂₃_eq_zero δ₁₃' h exact on_param_sin_θ₂₃_eq_zero δ₁₃' h
theorem exists_for_CKMatrix (V : CKMMatrix) : theorem exists_for_CKMatrix (V : CKMMatrix) :
∃ (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ), V ≈ standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃ := by ∃ (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ), V ≈ standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃ := by
use θ₁₂ ⟦V⟧, θ₁₃ ⟦V⟧, θ₂₃ ⟦V⟧, δ₁₃ ⟦V⟧ use θ₁₂ ⟦V⟧, θ₁₃ ⟦V⟧, θ₂₃ ⟦V⟧, δ₁₃ ⟦V⟧
@ -678,9 +665,6 @@ theorem exists_for_CKMatrix (V : CKMMatrix) :
end standParam end standParam
open CKMMatrix open CKMMatrix
end end

5
HepLean/Mathematics/LinearMaps.lean
View file

@ -40,7 +40,6 @@ lemma map_smul (f : HomogeneousQuadratic V) (a : ℚ) (S : V) : f (a • S) = a
end HomogeneousQuadratic end HomogeneousQuadratic
/-- The structure of a symmetric bilinear function. -/ /-- The structure of a symmetric bilinear function. -/
structure BiLinearSymm (V : Type) [AddCommMonoid V] [Module ℚ V] extends V →ₗ[ℚ] V →ₗ[ℚ] ℚ where structure BiLinearSymm (V : Type) [AddCommMonoid V] [Module ℚ V] extends V →ₗ[ℚ] V →ₗ[ℚ] ℚ where
swap' : ∀ S T, toFun S T = toFun T S swap' : ∀ S T, toFun S T = toFun T S
@ -126,7 +125,6 @@ lemma map_sum₂ {n : ℕ} (f : BiLinearSymm V) (S : Fin n → V) (T : V) :
intro i intro i
rw [swap] rw [swap]
/-- The homogenous quadratic equation obtainable from a bilinear function. -/ /-- The homogenous quadratic equation obtainable from a bilinear function. -/
@[simps!] @[simps!]
def toHomogeneousQuad {V : Type} [AddCommMonoid V] [Module ℚ V] def toHomogeneousQuad {V : Type} [AddCommMonoid V] [Module ℚ V]
@ -146,7 +144,6 @@ lemma toHomogeneousQuad_add {V : Type} [AddCommMonoid V] [Module ℚ V]
rw [τ.map_add₁, τ.map_add₁, τ.swap T S] rw [τ.map_add₁, τ.map_add₁, τ.swap T S]
ring ring
end BiLinearSymm end BiLinearSymm
/-- The structure of a homogeneous cubic equation. -/ /-- The structure of a homogeneous cubic equation. -/
@ -222,7 +219,6 @@ def mk₃ (f : V × V × V→ ℚ) (map_smul : ∀ a S T L, f (a • S, T, L) =
swap₁' := swap₁ swap₁' := swap₁
swap₂' := swap₂ swap₂' := swap₂
lemma swap₁ (f : TriLinearSymm V) (S T L : V) : f S T L = f T S L := lemma swap₁ (f : TriLinearSymm V) (S T L : V) : f S T L = f T S L :=
f.swap₁' S T L f.swap₁' S T L
@ -300,7 +296,6 @@ lemma map_sum₁₂₃ {n1 n2 n3 : ℕ} (f : TriLinearSymm V) (S : Fin n1 → V)
intro i intro i
rw [map_sum₃] rw [map_sum₃]
/-- The homogenous cubic equation obtainable from a symmetric trilinear function. -/ /-- The homogenous cubic equation obtainable from a symmetric trilinear function. -/
@[simps!] @[simps!]
def toCubic {charges : Type} [AddCommMonoid charges] [Module ℚ charges] def toCubic {charges : Type} [AddCommMonoid charges] [Module ℚ charges]

5
HepLean/Mathematics/SO3/Basic.lean
View file

@ -11,7 +11,6 @@ import Mathlib.Analysis.InnerProductSpace.PiL2
/-! /-!
# The group SO(3) # The group SO(3)
-/ -/
namespace GroupTheory namespace GroupTheory
@ -107,7 +106,6 @@ lemma toProd_continuous : Continuous toProd := by
refine Continuous.matrix_transpose ?_ refine Continuous.matrix_transpose ?_
exact continuous_iff_le_induced.mpr fun U a => a exact continuous_iff_le_induced.mpr fun U a => a
/-- The embedding of `SO(3)` into the monoid of matrices times the opposite of /-- The embedding of `SO(3)` into the monoid of matrices times the opposite of
the monoid of matrices. -/ the monoid of matrices. -/
lemma toProd_embedding : Embedding toProd where lemma toProd_embedding : Embedding toProd where
@ -223,10 +221,7 @@ lemma exists_basis_preserved (A : SO(3)) :
use b use b
rw [hb, hv.2] rw [hb, hv.2]
end action end action
end SO3 end SO3
end GroupTheory end GroupTheory

1
HepLean/SpaceTime/Basic.lean
View file

@ -29,7 +29,6 @@ instance euclideanNormedAddCommGroup : NormedAddCommGroup SpaceTime := Pi.normed
instance euclideanNormedSpace : NormedSpace ℝ SpaceTime := Pi.normedSpace instance euclideanNormedSpace : NormedSpace ℝ SpaceTime := Pi.normedSpace
namespace SpaceTime namespace SpaceTime
open Manifold open Manifold

8
HepLean/SpaceTime/LorentzAlgebra/Basic.lean
View file

@ -17,7 +17,6 @@ We define
-/ -/
namespace SpaceTime namespace SpaceTime
open Matrix open Matrix
open TensorProduct open TensorProduct
@ -34,7 +33,6 @@ lemma transpose_eta (A : lorentzAlgebra) : A.1ᵀ * η = - η * A.1 := by
erw [mem_skewAdjointMatricesLieSubalgebra] at h1 erw [mem_skewAdjointMatricesLieSubalgebra] at h1
simpa [LieAlgebra.Orthogonal.so', IsSkewAdjoint, IsAdjointPair] using h1 simpa [LieAlgebra.Orthogonal.so', IsSkewAdjoint, IsAdjointPair] using h1
lemma mem_of_transpose_eta_eq_eta_mul_self {A : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ} lemma mem_of_transpose_eta_eq_eta_mul_self {A : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ}
(h : Aᵀ * η = - η * A) : A ∈ lorentzAlgebra := by (h : Aᵀ * η = - η * A) : A ∈ lorentzAlgebra := by
erw [mem_skewAdjointMatricesLieSubalgebra] erw [mem_skewAdjointMatricesLieSubalgebra]
@ -58,7 +56,6 @@ lemma mem_iff' (A : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ) :
rw [minkowskiMatrix.sq] rw [minkowskiMatrix.sq]
all_goals noncomm_ring all_goals noncomm_ring
lemma diag_comp (Λ : lorentzAlgebra) (μ : Fin 1 ⊕ Fin 3) : Λ.1 μ μ = 0 := by lemma diag_comp (Λ : lorentzAlgebra) (μ : Fin 1 ⊕ Fin 3) : Λ.1 μ μ = 0 := by
have h := congrArg (fun M ↦ M μ μ) $ mem_iff.mp Λ.2 have h := congrArg (fun M ↦ M μ μ) $ mem_iff.mp Λ.2
simp only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, mul_diagonal, simp only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, mul_diagonal,
@ -67,22 +64,18 @@ lemma diag_comp (Λ : lorentzAlgebra) (μ : Fin 1 ⊕ Fin 3) : Λ.1 μ μ = 0 :=
simpa using h simpa using h
simpa using h simpa using h
lemma time_comps (Λ : lorentzAlgebra) (i : Fin 3) : lemma time_comps (Λ : lorentzAlgebra) (i : Fin 3) :
Λ.1 (Sum.inr i) (Sum.inl 0) = Λ.1 (Sum.inl 0) (Sum.inr i) := by Λ.1 (Sum.inr i) (Sum.inl 0) = Λ.1 (Sum.inl 0) (Sum.inr i) := by
simpa only [Fin.isValue, minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, mul_diagonal, simpa only [Fin.isValue, minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, mul_diagonal,
transpose_apply, Sum.elim_inr, mul_neg, mul_one, diagonal_neg, diagonal_mul, Sum.elim_inl, transpose_apply, Sum.elim_inr, mul_neg, mul_one, diagonal_neg, diagonal_mul, Sum.elim_inl,
neg_mul, one_mul, neg_inj] using congrArg (fun M ↦ M (Sum.inl 0) (Sum.inr i)) $ mem_iff.mp Λ.2 neg_mul, one_mul, neg_inj] using congrArg (fun M ↦ M (Sum.inl 0) (Sum.inr i)) $ mem_iff.mp Λ.2
lemma space_comps (Λ : lorentzAlgebra) (i j : Fin 3) : lemma space_comps (Λ : lorentzAlgebra) (i j : Fin 3) :
Λ.1 (Sum.inr i) (Sum.inr j) = - Λ.1 (Sum.inr j) (Sum.inr i) := by Λ.1 (Sum.inr i) (Sum.inr j) = - Λ.1 (Sum.inr j) (Sum.inr i) := by
simpa only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, diagonal_neg, diagonal_mul, simpa only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, diagonal_neg, diagonal_mul,
Sum.elim_inr, neg_neg, one_mul, mul_diagonal, transpose_apply, mul_neg, mul_one] using Sum.elim_inr, neg_neg, one_mul, mul_diagonal, transpose_apply, mul_neg, mul_one] using
(congrArg (fun M ↦ M (Sum.inr i) (Sum.inr j)) $ mem_iff.mp Λ.2).symm (congrArg (fun M ↦ M (Sum.inr i) (Sum.inr j)) $ mem_iff.mp Λ.2).symm
end lorentzAlgebra end lorentzAlgebra
@[simps!] @[simps!]
@ -104,5 +97,4 @@ instance spaceTimeAsLieModule : LieModule ℝ lorentzAlgebra (LorentzVector 3) w
simp [Bracket.bracket] simp [Bracket.bracket]
rw [mulVec_smul] rw [mulVec_smul]
end SpaceTime end SpaceTime

1
HepLean/SpaceTime/LorentzGroup/Basic.lean
View file

@ -44,7 +44,6 @@ def LorentzGroup (d : ℕ) : Set (Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ
{Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ | {Λ : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ |
∀ (x y : LorentzVector d), ⟪Λ *ᵥ x, Λ *ᵥ y⟫ₘ = ⟪x, y⟫ₘ} ∀ (x y : LorentzVector d), ⟪Λ *ᵥ x, Λ *ᵥ y⟫ₘ = ⟪x, y⟫ₘ}
namespace LorentzGroup namespace LorentzGroup
/-- Notation for the Lorentz group. -/ /-- Notation for the Lorentz group. -/
scoped[LorentzGroup] notation (name := lorentzGroup_notation) "𝓛" => LorentzGroup scoped[LorentzGroup] notation (name := lorentzGroup_notation) "𝓛" => LorentzGroup

4
HepLean/SpaceTime/LorentzGroup/Boosts.lean
View file

@ -140,7 +140,6 @@ lemma toMatrix_continuous (u : FuturePointing d) : Continuous (toMatrix u) := by
exact FuturePointing.metric_continuous _ exact FuturePointing.metric_continuous _
exact fun x => FuturePointing.one_add_metric_non_zero u x exact fun x => FuturePointing.one_add_metric_non_zero u x
lemma toMatrix_in_lorentzGroup (u v : FuturePointing d) : (toMatrix u v) ∈ LorentzGroup d:= by lemma toMatrix_in_lorentzGroup (u v : FuturePointing d) : (toMatrix u v) ∈ LorentzGroup d:= by
intro x y intro x y
rw [toMatrix_mulVec, toMatrix_mulVec, genBoost, genBoostAux₁, genBoostAux₂] rw [toMatrix_mulVec, toMatrix_mulVec, genBoost, genBoostAux₁, genBoostAux₂]
@ -161,7 +160,6 @@ lemma toLorentz_continuous (u : FuturePointing d) : Continuous (toLorentz u) :=
refine Continuous.subtype_mk ?_ (fun x => toMatrix_in_lorentzGroup u x) refine Continuous.subtype_mk ?_ (fun x => toMatrix_in_lorentzGroup u x)
exact toMatrix_continuous u exact toMatrix_continuous u
lemma toLorentz_joined_to_1 (u v : FuturePointing d) : Joined 1 (toLorentz u v) := by lemma toLorentz_joined_to_1 (u v : FuturePointing d) : Joined 1 (toLorentz u v) := by
obtain ⟨f, _⟩ := FuturePointing.isPathConnected.joinedIn u trivial v trivial obtain ⟨f, _⟩ := FuturePointing.isPathConnected.joinedIn u trivial v trivial
use ContinuousMap.comp ⟨toLorentz u, toLorentz_continuous u⟩ f use ContinuousMap.comp ⟨toLorentz u, toLorentz_continuous u⟩ f
@ -180,8 +178,6 @@ lemma isProper (u v : FuturePointing d) : IsProper (toLorentz u v) :=
end genBoost end genBoost
end LorentzGroup end LorentzGroup
end end

3
HepLean/SpaceTime/LorentzGroup/Orthochronous.lean
View file

@ -17,10 +17,8 @@ matrices.
-/ -/
noncomputable section noncomputable section
open Matrix open Matrix
open Complex open Complex
open ComplexConjugate open ComplexConjugate
@ -66,7 +64,6 @@ lemma not_orthochronous_iff_le_zero :
rw [IsOrthochronous_iff_ge_one] rw [IsOrthochronous_iff_ge_one]
linarith linarith
/-- The continuous map taking a Lorentz transformation to its `0 0` element. -/ /-- 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 Λ => timeComp Λ ,
Continuous.matrix_elem (continuous_iff_le_induced.mpr fun _ a => a) (Sum.inl 0) (Sum.inl 0)⟩ Continuous.matrix_elem (continuous_iff_le_induced.mpr fun _ a => a) (Sum.inl 0) (Sum.inl 0)⟩

4
HepLean/SpaceTime/LorentzGroup/Proper.lean
View file

@ -11,10 +11,8 @@ We define the give a series of lemmas related to the determinant of the lorentz
-/ -/
noncomputable section noncomputable section
open Matrix open Matrix
open Complex open Complex
open ComplexConjugate open ComplexConjugate
@ -31,7 +29,6 @@ lemma det_eq_one_or_neg_one (Λ : 𝓛 d) : Λ.1.det = 1 ∨ Λ.1.det = -1 := by
simp [det_mul, det_dual] at h1 simp [det_mul, det_dual] at h1
exact mul_self_eq_one_iff.mp h1 exact mul_self_eq_one_iff.mp h1
local notation "ℤ₂" => Multiplicative (ZMod 2) local notation "ℤ₂" => Multiplicative (ZMod 2)
instance : TopologicalSpace ℤ₂ := instTopologicalSpaceFin instance : TopologicalSpace ℤ₂ := instTopologicalSpaceFin
@ -76,7 +73,6 @@ lemma detContinuous_eq_iff_det_eq (Λ Λ' : LorentzGroup d) :
· intro h · intro h
simp [detContinuous, h] simp [detContinuous, h]
/-- The representation taking a lorentz matrix to its determinant. -/ /-- The representation taking a lorentz matrix to its determinant. -/
@[simps!] @[simps!]
def detRep : 𝓛 d →* ℤ₂ where def detRep : 𝓛 d →* ℤ₂ where

2
HepLean/SpaceTime/LorentzGroup/Rotations.lean
View file

@ -54,8 +54,6 @@ def SO3ToLorentz : SO(3) →* LorentzGroup 3 where
apply Subtype.eq apply Subtype.eq
simp [Matrix.fromBlocks_multiply] simp [Matrix.fromBlocks_multiply]
end LorentzGroup end LorentzGroup
end end

1
HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean
View file

@ -52,7 +52,6 @@ noncomputable def fromSelfAdjointMatrix' (x : selfAdjoint (Matrix (Fin 2) (Fin 2
| Sum.inr 1 => (x.1 1 0).im | Sum.inr 1 => (x.1 1 0).im
| Sum.inr 2 => 1/2 * (x.1 0 0 - x.1 1 1).re | Sum.inr 2 => 1/2 * (x.1 0 0 - x.1 1 1).re
/-- The linear equivalence between the vector-space `spaceTime` and self-adjoint /-- The linear equivalence between the vector-space `spaceTime` and self-adjoint
2×2-complex matrices. -/ 2×2-complex matrices. -/
noncomputable def toSelfAdjointMatrix : noncomputable def toSelfAdjointMatrix :

1
HepLean/SpaceTime/LorentzVector/Basic.lean
View file

@ -77,7 +77,6 @@ lemma timeVec_space : (@timeVec d).space = 0 := by
lemma timeVec_time: (@timeVec d).time = 1 := by lemma timeVec_time: (@timeVec d).time = 1 := by
simp only [time, Fin.isValue, stdBasis_apply, ↓reduceIte] simp only [time, Fin.isValue, stdBasis_apply, ↓reduceIte]
/-! /-!
# Reflection of space # Reflection of space

10
HepLean/SpaceTime/LorentzVector/NormOne.lean
View file

@ -63,7 +63,6 @@ lemma time_nonpos_iff : v.1.time ≤ 0 ↔ v.1.time ≤ - 1 := by
· intro h · intro h
linarith linarith
lemma time_nonneg_iff : 0 ≤ v.1.time ↔ 1 ≤ v.1.time := by lemma time_nonneg_iff : 0 ≤ v.1.time ↔ 1 ≤ v.1.time := by
apply Iff.intro apply Iff.intro
· intro h · intro h
@ -167,14 +166,12 @@ lemma metric_reflect_mem_mem (h : v ∈ FuturePointing d) (hw : w ∈ FuturePoin
apply le_trans (neg_le_abs _ : _ ≤ |⟪(v.1).space, (w.1).space⟫_ℝ|) ?_ apply le_trans (neg_le_abs _ : _ ≤ |⟪(v.1).space, (w.1).space⟫_ℝ|) ?_
exact abs_real_inner_le_norm (v.1).space (w.1).space exact abs_real_inner_le_norm (v.1).space (w.1).space
lemma metric_reflect_not_mem_not_mem (h : v ∉ FuturePointing d) (hw : w ∉ FuturePointing d) : lemma metric_reflect_not_mem_not_mem (h : v ∉ FuturePointing d) (hw : w ∉ FuturePointing d) :
0 ≤ ⟪v.1, w.1.spaceReflection⟫ₘ := by 0 ≤ ⟪v.1, w.1.spaceReflection⟫ₘ := by
have h1 := metric_reflect_mem_mem ((not_mem_iff_neg v).mp h) ((not_mem_iff_neg w).mp hw) 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 ?_ apply le_of_le_of_eq h1 ?_
simp [neg] simp [neg]
lemma metric_reflect_mem_not_mem (h : v ∈ FuturePointing d) (hw : w ∉ FuturePointing d) : lemma metric_reflect_mem_not_mem (h : v ∈ FuturePointing d) (hw : w ∉ FuturePointing d) :
⟪v.1, w.1.spaceReflection⟫ₘ ≤ 0 := by ⟪v.1, w.1.spaceReflection⟫ₘ ≤ 0 := by
rw [show (0 : ℝ) = - 0 from zero_eq_neg.mpr rfl, le_neg] rw [show (0 : ℝ) = - 0 from zero_eq_neg.mpr rfl, le_neg]
@ -209,7 +206,6 @@ noncomputable def timeVecNormOneFuture : FuturePointing d := ⟨⟨timeVec, by
rw [NormOneLorentzVector.mem_iff, on_timeVec]⟩, by rw [NormOneLorentzVector.mem_iff, on_timeVec]⟩, by
rw [mem_iff, timeVec_time]; exact Real.zero_lt_one⟩ rw [mem_iff, timeVec_time]; exact Real.zero_lt_one⟩
/-- A continuous path from `timeVecNormOneFuture` to any other. -/ /-- A continuous path from `timeVecNormOneFuture` to any other. -/
noncomputable def pathFromTime (u : FuturePointing d) : Path timeVecNormOneFuture u where noncomputable def pathFromTime (u : FuturePointing d) : Path timeVecNormOneFuture u where
toFun t := ⟨ toFun t := ⟨
@ -266,9 +262,6 @@ noncomputable def pathFromTime (u : FuturePointing d) : Path timeVecNormOneFutur
simp only [Set.Icc.coe_one, one_pow, space, one_mul, Fin.isValue] simp only [Set.Icc.coe_one, one_pow, space, one_mul, Fin.isValue]
exact rfl exact rfl
lemma isPathConnected : IsPathConnected (@Set.univ (FuturePointing d)) := by lemma isPathConnected : IsPathConnected (@Set.univ (FuturePointing d)) := by
use timeVecNormOneFuture use timeVecNormOneFuture
apply And.intro trivial ?_ apply And.intro trivial ?_
@ -276,7 +269,6 @@ lemma isPathConnected : IsPathConnected (@Set.univ (FuturePointing d)) := by
use pathFromTime y use pathFromTime y
exact fun _ => a exact fun _ => a
lemma metric_continuous (u : LorentzVector d) : lemma metric_continuous (u : LorentzVector d) :
Continuous (fun (a : FuturePointing d) => ⟪u, a.1.1⟫ₘ) := by Continuous (fun (a : FuturePointing d) => ⟪u, a.1.1⟫ₘ) := by
simp only [minkowskiMetric.eq_time_minus_inner_prod] simp only [minkowskiMetric.eq_time_minus_inner_prod]
@ -289,8 +281,6 @@ lemma metric_continuous (u : LorentzVector d) :
(Continuous.comp' (Pi.continuous_precomp Sum.inr) (Continuous.comp' (Continuous.comp' (Pi.continuous_precomp Sum.inr) (Continuous.comp'
continuous_subtype_val continuous_subtype_val)) continuous_subtype_val continuous_subtype_val))
end FuturePointing end FuturePointing
end NormOneLorentzVector end NormOneLorentzVector

9
HepLean/SpaceTime/MinkowskiMetric.lean
View file

@ -16,7 +16,6 @@ of Lorentz vectors in d dimensions.
-/ -/
open Matrix open Matrix
/-! /-!
@ -55,7 +54,6 @@ lemma sq : @minkowskiMatrix d * minkowskiMatrix = 1 := by
lemma eq_transpose : minkowskiMatrixᵀ = @minkowskiMatrix d := by lemma eq_transpose : minkowskiMatrixᵀ = @minkowskiMatrix d := by
simp only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, diagonal_transpose] simp only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, diagonal_transpose]
@[simp] @[simp]
lemma det_eq_neg_one_pow_d : (@minkowskiMatrix d).det = (- 1) ^ d := by lemma det_eq_neg_one_pow_d : (@minkowskiMatrix d).det = (- 1) ^ d := by
simp [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal] simp [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
@ -71,10 +69,8 @@ lemma as_block : @minkowskiMatrix d = (
rw [← diagonal_neg] rw [← diagonal_neg]
rfl rfl
end minkowskiMatrix end minkowskiMatrix
/-! /-!
# The definition of the Minkowski Metric # The definition of the Minkowski Metric
@ -133,7 +129,6 @@ lemma as_sum :
Function.comp_apply, minkowskiMatrix] Function.comp_apply, minkowskiMatrix]
ring ring
/-- The Minkowski metric expressed as a sum for a single vector. -/ /-- The Minkowski metric expressed as a sum for a single vector. -/
lemma as_sum_self : ⟪v, v⟫ₘ = v.time ^ 2 - ‖v.space‖ ^ 2 := by lemma as_sum_self : ⟪v, v⟫ₘ = v.time ^ 2 - ‖v.space‖ ^ 2 := by
rw [← real_inner_self_eq_norm_sq, PiLp.inner_apply, as_sum] rw [← real_inner_self_eq_norm_sq, PiLp.inner_apply, as_sum]
@ -167,7 +162,6 @@ lemma right_spaceReflection : ⟪v, w.spaceReflection⟫ₘ = v.time * w.time +
simp only [time, Fin.isValue, space, inner_neg_right, PiLp.inner_apply, Function.comp_apply, simp only [time, Fin.isValue, space, inner_neg_right, PiLp.inner_apply, Function.comp_apply,
RCLike.inner_apply, conj_trivial, sub_neg_eq_add] RCLike.inner_apply, conj_trivial, sub_neg_eq_add]
lemma self_spaceReflection_eq_zero_iff : ⟪v, v.spaceReflection⟫ₘ = 0 ↔ v = 0 := by lemma self_spaceReflection_eq_zero_iff : ⟪v, v.spaceReflection⟫ₘ = 0 ↔ v = 0 := by
refine Iff.intro (fun h => ?_) (fun h => ?_) refine Iff.intro (fun h => ?_) (fun h => ?_)
· rw [right_spaceReflection] at h · rw [right_spaceReflection] at h
@ -195,7 +189,6 @@ lemma nondegenerate : (∀ w, ⟪w, v⟫ₘ = 0) ↔ v = 0 := by
· exact (self_spaceReflection_eq_zero_iff _ ).mp ((symm _ _).trans $ h v.spaceReflection) · exact (self_spaceReflection_eq_zero_iff _ ).mp ((symm _ _).trans $ h v.spaceReflection)
· simp [h] · simp [h]
/-! /-!
# Inequalitites involving the Minkowski metric # Inequalitites involving the Minkowski metric
@ -215,7 +208,6 @@ lemma ge_sub_norm : v.time * w.time - ‖v.space‖ * ‖w.space‖ ≤ ⟪v, w
rw [sub_le_sub_iff_left] rw [sub_le_sub_iff_left]
exact norm_inner_le_norm v.space w.space exact norm_inner_le_norm v.space w.space
/-! /-!
# The Minkowski metric and matrices # The Minkowski metric and matrices
@ -303,7 +295,6 @@ lemma matrix_eq_id_iff : Λ = 1 ↔ ∀ w v, ⟪v, Λ *ᵥ w⟫ₘ = ⟪v, w⟫
rw [matrix_eq_iff_eq_forall] rw [matrix_eq_iff_eq_forall]
simp simp
/-! /-!
# The Minkowski metric and the standard basis # The Minkowski metric and the standard basis

2
HepLean/SpaceTime/SL2C/Basic.lean
View file

@ -130,8 +130,6 @@ Complete this section.
-/ -/
end end
end SL2C end SL2C

2
HepLean/StandardModel/HiggsBoson/Basic.lean
View file

@ -98,7 +98,6 @@ lemma apply_im_smooth (φ : HiggsField) (i : Fin 2):
/-- Given two `higgsField`, the map `spaceTime → ℂ` obtained by taking their inner product. -/ /-- Given two `higgsField`, the map `spaceTime → ℂ` obtained by taking their inner product. -/
def innerProd (φ1 φ2 : HiggsField) : SpaceTime → ℂ := fun x => ⟪φ1 x, φ2 x⟫_ℂ def innerProd (φ1 φ2 : HiggsField) : SpaceTime → ℂ := fun x => ⟪φ1 x, φ2 x⟫_ℂ
/-- Given a `higgsField`, the map `spaceTime → ℝ` obtained by taking the square norm of the /-- Given a `higgsField`, the map `spaceTime → ℝ` obtained by taking the square norm of the
higgs vector. -/ higgs vector. -/
@[simp] @[simp]
@ -154,7 +153,6 @@ lemma potential_apply (φ : HiggsField) (μSq lambda : ℝ) (x : SpaceTime) :
simp [HiggsVec.potential, toHiggsVec_norm] simp [HiggsVec.potential, toHiggsVec_norm]
ring ring
/-- A higgs field is constant if it is equal for all `x` `y` in `spaceTime`. -/ /-- A higgs field is constant if it is equal for all `x` `y` in `spaceTime`. -/
def IsConst (Φ : HiggsField) : Prop := ∀ x y, Φ x = Φ y def IsConst (Φ : HiggsField) : Prop := ∀ x y, Φ x = Φ y

2
HepLean/StandardModel/HiggsBoson/TargetSpace.lean
View file

@ -39,7 +39,6 @@ open ComplexConjugate
/-- The complex vector space in which the Higgs field takes values. -/ /-- The complex vector space in which the Higgs field takes values. -/
abbrev HiggsVec := EuclideanSpace ℂ (Fin 2) abbrev HiggsVec := EuclideanSpace ℂ (Fin 2)
/-- The continuous linear map from the vector space `higgsVec` to `(Fin 2 → ℂ)` achieved by /-- The continuous linear map from the vector space `higgsVec` to `(Fin 2 → ℂ)` achieved by
casting vectors. -/ casting vectors. -/
def higgsVecToFin2ℂ : HiggsVec →L[ℝ] (Fin 2 → ℂ) where def higgsVecToFin2ℂ : HiggsVec →L[ℝ] (Fin 2 → ℂ) where
@ -144,7 +143,6 @@ lemma potential_snd_term_nonneg (φ : HiggsVec) :
simp_all only [ge_iff_le, norm_nonneg, pow_nonneg, and_true] simp_all only [ge_iff_le, norm_nonneg, pow_nonneg, and_true]
exact le_of_lt hLam exact le_of_lt hLam
lemma zero_le_potential_discrim (φ : HiggsVec) : lemma zero_le_potential_discrim (φ : HiggsVec) :
0 ≤ discrim (λ) (- μSq ) (- potential μSq (λ) φ) := by 0 ≤ discrim (λ) (- μSq ) (- potential μSq (λ) φ) := by
have h1 := potential_as_quad μSq (λ) φ have h1 := potential_as_quad μSq (λ) φ

1
HepLean/StandardModel/Representations.lean
View file

@ -53,5 +53,4 @@ lemma repU1_fundamentalSU2_commute (u1 : unitary ℂ) (g : specialUnitaryGroup (
apply Subtype.ext apply Subtype.ext
simp simp
end StandardModel end StandardModel

4
lakefile.toml
View file

@ -37,3 +37,7 @@ srcDir = "scripts"
[[lean_exe]] [[lean_exe]]
name = "type_former_lint" name = "type_former_lint"
srcDir = "scripts" srcDir = "scripts"
[[lean_exe]]
name = "double_line_lint"
srcDir = "scripts"

71
scripts/double_line_lint.lean Normal file
View file

@ -0,0 +1,71 @@
/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license.
Authors: Joseph Tooby-Smith
-/
import Lean
import Mathlib.Tactic.Linter.TextBased
/-!
# Double line Lint
This linter double empty lines in files.
## Note
Parts of this file are adapted from `Mathlib.Tactic.Linter.TextBased`,
authored by Michael Rothgang.
-/
open Lean System Meta
/-- Given a list of lines, outputs an error message and a line number. -/
def HepLeanTextLinter : Type := Array String → Array (String × ℕ)
/-- Checks if there are two consecutive empty lines. -/
def doubleEmptyLineLinter : HepLeanTextLinter := fun lines ↦ Id.run do
let enumLines := (lines.toList.enumFrom 1)
let pairLines := List.zip enumLines (List.tail! enumLines)
let errors := pairLines.filterMap (fun ((lno1, l1), _, l2) ↦
if l1.length == 0 && l2.length == 0 then
some (s!" Double empty line. ", lno1)
else none)
errors.toArray
structure HepLeanErrorContext where
/-- The underlying `message`. -/
error : String
/-- The line number -/
lineNumber : ℕ
/-- The file path -/
path : FilePath
def printErrors (errors : Array HepLeanErrorContext) : IO Unit := do
for e in errors do
IO.println (s!"error: {e.path}:{e.lineNumber}: {e.error}")
def hepLeanLintFile (path : FilePath) : IO Bool := do
let lines ← IO.FS.lines path
let allOutput := (Array.map (fun lint ↦
(Array.map (fun (e, n) ↦ HepLeanErrorContext.mk e n path)) (lint lines)))
#[doubleEmptyLineLinter]
let errors := allOutput.flatten
printErrors errors
return errors.size > 0
def main (_ : List String) : IO UInt32 := do
initSearchPath (← findSysroot)
let mods : Name := `HepLean
let imp : Import := {module := mods}
let mFile ← findOLean imp.module
unless (← mFile.pathExists) do
throw <| IO.userError s!"object file '{mFile}' of module {imp.module} does not exist"
let (hepLeanMod, _) ← readModuleData mFile
let mut warned := false
for imp in hepLeanMod.imports do
if imp.module == `Init then continue
let filePath := (mkFilePath (imp.module.toString.split (· == '.'))).addExtension "lean"
if ← hepLeanLintFile filePath then
warned := true
if warned then
throw <| IO.userError s!"Errors found."
return 0