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

Merge branch 'master' into Tensors

Browse source
This commit is contained in:
jstoobysmith 2024-07-11 09:20:55 -04:00
commit 92cca4c6df
84 changed files with 1035 additions and 782 deletions
Download patch file Download diff file Expand all files Collapse all files

BIN
.DS_Store vendored
View file

Binary file not shown.

29
.github/workflows/docs.yml vendored
View file

@ -21,30 +21,30 @@ jobs:
with:
fetch-depth: 0
- name: Print files to upstream
run: |
grep -r --files-without-match 'import HepLean' HepLean | sort > 1.txt
grep -r --files-with-match 'sorry' HepLean | sort > 2.txt
mkdir -p docs/_includes
comm -23 1.txt 2.txt | sed -e 's/^\(.*\)$/- [`\1`](https:\/\/github.com\/teorth\/HepLean\/blob\/master\/\1)/' > docs/_includes/files_to_upstream.md
rm 1.txt 2.txt
##################
# Remove this section if you don't want docs to be made
- name: Install elan
run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.0.0
run: |
set -o pipefail
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
~/.elan/bin/lean --version
echo "$HOME/.elan/bin" >> $GITHUB_PATH
- name: Get cache
run: ~/.elan/bin/lake -Kenv=dev exe cache get || true
- name: Get Mathlib cache
run: lake -Kenv=dev exe cache get || true
- name: Build project
run: ~/.elan/bin/lake -Kenv=dev build HepLean
run: lake -Kenv=dev build HepLean
- name: Cache mathlib docs
- name: Get doc cache
uses: actions/cache@v3
with:
path: |
.lake/build/doc/Init
.lake/build/doc/DocGen4
.lake/build/doc/Aesop
.lake/build/doc/Lake
.lake/build/doc/Batteries
.lake/build/doc/Lean
.lake/build/doc/Std
.lake/build/doc/Mathlib
@ -55,7 +55,10 @@ jobs:
MathlibDoc-
- name: Build documentation
run: ~/.elan/bin/lake -Kenv=dev build HepLean:docs
run: lake -Kenv=dev build HepLean:docs
- name: make TODO list
run : lake exe find_TODOs mkFile
- name: Copy documentation to `docs/docs`
run: |

3
.gitignore vendored
View file

@ -1,4 +1,5 @@
/build
/lake-packages/*
.lake/packages/*
.lake/build
.lake/build
.DS_Store

4
HepLean.lean
View file

@ -77,5 +77,7 @@ import HepLean.SpaceTime.MinkowskiMetric
import HepLean.SpaceTime.SL2C.Basic
import HepLean.StandardModel.Basic
import HepLean.StandardModel.HiggsBoson.Basic
import HepLean.StandardModel.HiggsBoson.TargetSpace
import HepLean.StandardModel.HiggsBoson.GaugeAction
import HepLean.StandardModel.HiggsBoson.PointwiseInnerProd
import HepLean.StandardModel.HiggsBoson.Potential
import HepLean.StandardModel.Representations

8
HepLean/AnomalyCancellation/Basic.lean
View file

@ -13,12 +13,10 @@ This file defines the basic structures for the anomaly cancellation conditions.
It defines a module structure on the charges, and the solutions to the linear ACCs.
## TODO
- Derive ACC systems from gauge algebras and fermionic representations.
- Relate ACCSystems to algebraic varieties.
-/
/-! TODO: Derive an ACC system from a guage algebra and fermionic representations. -/
/-! TODO: Relate ACC Systems to algebraic varieties. -/
/-! TODO: Refactor whole file, and dependent files. -/
/-- A system of charges, specified by the number of charges. -/
structure ACCSystemCharges where

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

@ -22,7 +22,6 @@ universe v u
open Nat
open BigOperators
/-- The vector space of charges corresponding to the MSSM fermions. -/
@[simps!]
def MSSMCharges : ACCSystemCharges := ACCSystemChargesMk 20
@ -314,7 +313,6 @@ def quadBiLin : BiLinearSymm MSSMCharges.Charges := BiLinearSymm.mk₂ (
ring
ring)
/-- The quadratic ACC. -/
@[simp]
def accQuad : HomogeneousQuadratic MSSMCharges.Charges := quadBiLin.toHomogeneousQuad
@ -335,7 +333,6 @@ lemma accQuad_ext {S T : (MSSMCharges).Charges}
repeat rw [h1]
rw [hd, hu]
/-- The function underlying the symmetric trilinear form used to define the cubic ACC. -/
@[simp]
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]
ring
lemma cubeTriLinToFun_map_add₁ (S T R L : MSSMCharges.Charges) :
cubeTriLinToFun (S + T, R, L) = cubeTriLinToFun (S, R, L) + cubeTriLinToFun (T, R, L) := by
simp only [cubeTriLinToFun]
@ -382,7 +378,6 @@ lemma cubeTriLinToFun_map_add₁ (S T R L : MSSMCharges.Charges) :
rw [Hd.map_add, Hu.map_add]
ring
lemma cubeTriLinToFun_swap1 (S T R : MSSMCharges.Charges) :
cubeTriLinToFun (S, T, R) = cubeTriLinToFun (T, S, R) := by
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 :=
MSSMACC.AnomalyFreeMk YAsCharge (by rfl) (by rfl) (by rfl) (by rfl) (by rfl) (by rfl)
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
linarith
lemma quad_Y₃_proj (T : MSSMACC.LinSols) :
quadBiLin Y₃.val (proj T).val = dot Y₃.val B₃.val * quadBiLin Y₃.val T.val := by
rw [proj_val]
@ -119,7 +117,6 @@ lemma quad_proj (T : MSSMACC.Sols) :
rw [quad_Y₃_proj, quad_B₃_proj, quad_self_proj]
ring
lemma cube_proj_proj_Y₃ (T : MSSMACC.LinSols) :
cubeTriLin (proj T).val (proj T).val Y₃.val =
(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]
ring
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
namespace MSSMACC
@ -44,7 +42,6 @@ lemma planeY₃B₃_smul (R : MSSMACC.AnomalyFreePerp) (a b c d : ℚ) :
rw [smul_add, smul_add]
rw [smul_smul, smul_smul, smul_smul]
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
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]
simp
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
+ 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 B₃.val - a₂ * cubeTriLin R.val R.val Y₃.val))
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
apply ACCSystemLinear.LinSols.ext
@ -242,5 +237,4 @@ lemma α₂_proj_zero (T : MSSMACC.Sols) (h1 : α₃ (proj T.1.1) = 0) :
end proj
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
surjection on certain subtypes of `MSSMACC.Sols`.
# References
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]
simp
/-- A condition which is satisfied if the plane spanned by `R`, `Y₃` and `B₃` lies
entirely in the quadratic surface. -/
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 Y₃.val = 0
instance (R : MSSMACC.AnomalyFreePerp) : Decidable (InCubeProp R) := by
apply And.decidable
@ -238,7 +235,6 @@ not surjective. -/
def toSolNS : MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, a, _ , _) =>
a • AnomalyFreeMk'' (toSolNSQuad R) (toSolNSQuad_cube R)
/-- A map from `Sols` to `MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ` which on elements of
`notInLineEqSol` will produce a right inverse to `toSolNS`. -/
def toSolNSProj (T : MSSMACC.Sols) : MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ :=
@ -458,7 +454,6 @@ theorem toSol_surjective : Function.Surjective toSol := by
simp at h₃
exact toSol_inQuadCube ⟨T, And.intro h₁ (And.intro h₂ h₃)⟩
end AnomalyFreePerp
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
open Nat
open Finset
namespace PureU1
@ -35,7 +34,6 @@ def accGrav (n : ℕ) : ((PureU1Charges n).Charges →ₗ[ℚ] ℚ) where
simp [HSMul.hSMul, SMul.smul]
rw [← Finset.mul_sum]
/-- The symmetric trilinear form used to define the cubic anomaly. -/
@[simps!]
def accCubeTriLinSymm {n : ℕ} : TriLinearSymm (PureU1Charges n).Charges := TriLinearSymm.mk₃
@ -70,14 +68,11 @@ def accCubeTriLinSymm {n : ℕ} : TriLinearSymm (PureU1Charges n).Charges := Tri
ring
)
/-- The cubic anomaly equation. -/
@[simp]
def accCube (n : ℕ) : HomogeneousCubic ((PureU1Charges n).Charges) :=
(accCubeTriLinSymm).toCubic
lemma accCube_explicit (n : ℕ) (S : (PureU1Charges n).Charges) :
accCube n S = ∑ i : Fin n, S i ^ 3:= by
rw [accCube, TriLinearSymm.toCubic]
@ -165,7 +160,6 @@ lemma sum_of_charges {n : ℕ} (f : Fin k → (PureU1 n).Charges) (j : Fin n) :
erw [← hlt]
simp
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
induction k
@ -177,5 +171,4 @@ lemma sum_of_anomaly_free_linear {n : ℕ} (f : Fin k → (PureU1 n).LinSols) (j
erw [← hlt]
simp
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
simp at hk⟩
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) :=
sum_of_anomaly_free_linear (fun i => f i) j
@ -134,5 +133,4 @@ lemma finrank_AnomalyFreeLinear :
end BasisLinear
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
simp
lemma boundary_accGrav'' (k : Fin n) (hk : Boundary S k) :
accGrav n.succ S = (2 * ↑↑k + 1 - ↑n) * S (0 : Fin n.succ) := by
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
simp [accGrav, ← not_hasBoundry_zero hS hnot]
lemma AFL_hasBoundary (h : A.val (0 : Fin n.succ) ≠ 0) : HasBoundary A.val := by
by_contra 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
exact AFL_even_above' h hA i
end charges
end ConstAbsSorted
namespace ConstAbs
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)
sortAFL_zero S (ConstAbsSorted.AFL_odd (sortAFL S) hS)
theorem boundary_value_even (S : (PureU1 (2 * n.succ)).LinSols) (hs : ConstAbs S.val) :
VectorLikeEven S.val := by
have hS := And.intro (constAbs_sort hs) (sort_sorted S.val)

8
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_all only [ne_eq, ↓reduceIte]
lemma basis!_on_δ!₁_other {k j : Fin n} (h : k ≠ j) :
basis!AsCharges k (δ!₁ j) = 0 := by
simp [basis!AsCharges]
@ -310,7 +309,6 @@ lemma basis!_accCube (j : Fin n) :
simp [basis!_δ!₂_eq_minus_δ!₁]
ring
/-- The first part of the basis as `LinSols`. -/
@[simps!]
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
exact P!_zero f h1
theorem basisa_linear_independent : LinearIndependent ℚ (@basisa n) := by
apply Fintype.linearIndependent_iff.mpr
intro f h
@ -626,7 +623,8 @@ lemma Pa'_eq (f f' : (Fin n.succ) ⊕ (Fin n) → ℚ) : Pa' f = Pa' f' ↔ f =
intro h
rw [h]
/-- A helper function for what follows. TODO: replace this with mathlib functions. -/
/-! TODO: Replace the definition of `join` with a Mathlib definition, most likely `Sum.elim`. -/
/-- A helper function for what follows. -/
def join (g : Fin n.succ → ℚ) (f : Fin n → ℚ) : (Fin n.succ) ⊕ (Fin n) → ℚ := fun i =>
match i with
| .inl i => g i
@ -663,7 +661,6 @@ lemma Pa_eq (g g' : Fin n.succ → ℚ) (f f' : Fin n → ℚ) :
rw [← join_ext]
exact Pa'_eq _ _
lemma basisa_card : Fintype.card ((Fin n.succ) ⊕ (Fin n)) =
FiniteDimensional.finrank ℚ (PureU1 (2 * n.succ)).LinSols := by
erw [BasisLinear.finrank_AnomalyFreeLinear]
@ -675,7 +672,6 @@ noncomputable def basisaAsBasis :
Basis (Fin (succ n) ⊕ Fin n) ℚ (PureU1 (2 * succ n)).LinSols :=
basisOfLinearIndependentOfCardEqFinrank (@basisa_linear_independent n) basisa_card
lemma span_basis (S : (PureU1 (2 * n.succ)).LinSols) :
∃ (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)

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
exact h
lemma special_case_lineInCubic {S : (PureU1 (2 * n.succ)).Sols}
(h : SpecialCase S) : LineInCubic S.1.1 := by
intro g f hS a b
@ -152,7 +151,6 @@ lemma special_case_lineInCubic {S : (PureU1 (2 * n.succ)).Sols}
erw [h]
simp
lemma special_case_lineInCubic_perm {S : (PureU1 (2 * n.succ)).Sols}
(h : ∀ (M : (FamilyPermutations (2 * n.succ)).group),
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
exact special_case_lineInCubic (h M)
theorem special_case {S : (PureU1 (2 * n.succ.succ)).Sols}
(h : ∀ (M : (FamilyPermutations (2 * n.succ.succ)).group),
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
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,
not_false_eq_true]
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 ) :
(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_all
lemma linesInPlane_eq_sq_four {S : (PureU1 4).Sols}
(hS : LineInPlaneCond S.1.1) : ∀ (i j : Fin 4) (_ : i ≠ j),
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)
exact linesInPlane_four S' hS'
lemma linesInPlane_constAbs_four (S : (PureU1 4).Sols)
(hS : LineInPlaneCond S.1.1) : ConstAbs S.val := by
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 hS
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⟩,
(cube_for_linSol S).mp hS⟩
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.val (2 : Fin 3) = 0), solOfLinear T hT = S := by

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

@ -23,7 +23,6 @@ namespace PureU1
variable {n : ℕ}
namespace VectorLikeOddPlane
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
lemma P_zero (f : Fin n → ℚ) (h : P f = 0) : ∀ i, f i = 0 := by
intro i
erw [← P_δ₁ f]
@ -572,7 +570,6 @@ theorem basis!_linear_independent : LinearIndependent ℚ (@basis! n) := by
rw [P!'_val] at h1
exact P!_zero f h1
theorem basisa_linear_independent : LinearIndependent ℚ (@basisa n.succ) := by
apply Fintype.linearIndependent_iff.mpr
intro f h
@ -611,7 +608,8 @@ lemma Pa'_eq (f f' : (Fin n.succ) ⊕ (Fin n.succ) → ℚ) : Pa' f = Pa' f'
intro h
rw [h]
/-- A helper function for what follows. TODO: replace this with mathlib functions. -/
/-! TODO: Replace the definition of `join` with a Mathlib definition, most likely `Sum.elim`. -/
/-- A helper function for what follows. -/
def join (g f : Fin n → ℚ) : Fin n ⊕ Fin n → ℚ := fun i =>
match i with
| .inl i => g i
@ -648,8 +646,6 @@ lemma Pa_eq (g g' : Fin n.succ → ℚ) (f f' : Fin n.succ → ℚ) :
rw [← join_ext]
exact Pa'_eq _ _
lemma basisa_card : Fintype.card ((Fin n.succ) ⊕ (Fin n.succ)) =
FiniteDimensional.finrank ℚ (PureU1 (2 * n.succ + 1)).LinSols := by
erw [BasisLinear.finrank_AnomalyFreeLinear]
@ -706,8 +702,6 @@ lemma span_basis_swap! {S : (PureU1 (2 * n.succ + 1)).LinSols} (j : Fin n.succ)
apply swap!_as_add at hS
exact hS
end VectorLikeOddPlane
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]
ring
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),
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 ) -
(lineInCubic_expand h g f hS 1 2 ) / 6
/-- We say a `LinSol` satisfies `lineInCubicPerm` if all its permutations satisfy `lineInCubic`. -/
def LineInCubicPerm (S : (PureU1 (2 * n + 1)).LinSols) : Prop :=
∀ (M : (FamilyPermutations (2 * n + 1)).group ),
@ -86,7 +83,6 @@ lemma lineInCubicPerm_permute {S : (PureU1 (2 * n + 1)).LinSols}
rw [ht]
exact hS (M * M')
lemma lineInCubicPerm_swap {S : (PureU1 (2 * n.succ + 1)).LinSols}
(LIC : LineInCubicPerm S) :
∀ (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
exact h
lemma special_case_lineInCubic {S : (PureU1 (2 * n.succ + 1)).Sols}
(h : SpecialCase S) :
LineInCubic S.1.1 := by

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

@ -96,7 +96,6 @@ def FamilyPermutations (n : ℕ) : ACCSystemGroupAction (PureU1 n) where
exact Fin.elim0 i
cubicInvariant := accCube_invariant
lemma FamilyPermutations_charges_apply (S : (PureU1 n).Charges)
(i : Fin n) (f : (FamilyPermutations n).group) :
((FamilyPermutations n).rep f S) i = S (f.invFun i) := by
@ -107,8 +106,8 @@ lemma FamilyPermutations_anomalyFreeLinear_apply (S : (PureU1 n).LinSols)
((FamilyPermutations n).linSolRep f S).val i = S.val (f.invFun i) := by
rfl
/-- The permutation which swaps i and j. TODO: Replace with: `Equiv.swap`. -/
/-! TODO: Replace the definition of `pairSwap` with `Equiv.swap`. -/
/-- The permutation which swaps i and j. -/
def pairSwap {n : ℕ} (i j : Fin n) : (FamilyPermutations n).group where
toFun s :=
if s = i then
@ -247,7 +246,6 @@ lemma permThreeInj_fst_apply :
⟨i, permThreeInj_fst hij hjk hik⟩ = 0 := by
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
simp only [Set.mem_range]
use 1
@ -338,5 +336,4 @@ lemma Prop_three (P : ℚ × ℚ × ℚ → Prop) {S : (PureU1 n).LinSols}
erw [permThree_fst,permThree_snd, permThree_thd] at h1
exact h1
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
rfl
lemma sortAFL_zero {n : ℕ} (S : (PureU1 n).LinSols) (hS : sortAFL S = 0) : S = 0 := by
apply ACCSystemLinear.LinSols.ext
have h1 : sort S.val = 0 := by

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

@ -10,11 +10,8 @@ import Mathlib.Logic.Equiv.Fin
For the `n`-even case we define the property of a charge assignment being vector like.
## TODO
The `n`-odd case.
-/
/-! TODO: Define vector like ACC in the `n`-odd case. -/
universe v u
open Nat
@ -30,7 +27,6 @@ variable {n : ℕ}
-/
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
/-- A charge configuration for n even is vector like if when sorted the `i`th element
@ -40,5 +36,4 @@ def VectorLikeEven (S : (PureU1 (2 * n)).Charges) : Prop :=
∀ (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))
end PureU1

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

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

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

@ -24,7 +24,6 @@ open SMCharges
open SMACCs
open BigOperators
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
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
exact S'.cubic_zero_E'_zero hC hE
lemma accGrav_Q_zero {S : (SMNoGrav 1).Sols} (hQ : Q S.val (0 : Fin 1) = 0) :
accGrav S.val = 0 := by
rw [accGrav]
@ -74,7 +71,6 @@ theorem accGravSatisfied {S : (SMNoGrav 1).Sols} (FLTThree : FermatLastTheoremWi
exact accGrav_Q_zero hQ
exact accGrav_Q_neq_zero hQ FLTThree
end One
end SMNoGrav
end SM

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

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

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

@ -33,7 +33,6 @@ variable {n : ℕ}
@[simp]
instance : Group (PermGroup n) := Pi.group
/-- The image of an element of `permGroup n` under the representation on charges. -/
@[simps!]
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
erw [toSMSpecies_toSpecies_inv]
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 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)
(fun x => ((fun a => a ^ m) ∘ (toSpecies j) S) x) (congrFun rfl)
lemma accGrav_invariant (f : PermGroup n) (S : (SMCharges n).Charges) :
accGrav (repCharges f S) = accGrav S :=
accGrav_ext
(by simpa using toSpecies_sum_invariant 1 f S)
lemma accSU2_invariant (f : PermGroup n) (S : (SMCharges n).Charges) :
accSU2 (repCharges f S) = accSU2 S :=
accSU2_ext
(by simpa using toSpecies_sum_invariant 1 f S)
lemma accSU3_invariant (f : PermGroup n) (S : (SMCharges n).Charges) :
accSU3 (repCharges f S) = accSU3 S :=
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.
-/
universe v u
open Nat
open BigOperators
@ -83,7 +82,6 @@ abbrev E := @toSpecies n 4
/-- The `N` charges as a map `Fin n → ℚ`. -/
abbrev N := @toSpecies n 5
end SMνCharges
namespace SMνACCs
@ -111,7 +109,6 @@ def accGrav : (SMνCharges n).Charges →ₗ[ℚ] ℚ where
-- rw [show Rat.cast a = a from rfl]
ring
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 +
∑ i, N S i := by
@ -127,7 +124,6 @@ lemma accGrav_ext {S T : (SMνCharges n).Charges}
rw [accGrav_decomp, accGrav_decomp]
repeat erw [hj]
/-- The `SU(2)` anomaly equation. -/
@[simp]
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.mul_sum]
/-- The cubic ACC. -/
@[simp]
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]
exact Eq.symm (Rat.mul_zero a)
/-- The embedding of the `m`-family charges onto the `n`-family charges, with all
other charges zero. -/
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
cubicInvariant := accCube_invariant
end SMNoGrav
end SMRHN

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

@ -37,7 +37,6 @@ def SM (n : ℕ) : ACCSystem where
namespace SM
variable {n : ℕ}
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
cubicInvariant := accCube_invariant
end SM
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 [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) :
cubeTriLin (B 1) (B i) S = 0 := by
change cubeTriLin B₁ (B i) S = 0
@ -246,7 +245,6 @@ lemma B₆_B₆_Bi_cubic {i : Fin 7} :
fin_cases i <;>
simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
lemma Bi_Bi_Bj_cubic (i j : Fin 7) :
cubeTriLin (B i) (B i) (B j) = 0 := by
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.B_sum_is_sol
end SM
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
erw [toSMSpecies_toSpecies_inv]
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 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 _ _ _ ?_
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) :
accGrav (repCharges f S) = accGrav S :=
accGrav_ext
(by simpa using toSpecies_sum_invariant 1 f S)
lemma accSU2_invariant (f : PermGroup n) (S : (SMνCharges n).Charges) :
accSU2 (repCharges f S) = accSU2 S :=
accSU2_ext
(by simpa using toSpecies_sum_invariant 1 f S)
lemma accSU3_invariant (f : PermGroup n) (S : (SMνCharges n).Charges) :
accSU3 (repCharges f S) = accSU3 S :=
accSU3_ext
@ -97,7 +93,6 @@ lemma accYY_invariant (f : PermGroup n) (S : (SMνCharges n).Charges) :
accYY_ext
(by simpa using toSpecies_sum_invariant 1 f S)
lemma accQuad_invariant (f : PermGroup n) (S : (SMνCharges n).Charges) :
accQuad (repCharges f S) = accQuad S :=
accQuad_ext
@ -108,6 +103,4 @@ lemma accCube_invariant (f : PermGroup n) (S : (SMνCharges n).Charges) :
accCube_ext
(by simpa using toSpecies_sum_invariant 3 f S)
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]
ring
end BL
end PlusU1
end SMRHN

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

@ -37,7 +37,6 @@ def PlusU1 (n : ℕ) : ACCSystem where
namespace PlusU1
variable {n : ℕ}
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.inr i => exact h4 i
theorem plane_exists_dim_le_7 {n : ℕ} (hn : ExistsPlane n) : n ≤ 7 := by
obtain ⟨B, hB⟩ := exists_plane_exists_basis hn
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
exact Nat.le_of_add_le_add_left h1
end PlusU1
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 [YYsol S]
lemma add_AFL_quad (S : (PlusU1 n).LinSols) (a b : ℚ) :
accQuad (a • S.val + b • (Y n).val) = a ^ 2 * accQuad S.val := by
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 :=
quadToAF (addQuad S.1 a b) (add_AF_cube S a b)
end Y
end PlusU1
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]
ring
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
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_f10 f hS
lemma isSolution_only_if_zero (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i • B i)) :
∑ i, f i • B i = 0 := by
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]
simp
theorem basis_linear_independent : LinearIndependent ℚ B := by
apply Fintype.linearIndependent_iff.mpr
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
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
`α₂ 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]
simp
end QuadSolToSol
open QuadSolToSol
/-- A map from `QuadSols × ℚ × ℚ` to `Sols` taking account of the special and generic cases.
We will show that this map is a surjection. -/

97
HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean
View file

@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license.
Authors: Joseph Tooby-Smith
-/
import HepLean.StandardModel.HiggsBoson.Basic
import HepLean.StandardModel.HiggsBoson.Potential
/-!
# The Two Higgs Doublet Model
@ -18,20 +18,93 @@ namespace TwoHDM
open StandardModel
open ComplexConjugate
open HiggsField
noncomputable section
/-- The potential of the two Higgs doublet model. -/
def potential (Φ1 Φ2 : HiggsField)
(m11Sq m22Sq lam₁ lam₂ lam₃ lam₄ : ℝ) (m12Sq lam₅ lam₆ lam₇ : ℂ) (x : SpaceTime) : ℝ :=
m11Sq * Φ1.normSq x + m22Sq * Φ2.normSq x
- (m12Sq * (Φ1.innerProd Φ2) x + conj m12Sq * (Φ2.innerProd Φ1) x).re
+ 1/2 * lam₁ * Φ1.normSq x ^ 2 + 1/2 * lam₂ * Φ2.normSq x ^ 2
+ lam₃ * Φ1.normSq x * Φ2.normSq x
+ lam₄ * ‖Φ1.innerProd Φ2 x‖
+ (1/2 * lam₅ * (Φ1.innerProd Φ2) x ^ 2 + 1/2 * conj lam₅ * (Φ2.innerProd Φ1) x ^ 2).re
+ (lam₆ * Φ1.normSq x * (Φ1.innerProd Φ2) x + conj lam₆ * Φ1.normSq x * (Φ2.innerProd Φ1) x).re
+ (lam₇ * Φ2.normSq x * (Φ1.innerProd Φ2) x + conj lam₇ * Φ2.normSq x * (Φ2.innerProd Φ1) x).re
/-- The potential of the two Higgs doublet model. -/
def potential (m₁₁2 m₂₂2 𝓵₁ 𝓵₂ 𝓵₃ 𝓵₄ : ℝ)
(m₁₂2 𝓵₅ 𝓵₆ 𝓵₇ : ℂ) (Φ1 Φ2 : HiggsField) (x : SpaceTime) : ℝ :=
m₁₁2 * ‖Φ1‖_H ^ 2 x + m₂₂2 * ‖Φ2‖_H ^ 2 x - (m₁₂2 * ⟪Φ1, Φ2⟫_H x + conj m₁₂2 * ⟪Φ2, Φ1⟫_H x).re
+ 1/2 * 𝓵₁ * ‖Φ1‖_H ^ 2 x * ‖Φ1‖_H ^ 2 x + 1/2 * 𝓵₂ * ‖Φ2‖_H ^ 2 x * ‖Φ2‖_H ^ 2 x
+ 𝓵₃ * ‖Φ1‖_H ^ 2 x * ‖Φ2‖_H ^ 2 x
+ 𝓵₄ * ‖⟪Φ1, Φ2⟫_H x‖ ^ 2 + (1/2 * 𝓵₅ * ⟪Φ1, Φ2⟫_H x ^ 2 + 1/2 * conj 𝓵₅ * ⟪Φ2, Φ1⟫_H x ^ 2).re
+ (𝓵₆ * ‖Φ1‖_H ^ 2 x * ⟪Φ1, Φ2⟫_H x + conj 𝓵₆ * ‖Φ1‖_H ^ 2 x * ⟪Φ2, Φ1⟫_H x).re
+ (𝓵₇ * ‖Φ2‖_H ^ 2 x * ⟪Φ1, Φ2⟫_H x + conj 𝓵₇ * ‖Φ2‖_H ^ 2 x * ⟪Φ2, Φ1⟫_H x).re
namespace potential
variable (Φ1 Φ2 : HiggsField)
variable (m₁₁2 m₂₂2 𝓵₁ 𝓵₂ 𝓵₃ 𝓵₄ : ℝ)
variable (m₁₂2 𝓵₅ 𝓵₆ 𝓵₇ : ℂ)
/-!
## Simple properties of the potential
-/
/-- Swapping `Φ1` with `Φ2`, and a number of the parameters (with possible conjugation) leads
to an identical potential. -/
lemma swap_fields :
potential m₁₁2 m₂₂2 𝓵₁ 𝓵₂ 𝓵₃ 𝓵₄ m₁₂2 𝓵₅ 𝓵₆ 𝓵₇ Φ1 Φ2
= potential m₂₂2 m₁₁2 𝓵₂ 𝓵₁ 𝓵₃ 𝓵₄ (conj m₁₂2) (conj 𝓵₅) (conj 𝓵₇) (conj 𝓵₆) Φ2 Φ1 := by
funext x
simp only [potential, HiggsField.normSq, Complex.add_re, Complex.mul_re, Complex.conj_re,
Complex.conj_im, neg_mul, sub_neg_eq_add, one_div, Complex.norm_eq_abs, Complex.inv_re,
Complex.re_ofNat, Complex.normSq_ofNat, div_self_mul_self', Complex.inv_im, Complex.im_ofNat,
neg_zero, zero_div, zero_mul, sub_zero, Complex.mul_im, add_zero, mul_neg, Complex.ofReal_pow,
RingHomCompTriple.comp_apply, RingHom.id_apply]
ring_nf
simp only [one_div, add_left_inj, add_right_inj, mul_eq_mul_left_iff]
apply Or.inl
rw [HiggsField.innerProd, HiggsField.innerProd, ← InnerProductSpace.conj_symm, Complex.abs_conj]
/-- If `Φ₂` is zero the potential reduces to the Higgs potential on `Φ₁`. -/
lemma right_zero : potential m₁₁2 m₂₂2 𝓵₁ 𝓵₂ 𝓵₃ 𝓵₄ m₁₂2 𝓵₅ 𝓵₆ 𝓵₇ Φ1 0 =
StandardModel.HiggsField.potential (- m₁₁2) (𝓵₁/2) Φ1 := by
funext x
simp only [potential, normSq, ContMDiffSection.coe_zero, Pi.zero_apply, norm_zero, ne_eq,
OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, mul_zero, add_zero, innerProd_right_zero,
innerProd_left_zero, Complex.zero_re, sub_zero, one_div, Complex.ofReal_pow,
Complex.ofReal_zero, HiggsField.potential, neg_neg, add_right_inj, mul_eq_mul_right_iff,
pow_eq_zero_iff, norm_eq_zero, or_self_right]
ring_nf
simp only [true_or]
/-- If `Φ₁` is zero the potential reduces to the Higgs potential on `Φ₂`. -/
lemma left_zero : potential m₁₁2 m₂₂2 𝓵₁ 𝓵₂ 𝓵₃ 𝓵₄ m₁₂2 𝓵₅ 𝓵₆ 𝓵₇ 0 Φ2 =
StandardModel.HiggsField.potential (- m₂₂2) (𝓵₂/2) Φ2 := by
rw [swap_fields, right_zero]
/-!
## Potential bounded from below
-/
/-! TODO: Prove bounded properties of the 2HDM potential. -/
/-- The proposition on the coefficents for a potential to be bounded. -/
def IsBounded (m₁₁2 m₂₂2 𝓵₁ 𝓵₂ 𝓵₃ 𝓵₄ : ℝ) (m₁₂2 𝓵₅ 𝓵₆ 𝓵₇ : ℂ) : Prop :=
∃ c, ∀ Φ1 Φ2 x, c ≤ potential m₁₁2 m₂₂2 𝓵₁ 𝓵₂ 𝓵₃ 𝓵₄ m₁₂2 𝓵₅ 𝓵₆ 𝓵₇ Φ1 Φ2 x
/-!
## Smoothness of the potential
-/
/-! TODO: Prove smoothness properties of the 2HDM potential. -/
/-!
## Invariance of the potential under gauge transformations
-/
/-! TODO: Prove invariance properties of the 2HDM potential. -/
end potential
end
end TwoHDM

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
a quantum field theory.
-/
open CategoryTheory
@ -106,7 +105,6 @@ def preimageEdge {𝓔 𝓥 : Type} (v : 𝓔) :
map {f g} F := Over.homMk ((P.toEdge ⋙ preimageType' v).map F)
(funext <| fun x => congrArg Prod.fst <| congrFun F.w x.1)
/-!
## Finitness of pre-Feynman rules
@ -304,7 +302,6 @@ instance diagramEdgePropDecidable
(fun _ => P.preFeynmanRuleDecEq𝓱𝓔) _ _ _)) _ ) _)
(P.diagramEdgeProp_iff F f).symm
end PreFeynmanRule
/-!
@ -378,7 +375,6 @@ instance CondDecidable [IsFinitePreFeynmanRule P] {𝓔 𝓥 𝓱𝓔 : Type} (
(@diagramEdgePropDecidable P _ _ _ _ _ (Over.mk 𝓱𝓔To𝓔𝓥) _ h 𝓔𝓞)
(@diagramVertexPropDecidable P _ _ _ _ _ (Over.mk 𝓱𝓔To𝓔𝓥) _ h 𝓥𝓞)
/-- Making a Feynman diagram from maps of edges, vertices and half-edges. -/
def mk' {𝓔 𝓥 𝓱𝓔 : Type} (𝓔𝓞 : 𝓔 → P.EdgeLabel) (𝓥𝓞 : 𝓥 → P.VertexLabel)
(𝓱𝓔To𝓔𝓥 : 𝓱𝓔 → P.HalfEdgeLabel × 𝓔 × 𝓥)
@ -491,7 +487,6 @@ structure Hom (F G : FeynmanDiagram P) where
/-- The morphism of half-edge objects. -/
𝓱𝓔To𝓔𝓥 : (edgeVertexFunc 𝓔𝓞.left 𝓥𝓞.left).obj F.𝓱𝓔To𝓔𝓥 ⟶ G.𝓱𝓔To𝓔𝓥
namespace Hom
variable {F G : FeynmanDiagram P}
variable (f : Hom F G)
@ -508,12 +503,10 @@ def 𝓥 : F.𝓥 → G.𝓥 := f.𝓥𝓞.left
@[simp]
def 𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔 := f.𝓱𝓔To𝓔𝓥.left
/-- The morphism `F.𝓱𝓔𝓞 ⟶ G.𝓱𝓔𝓞` induced by a homomorphism of Feynman diagrams. -/
@[simp]
def 𝓱𝓔𝓞 : F.𝓱𝓔𝓞 ⟶ G.𝓱𝓔𝓞 := P.toHalfEdge.map f.𝓱𝓔To𝓔𝓥
/-- The identity morphism for a Feynman diagram. -/
def id (F : FeynmanDiagram P) : Hom F F where
𝓔𝓞 := 𝟙 F.𝓔𝓞
@ -579,7 +572,6 @@ instance {F G : FeynmanDiagram P} [IsFiniteDiagram F] [IsFiniteDiagram G] [IsFin
(𝓔 : F.𝓔 → G.𝓔) (𝓥 : F.𝓥 → G.𝓥) (𝓱𝓔 : F.𝓱𝓔 → G.𝓱𝓔) : Decidable (Cond 𝓔 𝓥 𝓱𝓔) :=
And.decidable
/-- Making a Feynman diagram from maps of edges, vertices and half-edges. -/
@[simps! 𝓔𝓞_left 𝓥𝓞_left 𝓱𝓔To𝓔𝓥_left]
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. -/
def SymmetryType : Type := F ≅ F
/-- An equivalence between `SymmetryType` and permutation of edges, vertices and half-edges
satisfying `Hom.Cond`. -/
def symmetryTypeEquiv :
@ -728,7 +719,6 @@ instance [IsFiniteDiagram F] : DecidableRel F.AdjRelation := fun _ _ =>
@And.decidable _ _ (instDecidableEq𝓥OfIsFiniteDiagram _ _)
(instDecidableEq𝓥OfIsFiniteDiagram _ _)) _ ) _
/-- From a Feynman diagram the simple graph showing those vertices which are connected. -/
def toSimpleGraph : SimpleGraph F.𝓥 where
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
-/
namespace PhiFour
open CategoryTheory
open FeynmanDiagram
@ -65,7 +62,4 @@ instance : IsFinitePreFeynmanRule complexScalarFeynmanRules where
match v with
| 0 => instDecidableEqFin _
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
Phi^4 theory.
-/
namespace PhiFour
open CategoryTheory
open FeynmanDiagram
@ -45,7 +43,6 @@ instance (a : ℕ) : OfNat phi4PreFeynmanRules.HalfEdgeLabel a where
instance (a : ℕ) : OfNat phi4PreFeynmanRules.VertexLabel a where
ofNat := (a : Fin _)
instance : IsFinitePreFeynmanRule phi4PreFeynmanRules where
edgeLabelDecidable := instDecidableEqFin _
vertexLabelDecidable := instDecidableEqFin _
@ -92,5 +89,4 @@ lemma figureEight_symmetryFactor : symmetryFactor figureEight = 8 := by decide
end Example
end PhiFour

8
HepLean/FeynmanDiagrams/Momentum.lean
View file

@ -19,14 +19,13 @@ vector space.
## TODO
- Prove lemmas that make the calcuation of the number of loops of a Feynman diagram easier.
- Prove lemmas that make the calculation of the number of loops of a Feynman diagram easier.
## Note
This section is non-computable as we depend on the norm on `F.HalfEdgeMomenta`.
-/
namespace FeynmanDiagram
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,
LinearMap.smul_apply]
/-- The type which assocaites to each ege a `1`-dimensional vector space.
Corresponding to that spanned by its total outflowing momentum. -/
def EdgeMomenta : Type := F.𝓔 → ℝ
@ -87,7 +85,6 @@ instance : AddCommGroup F.EdgeMomenta := Pi.addCommGroup
instance : Module ℝ F.EdgeMomenta := Pi.module _ _ _
/-- The type which assocaites to each ege a `1`-dimensional vector space.
Corresponding to that spanned by its total inflowing momentum. -/
def VertexMomenta : Type := F.𝓥 → ℝ
@ -119,7 +116,6 @@ instance : AddCommGroup F.EdgeVertexMomenta := DirectSum.instAddCommGroup _
instance : Module ℝ F.EdgeVertexMomenta := DirectSum.instModule
/-!
## Linear maps between the vector spaces.
@ -199,7 +195,6 @@ for specific Feynman diagrams.
- Complete this section.
-/
/-!
@ -210,7 +205,6 @@ for specific Feynman diagrams.
- Complete this section.
-/
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
`[V]ud|us` etc for the ratios of elements.
-/
open Matrix Complex
noncomputable section
/-- 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 [add_comm k e, add_comm l f, add_comm m g]
lemma phaseShiftRelation_equiv : Equivalence PhaseShiftRelation where
refl := phaseShiftRelation_refl
symm := phaseShiftRelation_symm
@ -270,7 +267,6 @@ lemma tb (V : CKMMatrix) (a b c d e f : ℝ) :
end phaseShiftApply
/-- The aboslute value of the `(i,j)`th element of `V`. -/
@[simp]
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]
abbrev VtbAbs := VAbs 2 2
namespace CKMMatrix
open ComplexConjugate
section ratios
/-- 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 CKMMatrix
end

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

@ -15,17 +15,14 @@ this equivalence.
Of note, this file defines the complex jarlskog invariant.
-/
open Matrix Complex
open ComplexConjugate
open CKMMatrix
noncomputable section
namespace Invariant
/-- The complex jarlskog invariant for a CKM matrix. -/
@[simps!]
def jarlskogℂCKM (V : CKMMatrix) : ℂ :=
@ -62,6 +59,5 @@ standard parameterization. -/
def mulExpδ₁₃ (V : Quotient CKMMatrixSetoid) : ℂ :=
jarlskogℂ V + VusVubVcdSq V
end Invariant
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
the ub element as absolute value 1.
-/
open Matrix Complex
noncomputable section
namespace CKMMatrix
open ComplexConjugate
@ -260,7 +258,6 @@ lemma fstRowThdColRealCond_holds_up_to_equiv (V : CKMMatrix) :
apply shift_cross_product_phase_zero _ _ _ _ _ _ hτ.symm
ring
lemma ubOnePhaseCond_hold_up_to_equiv_of_ub_one {V : CKMMatrix} (hb : ¬ ([V]ud ≠ 0 ∨ [V]us ≠ 0))
(hV : FstRowThdColRealCond V) :
∃ (U : CKMMatrix), V ≈ U ∧ ubOnePhaseCond U:= by

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

@ -16,7 +16,6 @@ matrix.
open Matrix Complex
noncomputable section
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
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) :
(normSq [V]ud : ℂ) + normSq [V]us ≠ 0 := by
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
simp_all
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
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]
ring
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))) :
[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
ring
end rows
section individual
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
nlinarith
end individual
section columns
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
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
exact h1.1
lemma cs_of_ud_us_zero {V : CKMMatrix} (ha : ¬ ([V]ud ≠ 0 ∨ [V]us ≠ 0)) :
VcsAbs ⟦V⟧ = √(1 - VcdAbs ⟦V⟧ ^ 2) := by
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
linear_combination (VAbs_sum_sq_col_eq_one V 2)
lemma cb_tb_neq_zero_iff_ub_neq_one (V : CKMMatrix) :
[V]cb ≠ 0 ∨ [V]tb ≠ 0 ↔ abs [V]ub ≠ 1 := by
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`.
-/
open Matrix Complex
@ -24,7 +23,6 @@ noncomputable section
namespace CKMMatrix
/-- The `u`th row of the CKM matrix. -/
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
in the file `FlavorPhysics.CKMMatrix.StandardParameters`.
-/
open Matrix Complex
open ComplexConjugate
@ -194,7 +193,5 @@ lemma mulExpδ₁₃_eq (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ) (h1 : 0 ≤
have h1 : cexp (I * δ₁₃) ≠ 0 := exp_ne_zero _
field_simp
end standParam
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
CKM matrix can be written using the standard parameterization.
-/
open Matrix Complex
open ComplexConjugate
@ -333,7 +332,6 @@ lemma Vs_zero_iff_cos_sin_zero (V : CKMMatrix) :
end VAbs
namespace standParam
open Invariant
@ -409,7 +407,6 @@ lemma on_param_cos_θ₁₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.c
rfl
rfl
lemma on_param_cos_θ₁₂_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.cos (θ₁₂ ⟦V⟧) = 0) :
standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by
use 0, δ₁₃, δ₁₃, -δ₁₃, 0, - δ₁₃
@ -434,7 +431,6 @@ lemma on_param_cos_θ₁₂_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.c
ring_nf
field_simp
lemma on_param_cos_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.cos (θ₂₃ ⟦V⟧) = 0) :
standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by
use 0, δ₁₃, 0, 0, 0, - δ₁₃
@ -451,7 +447,6 @@ lemma on_param_cos_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.c
ring
field_simp
lemma on_param_sin_θ₁₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.sin (θ₁₃ ⟦V⟧) = 0) :
standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by
use 0, 0, 0, 0, 0, 0
@ -488,8 +483,6 @@ lemma on_param_sin_θ₁₂_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.s
ring_nf
field_simp
lemma on_param_sin_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.sin (θ₂₃ ⟦V⟧) = 0) :
standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by
use 0, 0, δ₁₃, 0, 0, - δ₁₃
@ -506,9 +499,6 @@ lemma on_param_sin_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.s
ring
field_simp
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
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₁₃]
simp
lemma eq_standParam_of_ubOnePhaseCond {V : CKMMatrix} (hV : ubOnePhaseCond V) :
V = standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := 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]
simp
theorem exists_δ₁₃ (V : CKMMatrix) :
∃ (δ₃ : ℝ), V ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₃ := by
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
theorem exists_for_CKMatrix (V : CKMMatrix) :
∃ (θ₁₂ θ₁₃ θ₂₃ δ₁₃ : ℝ), V ≈ standParam θ₁₂ θ₁₃ θ₂₃ δ₁₃ := by
use θ₁₂ ⟦V⟧, θ₁₃ ⟦V⟧, θ₂₃ ⟦V⟧, δ₁₃ ⟦V⟧
@ -678,9 +665,6 @@ theorem exists_for_CKMatrix (V : CKMMatrix) :
end standParam
open CKMMatrix
end

11
HepLean/Mathematics/LinearMaps.lean
View file

@ -12,12 +12,8 @@ import Mathlib.Data.Fintype.BigOperators
Some definitions and properties of linear, bilinear, and trilinear maps, along with homogeneous
quadratic and cubic equations.
## TODO
Use definitions in `Mathlib4` for definitions where possible.
In particular a HomogeneousQuadratic should be a map `V →ₗ[ℚ] V →ₗ[ℚ] ℚ` etc.
-/
/-! TODO: Replace the definitions in this file with Mathlib definitions. -/
/-- The structure defining a homogeneous quadratic equation. -/
@[simp]
@ -40,7 +36,6 @@ lemma map_smul (f : HomogeneousQuadratic V) (a : ℚ) (S : V) : f (a • S) = a
end HomogeneousQuadratic
/-- The structure of a symmetric bilinear function. -/
structure BiLinearSymm (V : Type) [AddCommMonoid V] [Module ℚ V] extends V →ₗ[ℚ] V →ₗ[ℚ] ℚ where
swap' : ∀ S T, toFun S T = toFun T S
@ -126,7 +121,6 @@ lemma map_sum₂ {n : ℕ} (f : BiLinearSymm V) (S : Fin n → V) (T : V) :
intro i
rw [swap]
/-- The homogenous quadratic equation obtainable from a bilinear function. -/
@[simps!]
def toHomogeneousQuad {V : Type} [AddCommMonoid V] [Module ℚ V]
@ -146,7 +140,6 @@ lemma toHomogeneousQuad_add {V : Type} [AddCommMonoid V] [Module ℚ V]
rw [τ.map_add₁, τ.map_add₁, τ.swap T S]
ring
end BiLinearSymm
/-- The structure of a homogeneous cubic equation. -/
@ -222,7 +215,6 @@ def mk₃ (f : V × V × V→ ℚ) (map_smul : ∀ a S T L, f (a • S, T, L) =
swap₁' := swap₁
swap₂' := swap₂
lemma swap₁ (f : TriLinearSymm V) (S T L : V) : f S T L = f T S L :=
f.swap₁' S T L
@ -300,7 +292,6 @@ lemma map_sum₁₂₃ {n1 n2 n3 : ℕ} (f : TriLinearSymm V) (S : Fin n1 → V)
intro i
rw [map_sum₃]
/-- The homogenous cubic equation obtainable from a symmetric trilinear function. -/
@[simps!]
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)
-/
namespace GroupTheory
@ -107,7 +106,6 @@ lemma toProd_continuous : Continuous toProd := by
refine Continuous.matrix_transpose ?_
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 monoid of matrices. -/
lemma toProd_embedding : Embedding toProd where
@ -223,10 +221,7 @@ lemma exists_basis_preserved (A : SO(3)) :
use b
rw [hb, hv.2]
end action
end SO3
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
namespace SpaceTime
open Manifold

8
HepLean/SpaceTime/CliffordAlgebra.lean
View file

@ -9,13 +9,9 @@ import Mathlib.Analysis.Complex.Basic
This file defines the Gamma matrices.
## TODO
- Prove that the algebra generated by the gamma matrices is isomorphic to the
Clifford algebra associated with spacetime.
- Include relations for gamma matrices.
-/
/-! TODO: Prove algebra generated by gamma matrices is isomorphic to Clifford algebra. -/
/-! TODO: Define relations between the gamma matrices. -/
namespace spaceTime
open Complex

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

@ -17,7 +17,6 @@ We define
-/
namespace SpaceTime
open Matrix
open TensorProduct
@ -34,7 +33,6 @@ lemma transpose_eta (A : lorentzAlgebra) : A.1ᵀ * η = - η * A.1 := by
erw [mem_skewAdjointMatricesLieSubalgebra] at 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) ℝ}
(h : Aᵀ * η = - η * A) : A ∈ lorentzAlgebra := by
erw [mem_skewAdjointMatricesLieSubalgebra]
@ -58,7 +56,6 @@ lemma mem_iff' (A : Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ) :
rw [minkowskiMatrix.sq]
all_goals noncomm_ring
lemma diag_comp (Λ : lorentzAlgebra) (μ : Fin 1 ⊕ Fin 3) : Λ.1 μ μ = 0 := by
have h := congrArg (fun M ↦ M μ μ) $ mem_iff.mp Λ.2
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
lemma time_comps (Λ : lorentzAlgebra) (i : Fin 3) :
Λ.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,
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
lemma space_comps (Λ : lorentzAlgebra) (i j : Fin 3) :
Λ.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,
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
end lorentzAlgebra
@[simps!]
@ -104,5 +97,4 @@ instance spaceTimeAsLieModule : LieModule ℝ lorentzAlgebra (LorentzVector 3) w
simp [Bracket.bracket]
rw [mulVec_smul]
end SpaceTime

1
HepLean/SpaceTime/LorentzAlgebra/Basis.lean
View file

@ -15,3 +15,4 @@ This file is waiting for Lorentz Tensors to be done formally, before
it can be completed.
-/
/-! TODO: Define the standard basis of the Lorentz algebra. -/

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

@ -10,18 +10,13 @@ import HepLean.SpaceTime.LorentzVector.NormOne
We define the Lorentz group.
## TODO
- Show that the Lorentz is a Lie group.
- Prove that the restricted Lorentz group is equivalent to the connected component of the
identity.
- Define the continuous maps from `ℝ³` to `restrictedLorentzGroup` defining boosts.
## References
- http://home.ku.edu.tr/~amostafazadeh/phys517_518/phys517_2016f/Handouts/A_Jaffi_Lorentz_Group.pdf
-/
/-! TODO: Show that the Lorentz is a Lie group. -/
/-! TODO: Prove restricted Lorentz group equivalent to connected component of identity. -/
noncomputable section
@ -44,7 +39,6 @@ def LorentzGroup (d : ℕ) : Set (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⟫ₘ}
namespace LorentzGroup
/-- Notation for the Lorentz group. -/
scoped[LorentzGroup] notation (name := lorentzGroup_notation) "𝓛" => LorentzGroup

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

@ -16,17 +16,13 @@ a four velocity `u` to a four velocity `v`.
A boost is the special case of a generalised boost when `u = stdBasis 0`.
## TODO
- Show that generalised boosts are in the restricted Lorentz group.
- Define boosts.
## References
- The main argument follows: Guillem Cobos, The Lorentz Group, 2015:
https://diposit.ub.edu/dspace/bitstream/2445/68763/2/memoria.pdf
-/
/-! TODO: Show that generalised boosts are in the restricted Lorentz group. -/
noncomputable section
namespace LorentzGroup
@ -140,7 +136,6 @@ lemma toMatrix_continuous (u : FuturePointing d) : Continuous (toMatrix u) := by
exact FuturePointing.metric_continuous _
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
intro x y
rw [toMatrix_mulVec, toMatrix_mulVec, genBoost, genBoostAux₁, genBoostAux₂]
@ -161,7 +156,6 @@ lemma toLorentz_continuous (u : FuturePointing d) : Continuous (toLorentz u) :=
refine Continuous.subtype_mk ?_ (fun x => toMatrix_in_lorentzGroup u x)
exact toMatrix_continuous u
lemma toLorentz_joined_to_1 (u v : FuturePointing d) : Joined 1 (toLorentz u v) := by
obtain ⟨f, _⟩ := FuturePointing.isPathConnected.joinedIn u trivial v trivial
use ContinuousMap.comp ⟨toLorentz u, toLorentz_continuous u⟩ f
@ -180,8 +174,6 @@ lemma isProper (u v : FuturePointing d) : IsProper (toLorentz u v) :=
end genBoost
end LorentzGroup
end

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

@ -11,16 +11,11 @@ import HepLean.SpaceTime.LorentzGroup.Proper
We define the give a series of lemmas related to the orthochronous property of lorentz
matrices.
## TODO
- Prove topological properties.
-/
/-! TODO: Prove topological properties of the Orthochronous Lorentz Group. -/
noncomputable section
open Matrix
open Complex
open ComplexConjugate
@ -66,7 +61,6 @@ lemma not_orthochronous_iff_le_zero :
rw [IsOrthochronous_iff_ge_one]
linarith
/-- The continuous map taking a Lorentz transformation to its `0 0` element. -/
def timeCompCont : C(LorentzGroup d, ℝ) := ⟨fun Λ => timeComp Λ ,
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
open Matrix
open Complex
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
exact mul_self_eq_one_iff.mp h1
local notation "ℤ₂" => Multiplicative (ZMod 2)
instance : TopologicalSpace ℤ₂ := instTopologicalSpaceFin
@ -76,7 +73,6 @@ lemma detContinuous_eq_iff_det_eq (Λ Λ' : LorentzGroup d) :
· intro h
simp [detContinuous, h]
/-- The representation taking a lorentz matrix to its determinant. -/
@[simps!]
def detRep : 𝓛 d →* ℤ₂ where

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

@ -11,11 +11,8 @@ import Mathlib.Topology.Constructions
This file describes the embedding of `SO(3)` into `LorentzGroup 3`.
## TODO
Generalize to arbitrary dimensions.
-/
/-! TODO: Generalize the inclusion of rotations into LorentzGroup to abitary dimension. -/
noncomputable section
namespace LorentzGroup
@ -54,8 +51,6 @@ def SO3ToLorentz : SO(3) →* LorentzGroup 3 where
apply Subtype.eq
simp [Matrix.fromBlocks_multiply]
end LorentzGroup
end

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

@ -13,11 +13,8 @@ and the vector space of 2×2-complex self-adjoint matrices.
In this file we define this linear equivalence in `toSelfAdjointMatrix`.
## TODO
If possible generalize to arbitrary dimensions.
-/
/-! TODO: Generalize rep of Lorentz vector as a self-adjoint matrix to arbitrary dimension. -/
namespace SpaceTime
open Matrix
@ -52,7 +49,6 @@ noncomputable def fromSelfAdjointMatrix' (x : selfAdjoint (Matrix (Fin 2) (Fin 2
| Sum.inr 1 => (x.1 1 0).im
| 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
2×2-complex matrices. -/
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
simp only [time, Fin.isValue, stdBasis_apply, ↓reduceIte]
/-!
# 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
linarith
lemma time_nonneg_iff : 0 ≤ v.1.time ↔ 1 ≤ v.1.time := by
apply Iff.intro
· 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⟫_ℝ|) ?_
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) :
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)
apply le_of_le_of_eq h1 ?_
simp [neg]
lemma metric_reflect_mem_not_mem (h : v ∈ FuturePointing d) (hw : w ∉ FuturePointing d) :
⟪v.1, w.1.spaceReflection⟫ₘ ≤ 0 := by
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 [mem_iff, timeVec_time]; exact Real.zero_lt_one⟩
/-- A continuous path from `timeVecNormOneFuture` to any other. -/
noncomputable def pathFromTime (u : FuturePointing d) : Path timeVecNormOneFuture u where
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]
exact rfl
lemma isPathConnected : IsPathConnected (@Set.univ (FuturePointing d)) := by
use timeVecNormOneFuture
apply And.intro trivial ?_
@ -276,7 +269,6 @@ lemma isPathConnected : IsPathConnected (@Set.univ (FuturePointing d)) := by
use pathFromTime y
exact fun _ => a
lemma metric_continuous (u : LorentzVector d) :
Continuous (fun (a : FuturePointing d) => ⟪u, a.1.1⟫ₘ) := by
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_subtype_val continuous_subtype_val))
end FuturePointing
end NormOneLorentzVector

15
HepLean/SpaceTime/MinkowskiMetric.lean
View file

@ -11,12 +11,11 @@ import Mathlib.Algebra.Lie.Classical
This file introduces the Minkowski metric on spacetime in the mainly-minus signature.
We define the minkowski metric as a bilinear map on the vector space
We define the Minkowski metric as a bilinear map on the vector space
of Lorentz vectors in d dimensions.
-/
open Matrix
/-!
@ -55,7 +54,6 @@ lemma sq : @minkowskiMatrix d * minkowskiMatrix = 1 := by
lemma eq_transpose : minkowskiMatrixᵀ = @minkowskiMatrix d := by
simp only [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal, diagonal_transpose]
@[simp]
lemma det_eq_neg_one_pow_d : (@minkowskiMatrix d).det = (- 1) ^ d := by
simp [minkowskiMatrix, LieAlgebra.Orthogonal.indefiniteDiagonal]
@ -71,17 +69,15 @@ lemma as_block : @minkowskiMatrix d = (
rw [← diagonal_neg]
rfl
end minkowskiMatrix
/-!
# The definition of the Minkowski Metric
-/
/-- Given a Lorentz vector `v` we define the the linear map `w ↦ v * η * w -/
/-- Given a Lorentz vector `v` we define the the linear map `w ↦ v * η * w` -/
@[simps!]
def minkowskiLinearForm {d : ℕ} (v : LorentzVector d) : LorentzVector d →ₗ[ℝ] ℝ where
toFun w := v ⬝ᵥ (minkowskiMatrix *ᵥ w)
@ -133,7 +129,6 @@ lemma as_sum :
Function.comp_apply, minkowskiMatrix]
ring
/-- The Minkowski metric expressed as a sum for a single vector. -/
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]
@ -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,
RCLike.inner_apply, conj_trivial, sub_neg_eq_add]
lemma self_spaceReflection_eq_zero_iff : ⟪v, v.spaceReflection⟫ₘ = 0 ↔ v = 0 := by
refine Iff.intro (fun h => ?_) (fun h => ?_)
· rw [right_spaceReflection] at h
@ -195,10 +189,9 @@ lemma nondegenerate : (∀ w, ⟪w, v⟫ₘ = 0) ↔ v = 0 := by
· exact (self_spaceReflection_eq_zero_iff _ ).mp ((symm _ _).trans $ h v.spaceReflection)
· simp [h]
/-!
# Inequalitites involving the Minkowski metric
# Inequalities 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]
exact norm_inner_le_norm v.space w.space
/-!
# 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]
simp
/-!
# The Minkowski metric and the standard basis

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

@ -124,14 +124,9 @@ def toLorentzGroup : SL(2, ℂ) →* LorentzGroup 3 where
The homomorphism `toLorentzGroup` restricts to a homomorphism to the restricted Lorentz group.
In this section we will define this homomorphism.
### TODO
Complete this section.
-/
/-! TODO: Define homomorphism from `SL(2, ℂ)` to the restricted Lorentz group. -/
end
end SL2C

8
HepLean/StandardModel/Basic.lean
View file

@ -11,12 +11,8 @@ import Mathlib.LinearAlgebra.Matrix.ToLin
This file defines the basic properties of the standard model in particle physics.
## TODO
- Change the gauge group to a quotient of SU(3) x SU(2) x U(1) by a subgroup of ℤ₆.
(see e.g. pg 97 of http://www.damtp.cam.ac.uk/user/tong/gaugetheory/gt.pdf)
-/
/-! TODO: Redefine the gauge group as a quotient of SU(3) x SU(2) x U(1) by a subgroup of ℤ₆. -/
universe v u
namespace StandardModel
@ -25,7 +21,7 @@ open Matrix
open Complex
open ComplexConjugate
/-- The global gauge group of the standard model. TODO: Generalize to quotient. -/
/-- The global gauge group of the standard model. -/
abbrev GaugeGroup : Type :=
specialUnitaryGroup (Fin 3) ℂ × specialUnitaryGroup (Fin 2) ℂ × unitary ℂ

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

@ -4,29 +4,25 @@ Released under Apache 2.0 license.
Authors: Joseph Tooby-Smith
-/
import HepLean.SpaceTime.Basic
import HepLean.StandardModel.Basic
import HepLean.StandardModel.HiggsBoson.TargetSpace
import Mathlib.Data.Complex.Exponential
import Mathlib.Tactic.Polyrith
import Mathlib.Geometry.Manifold.VectorBundle.Basic
import Mathlib.Geometry.Manifold.VectorBundle.SmoothSection
import Mathlib.Geometry.Manifold.Instances.Real
import Mathlib.RepresentationTheory.Basic
import Mathlib.Analysis.InnerProductSpace.Basic
import Mathlib.Analysis.InnerProductSpace.Adjoint
import Mathlib.Geometry.Manifold.ContMDiff.Product
import Mathlib.Algebra.QuadraticDiscriminant
/-!
# The Higgs field
This file defines the basic properties for the higgs field in the standard model.
This file defines the basic properties for the Higgs field in the standard model.
## References
- We use conventions given in: https://pdg.lbl.gov/2019/reviews/rpp2019-rev-higgs-boson.pdf
- We use conventions given in: [Review of Particle Physics, PDG][ParticleDataGroup:2018ovx]
-/
universe v u
namespace StandardModel
noncomputable section
@ -36,21 +32,58 @@ open Complex
open ComplexConjugate
open SpaceTime
/-- The trivial vector bundle 𝓡² × ℂ². (TODO: Make associated bundle.) -/
/-!
## The definition of the Higgs vector space.
In other words, the target space of the Higgs field.
-/
/-- The complex vector space in which the Higgs field takes values. -/
abbrev HiggsVec := EuclideanSpace ℂ (Fin 2)
namespace HiggsVec
/-- The continuous linear map from the vector space `HiggsVec` to `(Fin 2 → ℂ)` achieved by
casting vectors. -/
def toFin2ℂ : HiggsVec →L[ℝ] (Fin 2 → ℂ) where
toFun x := x
map_add' x y := by simp
map_smul' a x := by simp
/-- The map `toFin2ℂ` is smooth. -/
lemma smooth_toFin2ℂ : Smooth 𝓘(ℝ, HiggsVec) 𝓘(ℝ, Fin 2 → ℂ) toFin2ℂ :=
ContinuousLinearMap.smooth toFin2ℂ
/-- An orthonormal basis of `HiggsVec`. -/
def orthonormBasis : OrthonormalBasis (Fin 2) ℂ HiggsVec :=
EuclideanSpace.basisFun (Fin 2) ℂ
end HiggsVec
/-!
## Definition of the Higgs Field
We also define the Higgs bundle.
-/
/-! TODO: Make `HiggsBundle` an associated bundle. -/
/-- The trivial vector bundle 𝓡² × ℂ². -/
abbrev HiggsBundle := Bundle.Trivial SpaceTime HiggsVec
instance : SmoothVectorBundle HiggsVec HiggsBundle SpaceTime.asSmoothManifold :=
Bundle.Trivial.smoothVectorBundle HiggsVec 𝓘(ℝ, SpaceTime)
/-- A higgs field is a smooth section of the higgs bundle. -/
/-- A Higgs field is a smooth section of the Higgs bundle. -/
abbrev HiggsField : Type := SmoothSection SpaceTime.asSmoothManifold HiggsVec HiggsBundle
instance : NormedAddCommGroup (Fin 2 → ℂ) := by
exact Pi.normedAddCommGroup
/-- Given a vector `ℂ²` the constant higgs field with value equal to that
/-- Given a vector in `HiggsVec` the constant Higgs field with value equal to that
section. -/
noncomputable def HiggsVec.toField (φ : HiggsVec) : HiggsField where
def HiggsVec.toField (φ : HiggsVec) : HiggsField where
toFun := fun _ ↦ φ
contMDiff_toFun := by
intro x
@ -58,9 +91,15 @@ noncomputable def HiggsVec.toField (φ : HiggsVec) : HiggsField where
exact smoothAt_const
namespace HiggsField
open Complex Real
open HiggsVec
/-- Given a `higgsField`, the corresponding map from `spaceTime` to `higgsVec`. -/
/-!
## Relation to `HiggsVec`
-/
/-- Given a `HiggsField`, the corresponding map from `SpaceTime` to `HiggsVec`. -/
def toHiggsVec (φ : HiggsField) : SpaceTime → HiggsVec := φ
lemma toHiggsVec_smooth (φ : HiggsField) : Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ, HiggsVec) φ.toHiggsVec := by
@ -77,85 +116,37 @@ lemma toHiggsVec_smooth (φ : HiggsField) : Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ
lemma toField_toHiggsVec_apply (φ : HiggsField) (x : SpaceTime) :
(φ.toHiggsVec x).toField x = φ x := rfl
lemma higgsVecToFin2ℂ_toHiggsVec (φ : HiggsField) :
higgsVecToFin2ℂ ∘ φ.toHiggsVec = φ := rfl
lemma toFin2ℂ_comp_toHiggsVec (φ : HiggsField) :
toFin2ℂ ∘ φ.toHiggsVec = φ := rfl
/-!
## Smoothness properties of components
-/
lemma toVec_smooth (φ : HiggsField) : Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ, Fin 2 → ℂ) φ :=
smooth_higgsVecToFin2ℂ.comp φ.toHiggsVec_smooth
smooth_toFin2ℂ.comp φ.toHiggsVec_smooth
lemma apply_smooth (φ : HiggsField) :
∀ i, Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℂ) (fun (x : SpaceTime) => (φ x i)) :=
(smooth_pi_space).mp (φ.toVec_smooth)
lemma apply_re_smooth (φ : HiggsField) (i : Fin 2):
lemma apply_re_smooth (φ : HiggsField) (i : Fin 2) :
Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℝ) (reCLM ∘ (fun (x : SpaceTime) => (φ x i))) :=
(ContinuousLinearMap.smooth reCLM).comp (φ.apply_smooth i)
lemma apply_im_smooth (φ : HiggsField) (i : Fin 2):
lemma apply_im_smooth (φ : HiggsField) (i : Fin 2) :
Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℝ) (imCLM ∘ (fun (x : SpaceTime) => (φ x i))) :=
(ContinuousLinearMap.smooth imCLM).comp (φ.apply_smooth i)
/-- Given two `higgsField`, the map `spaceTime → ℂ` obtained by taking their inner product. -/
def innerProd (φ1 φ2 : HiggsField) : SpaceTime → ℂ := fun x => ⟪φ1 x, φ2 x⟫_ℂ
/-!
## Constant Higgs fields
/-- Given a `higgsField`, the map `spaceTime → ℝ` obtained by taking the square norm of the
higgs vector. -/
@[simp]
def normSq (φ : HiggsField) : SpaceTime → ℝ := fun x => ( ‖φ x‖ ^ 2)
-/
lemma toHiggsVec_norm (φ : HiggsField) (x : SpaceTime) :
‖φ x‖ = ‖φ.toHiggsVec x‖ := rfl
lemma normSq_expand (φ : HiggsField) :
φ.normSq = fun x => (conj (φ x 0) * (φ x 0) + conj (φ x 1) * (φ x 1) ).re := by
funext x
simp [normSq, add_re, mul_re, conj_re, conj_im, neg_mul, sub_neg_eq_add, @norm_sq_eq_inner ℂ]
lemma normSq_smooth (φ : HiggsField) : Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℝ) φ.normSq := by
rw [normSq_expand]
refine Smooth.add ?_ ?_
simp only [mul_re, conj_re, conj_im, neg_mul, sub_neg_eq_add]
refine Smooth.add ?_ ?_
refine Smooth.smul ?_ ?_
exact φ.apply_re_smooth 0
exact φ.apply_re_smooth 0
refine Smooth.smul ?_ ?_
exact φ.apply_im_smooth 0
exact φ.apply_im_smooth 0
simp only [mul_re, conj_re, conj_im, neg_mul, sub_neg_eq_add]
refine Smooth.add ?_ ?_
refine Smooth.smul ?_ ?_
exact φ.apply_re_smooth 1
exact φ.apply_re_smooth 1
refine Smooth.smul ?_ ?_
exact φ.apply_im_smooth 1
exact φ.apply_im_smooth 1
lemma normSq_nonneg (φ : HiggsField) (x : SpaceTime) : 0 ≤ φ.normSq x := by
simp [normSq, ge_iff_le, norm_nonneg, pow_nonneg]
lemma normSq_zero (φ : HiggsField) (x : SpaceTime) : φ.normSq x = 0 ↔ φ x = 0 := by
simp [normSq, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff, norm_eq_zero]
/-- The Higgs potential of the form `- μ² * |φ|² + λ * |φ|⁴`. -/
@[simp]
def potential (φ : HiggsField) (μSq lambda : ℝ ) (x : SpaceTime) : ℝ :=
- μSq * φ.normSq x + lambda * φ.normSq x * φ.normSq x
lemma potential_smooth (φ : HiggsField) (μSq lambda : ℝ) :
Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℝ) (fun x => φ.potential μSq lambda x) := by
simp only [potential, normSq, neg_mul]
exact (smooth_const.smul φ.normSq_smooth).neg.add
((smooth_const.smul φ.normSq_smooth).smul φ.normSq_smooth)
lemma potential_apply (φ : HiggsField) (μSq lambda : ℝ) (x : SpaceTime) :
(φ.potential μSq lambda) x = HiggsVec.potential μSq lambda (φ.toHiggsVec x) := by
simp [HiggsVec.potential, toHiggsVec_norm]
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
lemma isConst_of_higgsVec (φ : HiggsVec) : φ.toField.IsConst := by
@ -165,17 +156,7 @@ lemma isConst_of_higgsVec (φ : HiggsVec) : φ.toField.IsConst := by
lemma isConst_iff_of_higgsVec (Φ : HiggsField) : Φ.IsConst ↔ ∃ (φ : HiggsVec), Φ = φ.toField :=
Iff.intro (fun h ↦ ⟨Φ 0, by ext x y; rw [← h x 0]; rfl⟩) (fun ⟨φ, hφ⟩ x y ↦ by subst hφ; rfl)
lemma normSq_of_higgsVec (φ : HiggsVec) : φ.toField.normSq = fun x => (norm φ) ^ 2 := by
funext x
simp [normSq, HiggsVec.toField]
lemma potential_of_higgsVec (φ : HiggsVec) (μSq lambda : ℝ) :
φ.toField.potential μSq lambda = fun _ => HiggsVec.potential μSq lambda φ := by
simp [HiggsVec.potential]
unfold potential
rw [normSq_of_higgsVec]
ring_nf
end HiggsField
end
end StandardModel

173
HepLean/StandardModel/HiggsBoson/GaugeAction.lean Normal file
View file

@ -0,0 +1,173 @@
/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license.
Authors: Joseph Tooby-Smith
-/
import HepLean.StandardModel.HiggsBoson.Basic
import Mathlib.RepresentationTheory.Basic
import HepLean.StandardModel.Basic
import HepLean.StandardModel.Representations
import Mathlib.Analysis.InnerProductSpace.Adjoint
/-!
# The action of the gauge group on the Higgs field
-/
/-! TODO: Currently this only contains the action of the global gauge group. Generalize. -/
noncomputable section
namespace StandardModel
namespace HiggsVec
open Manifold
open Matrix
open Complex
open ComplexConjugate
/-!
## The representation of the gauge group on the Higgs vector space
-/
/-- The Higgs representation as a homomorphism from the gauge group to unitary `2×2`-matrices. -/
@[simps!]
noncomputable def higgsRepUnitary : GaugeGroup →* unitaryGroup (Fin 2) ℂ where
toFun g := repU1 g.2.2 * fundamentalSU2 g.2.1
map_mul' := by
intro ⟨_, a2, a3⟩ ⟨_, b2, b3⟩
change repU1 (a3 * b3) * fundamentalSU2 (a2 * b2) = _
rw [repU1.map_mul, fundamentalSU2.map_mul, mul_assoc, mul_assoc,
← mul_assoc (repU1 b3) _ _, repU1_fundamentalSU2_commute]
repeat rw [mul_assoc]
map_one' := by simp
/-- Takes in a `2×2`-matrix and returns a linear map of `higgsVec`. -/
noncomputable def matrixToLin : Matrix (Fin 2) (Fin 2) ℂ →* (HiggsVec →L[ℂ] HiggsVec) where
toFun g := LinearMap.toContinuousLinearMap
$ Matrix.toLin orthonormBasis.toBasis orthonormBasis.toBasis g
map_mul' g h := ContinuousLinearMap.coe_inj.mp $
Matrix.toLin_mul orthonormBasis.toBasis orthonormBasis.toBasis orthonormBasis.toBasis g h
map_one' := ContinuousLinearMap.coe_inj.mp $ Matrix.toLin_one orthonormBasis.toBasis
lemma matrixToLin_star (g : Matrix (Fin 2) (Fin 2) ℂ) :
matrixToLin (star g) = star (matrixToLin g) :=
ContinuousLinearMap.coe_inj.mp $ Matrix.toLin_conjTranspose orthonormBasis orthonormBasis g
lemma matrixToLin_unitary (g : unitaryGroup (Fin 2) ℂ) :
matrixToLin g ∈ unitary (HiggsVec →L[ℂ] HiggsVec) := by
rw [@unitary.mem_iff, ← matrixToLin_star, ← matrixToLin.map_mul, ← matrixToLin.map_mul,
mem_unitaryGroup_iff.mp g.prop, mem_unitaryGroup_iff'.mp g.prop, matrixToLin.map_one]
simp
/-- The natural homomorphism from unitary `2×2` complex matrices to unitary transformations
of `higgsVec`. -/
noncomputable def unitaryToLin : unitaryGroup (Fin 2) ℂ →* unitary (HiggsVec →L[ℂ] HiggsVec) where
toFun g := ⟨matrixToLin g, matrixToLin_unitary g⟩
map_mul' g h := by simp
map_one' := by simp
/-- The inclusion of unitary transformations on `higgsVec` into all linear transformations. -/
@[simps!]
def unitToLinear : unitary (HiggsVec →L[ℂ] HiggsVec) →* HiggsVec →ₗ[ℂ] HiggsVec :=
DistribMulAction.toModuleEnd ℂ HiggsVec
/-- The representation of the gauge group acting on `higgsVec`. -/
@[simps!]
def rep : Representation ℂ GaugeGroup HiggsVec :=
unitToLinear.comp (unitaryToLin.comp higgsRepUnitary)
lemma higgsRepUnitary_mul (g : GaugeGroup) (φ : HiggsVec) :
(higgsRepUnitary g).1 *ᵥ φ = g.2.2 ^ 3 • (g.2.1.1 *ᵥ φ) := by
simp [higgsRepUnitary_apply_coe, smul_mulVec_assoc]
lemma rep_apply (g : GaugeGroup) (φ : HiggsVec) : rep g φ = g.2.2 ^ 3 • (g.2.1.1 *ᵥ φ) :=
higgsRepUnitary_mul g φ
/-!
# Gauge freedom
-/
/-- Given a Higgs vector, a rotation matrix which puts the first component of the
vector to zero, and the second component to a real -/
def rotateMatrix (φ : HiggsVec) : Matrix (Fin 2) (Fin 2) ℂ :=
![![φ 1 /‖φ‖ , - φ 0 /‖φ‖], ![conj (φ 0) / ‖φ‖ , conj (φ 1) / ‖φ‖] ]
lemma rotateMatrix_star (φ : HiggsVec) :
star φ.rotateMatrix =
![![conj (φ 1) /‖φ‖ , φ 0 /‖φ‖], ![- conj (φ 0) / ‖φ‖ , φ 1 / ‖φ‖] ] := by
simp_rw [star, rotateMatrix, conjTranspose]
ext i j
fin_cases i <;> fin_cases j <;> simp [conj_ofReal]
lemma rotateMatrix_det {φ : HiggsVec} (hφ : φ ≠ 0) : (rotateMatrix φ).det = 1 := by
have h1 : (‖φ‖ : ℂ) ≠ 0 := ofReal_inj.mp.mt (norm_ne_zero_iff.mpr hφ)
field_simp [rotateMatrix, det_fin_two]
rw [← ofReal_mul, ← sq, ← @real_inner_self_eq_norm_sq]
simp [PiLp.inner_apply, Complex.inner, neg_mul, sub_neg_eq_add,
Fin.sum_univ_two, ofReal_add, ofReal_mul, mul_conj, mul_comm, add_comm]
lemma rotateMatrix_unitary {φ : HiggsVec} (hφ : φ ≠ 0) :
(rotateMatrix φ) ∈ unitaryGroup (Fin 2) ℂ := by
rw [mem_unitaryGroup_iff', rotateMatrix_star, rotateMatrix]
erw [mul_fin_two, one_fin_two]
have : (‖φ‖ : ℂ) ≠ 0 := ofReal_inj.mp.mt (norm_ne_zero_iff.mpr hφ)
ext i j
fin_cases i <;> fin_cases j <;> field_simp
<;> rw [← ofReal_mul, ← sq, ← @real_inner_self_eq_norm_sq]
· simp [PiLp.inner_apply, Complex.inner, neg_mul, sub_neg_eq_add,
Fin.sum_univ_two, ofReal_add, ofReal_mul, mul_conj, mul_comm, add_comm]
· ring_nf
· ring_nf
· simp [PiLp.inner_apply, Complex.inner, neg_mul, sub_neg_eq_add,
Fin.sum_univ_two, ofReal_add, ofReal_mul, mul_conj, mul_comm]
lemma rotateMatrix_specialUnitary {φ : HiggsVec} (hφ : φ ≠ 0) :
(rotateMatrix φ) ∈ specialUnitaryGroup (Fin 2) ℂ :=
mem_specialUnitaryGroup_iff.mpr ⟨rotateMatrix_unitary hφ, rotateMatrix_det hφ⟩
/-- Given a Higgs vector, an element of the gauge group which puts the first component of the
vector to zero, and the second component to a real -/
def rotateGuageGroup {φ : HiggsVec} (hφ : φ ≠ 0) : GaugeGroup :=
⟨1, ⟨(rotateMatrix φ), rotateMatrix_specialUnitary hφ⟩, 1⟩
lemma rotateGuageGroup_apply {φ : HiggsVec} (hφ : φ ≠ 0) :
rep (rotateGuageGroup hφ) φ = ![0, ofReal ‖φ‖] := by
rw [rep_apply]
simp only [rotateGuageGroup, rotateMatrix, one_pow, one_smul,
Nat.succ_eq_add_one, Nat.reduceAdd, ofReal_eq_coe]
ext i
fin_cases i
· simp only [mulVec, Fin.zero_eta, Fin.isValue, cons_val', empty_val', cons_val_fin_one,
cons_val_zero, cons_dotProduct, vecHead, vecTail, Nat.succ_eq_add_one, Nat.reduceAdd,
Function.comp_apply, Fin.succ_zero_eq_one, dotProduct_empty, add_zero]
ring_nf
· simp only [Fin.mk_one, Fin.isValue, cons_val_one, head_cons, mulVec, Fin.isValue,
cons_val', empty_val', cons_val_fin_one, vecHead, cons_dotProduct, vecTail, Nat.succ_eq_add_one,
Nat.reduceAdd, Function.comp_apply, Fin.succ_zero_eq_one, dotProduct_empty, add_zero]
have : (‖φ‖ : ℂ) ≠ 0 := ofReal_inj.mp.mt (norm_ne_zero_iff.mpr hφ)
field_simp
rw [← ofReal_mul, ← sq, ← @real_inner_self_eq_norm_sq]
simp [PiLp.inner_apply, Complex.inner, neg_mul, sub_neg_eq_add,
Fin.sum_univ_two, ofReal_add, ofReal_mul, mul_conj, mul_comm]
theorem rotate_fst_zero_snd_real (φ : HiggsVec) :
∃ (g : GaugeGroup), rep g φ = ![0, ofReal ‖φ‖] := by
by_cases h : φ = 0
· use ⟨1, 1, 1⟩
simp [h]
ext i
fin_cases i <;> rfl
· use rotateGuageGroup h
exact rotateGuageGroup_apply h
end HiggsVec
/-! TODO: Define the global gauge action on HiggsField. -/
/-! TODO: Prove `⟪φ1, φ2⟫_H` invariant under the global gauge action. (norm_map_of_mem_unitary) -/
/-! TODO: Prove invariance of potential under global gauge action. -/
end StandardModel
end

153
HepLean/StandardModel/HiggsBoson/PointwiseInnerProd.lean Normal file
View file

@ -0,0 +1,153 @@
/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license.
Authors: Joseph Tooby-Smith
-/
import HepLean.StandardModel.HiggsBoson.Basic
/-!
# The pointwise inner product
We define the pointwise inner product of two Higgs fields.
The notation for the inner product is `⟪φ, ψ⟫_H`.
We also define the pointwise norm squared of a Higgs field `∥φ∥_H ^ 2`.
-/
noncomputable section
namespace StandardModel
namespace HiggsField
open Manifold
open Matrix
open Complex
open ComplexConjugate
open SpaceTime
/-!
## The pointwise inner product
-/
/-- Given two `HiggsField`, the map `SpaceTime → ℂ` obtained by taking their pointwise
inner product. -/
def innerProd (φ1 φ2 : HiggsField) : SpaceTime → ℂ := fun x => ⟪φ1 x, φ2 x⟫_ℂ
/-- Notation for the inner product of two Higgs fields. -/
scoped[StandardModel.HiggsField] notation "⟪" φ1 "," φ2 "⟫_H" => innerProd φ1 φ2
/-!
## Properties of the inner product
-/
@[simp]
lemma innerProd_left_zero (φ : HiggsField) : ⟪0, φ⟫_H = 0 := by
funext x
simp [innerProd]
@[simp]
lemma innerProd_right_zero (φ : HiggsField) : ⟪φ, 0⟫_H = 0 := by
funext x
simp [innerProd]
example (x : ℝ): RCLike.ofReal x = ofReal' x := by
rfl
lemma innerProd_expand (φ1 φ2 : HiggsField) :
⟪φ1, φ2⟫_H = fun x => equivRealProdCLM.symm (((φ1 x 0).re * (φ2 x 0).re
+ (φ1 x 1).re * (φ2 x 1).re+ (φ1 x 0).im * (φ2 x 0).im + (φ1 x 1).im * (φ2 x 1).im),
((φ1 x 0).re * (φ2 x 0).im + (φ1 x 1).re * (φ2 x 1).im
- (φ1 x 0).im * (φ2 x 0).re - (φ1 x 1).im * (φ2 x 1).re)) := by
funext x
simp only [innerProd, PiLp.inner_apply, RCLike.inner_apply, Fin.sum_univ_two,
equivRealProdCLM_symm_apply, ofReal_add, ofReal_mul, ofReal_sub]
rw [RCLike.conj_eq_re_sub_im, RCLike.conj_eq_re_sub_im]
nth_rewrite 1 [← RCLike.re_add_im (φ2 x 0)]
nth_rewrite 1 [← RCLike.re_add_im (φ2 x 1)]
ring_nf
repeat rw [show RCLike.ofReal _ = ofReal' _ by rfl]
simp only [Algebra.id.map_eq_id, RCLike.re_to_complex, RingHom.id_apply, RCLike.I_to_complex,
RCLike.im_to_complex, I_sq, mul_neg, mul_one, neg_mul, sub_neg_eq_add, one_mul]
ring
lemma smooth_innerProd (φ1 φ2 : HiggsField) : Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℂ) ⟪φ1, φ2⟫_H := by
rw [innerProd_expand]
exact (ContinuousLinearMap.smooth (equivRealProdCLM.symm : ℝ × ℝ →L[ℝ] ℂ)).comp $
(((((φ1.apply_re_smooth 0).smul (φ2.apply_re_smooth 0)).add
((φ1.apply_re_smooth 1).smul (φ2.apply_re_smooth 1))).add
((φ1.apply_im_smooth 0).smul (φ2.apply_im_smooth 0))).add
((φ1.apply_im_smooth 1).smul (φ2.apply_im_smooth 1))).prod_mk_space $
((((φ1.apply_re_smooth 0).smul (φ2.apply_im_smooth 0)).add
((φ1.apply_re_smooth 1).smul (φ2.apply_im_smooth 1))).sub
((φ1.apply_im_smooth 0).smul (φ2.apply_re_smooth 0))).sub
((φ1.apply_im_smooth 1).smul (φ2.apply_re_smooth 1))
/-!
## The pointwise norm squared
-/
/-- Given a `HiggsField`, the map `SpaceTime → ℝ` obtained by taking the square norm of the
pointwise Higgs vector. -/
@[simp]
def normSq (φ : HiggsField) : SpaceTime → ℝ := fun x => ( ‖φ x‖ ^ 2)
/-- Notation for the norm squared of a Higgs field. -/
scoped[StandardModel.HiggsField] notation "‖" φ1 "‖_H ^ 2" => normSq φ1
/-!
## Relation between inner prod and norm squared
-/
lemma innerProd_self_eq_normSq (φ : HiggsField) (x : SpaceTime) :
⟪φ, φ⟫_H x = ‖φ‖_H ^ 2 x := by
erw [normSq, @PiLp.norm_sq_eq_of_L2, Fin.sum_univ_two]
simp only [innerProd, PiLp.inner_apply, RCLike.inner_apply, conj_mul', norm_eq_abs,
Fin.sum_univ_two, ofReal_add, ofReal_pow]
lemma normSq_eq_innerProd_self (φ : HiggsField) (x : SpaceTime) :
‖φ x‖ ^ 2 = (⟪φ, φ⟫_H x).re := by
rw [innerProd_self_eq_normSq]
rfl
/-!
# Properties of the norm squared
-/
lemma toHiggsVec_norm (φ : HiggsField) (x : SpaceTime) :
‖φ x‖ = ‖φ.toHiggsVec x‖ := rfl
lemma normSq_expand (φ : HiggsField) :
φ.normSq = fun x => (conj (φ x 0) * (φ x 0) + conj (φ x 1) * (φ x 1) ).re := by
funext x
simp [normSq, add_re, mul_re, conj_re, conj_im, neg_mul, sub_neg_eq_add, @norm_sq_eq_inner ℂ]
lemma normSq_nonneg (φ : HiggsField) (x : SpaceTime) : 0 ≤ φ.normSq x := by
simp [normSq, ge_iff_le, norm_nonneg, pow_nonneg]
lemma normSq_zero (φ : HiggsField) (x : SpaceTime) : φ.normSq x = 0 ↔ φ x = 0 := by
simp [normSq, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff, norm_eq_zero]
lemma normSq_smooth (φ : HiggsField) : Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℝ) φ.normSq := by
rw [normSq_expand]
refine Smooth.add ?_ ?_
simp only [mul_re, conj_re, conj_im, neg_mul, sub_neg_eq_add]
exact ((φ.apply_re_smooth 0).smul (φ.apply_re_smooth 0)).add $
(φ.apply_im_smooth 0).smul (φ.apply_im_smooth 0)
simp only [mul_re, conj_re, conj_im, neg_mul, sub_neg_eq_add]
exact ((φ.apply_re_smooth 1).smul (φ.apply_re_smooth 1)).add $
(φ.apply_im_smooth 1).smul (φ.apply_im_smooth 1)
end HiggsField
end StandardModel
end

251
HepLean/StandardModel/HiggsBoson/Potential.lean Normal file
View file

@ -0,0 +1,251 @@
/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license.
Authors: Joseph Tooby-Smith
-/
import Mathlib.Algebra.QuadraticDiscriminant
import HepLean.StandardModel.HiggsBoson.PointwiseInnerProd
/-!
# The potential of the Higgs field
We define the potential of the Higgs field.
We show that the potential is a smooth function on spacetime.
-/
noncomputable section
namespace StandardModel
namespace HiggsField
open Manifold
open Matrix
open Complex
open ComplexConjugate
open SpaceTime
/-!
## The Higgs potential
-/
/-- The Higgs potential of the form `- μ² * |φ|² + 𝓵 * |φ|⁴`. -/
@[simp]
def potential (μ2 𝓵 : ℝ ) (φ : HiggsField) (x : SpaceTime) : ℝ :=
- μ2 * ‖φ‖_H ^ 2 x + 𝓵 * ‖φ‖_H ^ 2 x * ‖φ‖_H ^ 2 x
/-!
## Smoothness of the potential
-/
lemma potential_smooth (μSq lambda : ℝ) (φ : HiggsField) :
Smooth 𝓘(ℝ, SpaceTime) 𝓘(ℝ, ℝ) (fun x => φ.potential μSq lambda x) := by
simp only [potential, normSq, neg_mul]
exact (smooth_const.smul φ.normSq_smooth).neg.add
((smooth_const.smul φ.normSq_smooth).smul φ.normSq_smooth)
namespace potential
/-!
## Basic properties
-/
lemma complete_square (μ2 𝓵 : ℝ) (h : 𝓵 ≠ 0) (φ : HiggsField) (x : SpaceTime) :
potential μ2 𝓵 φ x = 𝓵 * (‖φ‖_H ^ 2 x - μ2 / (2 * 𝓵)) ^ 2 - μ2 ^ 2 / (4 * 𝓵) := by
simp only [potential]
field_simp
ring
/-!
## Boundness of the potential
-/
/-- The proposition on the coefficents for a potential to be bounded. -/
def IsBounded (μ2 𝓵 : ℝ) : Prop :=
∃ c, ∀ Φ x, c ≤ potential μ2 𝓵 Φ x
/-! TODO: Show when 𝓵 < 0, the potential is not bounded. -/
section lowerBound
/-!
## Lower bound on potential
-/
variable {𝓵 : ℝ}
variable (μ2 : ℝ)
variable (h𝓵 : 0 < 𝓵)
/-- The second term of the potential is non-negative. -/
lemma snd_term_nonneg (φ : HiggsField) (x : SpaceTime) :
0 ≤ 𝓵 * ‖φ‖_H ^ 2 x * ‖φ‖_H ^ 2 x := by
rw [mul_nonneg_iff]
apply Or.inl
simp_all only [normSq, gt_iff_lt, mul_nonneg_iff_of_pos_left, ge_iff_le, norm_nonneg, pow_nonneg,
and_self]
lemma as_quad (μ2 𝓵 : ℝ) (φ : HiggsField) (x : SpaceTime) :
𝓵 * ‖φ‖_H ^ 2 x * ‖φ‖_H ^ 2 x + (- μ2 ) * ‖φ‖_H ^ 2 x + (- potential μ2 𝓵 φ x) = 0 := by
simp only [normSq, neg_mul, potential, neg_add_rev, neg_neg]
ring
/-- The discriminant of the quadratic formed by the potential is non-negative. -/
lemma discrim_nonneg (φ : HiggsField) (x : SpaceTime) :
0 ≤ discrim 𝓵 (- μ2) (- potential μ2 𝓵 φ x) := by
have h1 := as_quad μ2 𝓵 φ x
rw [quadratic_eq_zero_iff_discrim_eq_sq] at h1
· simp only [h1, ne_eq, div_eq_zero_iff, OfNat.ofNat_ne_zero, or_false]
exact sq_nonneg (2 * 𝓵 * ‖φ‖_H ^ 2 x+ - μ2)
· exact ne_of_gt h𝓵
lemma eq_zero_at (φ : HiggsField) (x : SpaceTime)
(hV : potential μ2 𝓵 φ x = 0) : φ x = 0 ∨ ‖φ‖_H ^ 2 x = μ2 / 𝓵 := by
have h1 := as_quad μ2 𝓵 φ x
rw [hV] at h1
have h2 : ‖φ‖_H ^ 2 x * (𝓵 * ‖φ‖_H ^ 2 x + - μ2) = 0 := by
linear_combination h1
simp at h2
cases' h2 with h2 h2
simp_all
apply Or.inr
field_simp at h2 ⊢
ring_nf
linear_combination h2
lemma eq_zero_at_of_μSq_nonpos {μ2 : ℝ} (hμ2 : μ2 ≤ 0)
(φ : HiggsField) (x : SpaceTime) (hV : potential μ2 𝓵 φ x = 0) : φ x = 0 := by
cases' (eq_zero_at μ2 h𝓵 φ x hV) with h1 h1
exact h1
by_cases hμSqZ : μ2 = 0
simpa [hμSqZ] using h1
refine ((?_ : ¬ 0 ≤ μ2 / 𝓵) (?_)).elim
· simp_all [div_nonneg_iff]
intro h
exact lt_imp_lt_of_le_imp_le (fun _ => h) (lt_of_le_of_ne hμ2 hμSqZ)
· rw [← h1]
exact normSq_nonneg φ x
lemma bounded_below (φ : HiggsField) (x : SpaceTime) :
- μ2 ^ 2 / (4 * 𝓵) ≤ potential μ2 𝓵 φ x := by
have h1 := discrim_nonneg μ2 h𝓵 φ x
simp only [discrim, even_two, Even.neg_pow, normSq, neg_mul, neg_add_rev, neg_neg] at h1
ring_nf at h1
rw [← neg_le_iff_add_nonneg'] at h1
rw [show 𝓵 * potential μ2 𝓵 φ x * 4 = (4 * 𝓵) * potential μ2 𝓵 φ x by ring] at h1
have h2 := (div_le_iff' (by simp [h𝓵] : 0 < 4 * 𝓵)).mpr h1
ring_nf at h2 ⊢
exact h2
lemma bounded_below_of_μSq_nonpos {μ2 : ℝ}
(hμSq : μ2 ≤ 0) (φ : HiggsField) (x : SpaceTime) : 0 ≤ potential μ2 𝓵 φ x := by
refine add_nonneg ?_ (snd_term_nonneg h𝓵 φ x)
field_simp [mul_nonpos_iff]
simp_all [ge_iff_le, norm_nonneg, pow_nonneg, and_self, or_true]
end lowerBound
section MinimumOfPotential
variable {𝓵 : ℝ}
variable (μ2 : ℝ)
variable (h𝓵 : 0 < 𝓵)
/-!
## Minima of potential
-/
lemma discrim_eq_zero_of_eq_bound (φ : HiggsField) (x : SpaceTime)
(hV : potential μ2 𝓵 φ x = - μ2 ^ 2 / (4 * 𝓵)) :
discrim 𝓵 (- μ2) (- potential μ2 𝓵 φ x) = 0 := by
rw [discrim, hV]
field_simp
lemma normSq_of_eq_bound (φ : HiggsField) (x : SpaceTime)
(hV : potential μ2 𝓵 φ x = - μ2 ^ 2 / (4 * 𝓵)) :
‖φ‖_H ^ 2 x = μ2 / (2 * 𝓵) := by
have h1 := as_quad μ2 𝓵 φ x
rw [quadratic_eq_zero_iff_of_discrim_eq_zero _
(discrim_eq_zero_of_eq_bound μ2 h𝓵 φ x hV)] at h1
simp_rw [h1, neg_neg]
exact ne_of_gt h𝓵
lemma eq_bound_iff (φ : HiggsField) (x : SpaceTime) :
potential μ2 𝓵 φ x = - μ2 ^ 2 / (4 * 𝓵) ↔ ‖φ‖_H ^ 2 x = μ2 / (2 * 𝓵) :=
Iff.intro (normSq_of_eq_bound μ2 h𝓵 φ x)
(fun h ↦ by
rw [potential, h]
field_simp
ring_nf)
lemma eq_bound_iff_of_μSq_nonpos {μ2 : ℝ}
(hμ2 : μ2 ≤ 0) (φ : HiggsField) (x : SpaceTime) :
potential μ2 𝓵 φ x = 0 ↔ φ x = 0 :=
Iff.intro (fun h ↦ eq_zero_at_of_μSq_nonpos h𝓵 hμ2 φ x h)
(fun h ↦ by simp [potential, h])
lemma eq_bound_IsMinOn (φ : HiggsField) (x : SpaceTime)
(hv : potential μ2 𝓵 φ x = - μ2 ^ 2 / (4 * 𝓵)) :
IsMinOn (fun (φ, x) => potential μ2 𝓵 φ x) Set.univ (φ, x) := by
rw [isMinOn_univ_iff]
simp only [normSq, neg_mul, le_neg_add_iff_add_le, ge_iff_le, hv]
exact fun (φ', x') ↦ bounded_below μ2 h𝓵 φ' x'
lemma eq_bound_IsMinOn_of_μSq_nonpos {μ2 : ℝ}
(hμ2 : μ2 ≤ 0) (φ : HiggsField) (x : SpaceTime) (hv : potential μ2 𝓵 φ x = 0) :
IsMinOn (fun (φ, x) => potential μ2 𝓵 φ x) Set.univ (φ, x) := by
rw [isMinOn_univ_iff]
simp only [normSq, neg_mul, le_neg_add_iff_add_le, ge_iff_le, hv]
exact fun (φ', x') ↦ bounded_below_of_μSq_nonpos h𝓵 hμ2 φ' x'
lemma bound_reached_of_μSq_nonneg {μ2 : ℝ} (hμ2 : 0 ≤ μ2) :
∃ (φ : HiggsField) (x : SpaceTime),
potential μ2 𝓵 φ x = - μ2 ^ 2 / (4 * 𝓵) := by
use HiggsVec.toField ![√(μ2/(2 * 𝓵)), 0], 0
refine (eq_bound_iff μ2 h𝓵 (HiggsVec.toField ![√(μ2/(2 * 𝓵)), 0]) 0).mpr ?_
simp only [normSq, HiggsVec.toField, ContMDiffSection.coeFn_mk, PiLp.norm_sq_eq_of_L2,
Nat.succ_eq_add_one, Nat.reduceAdd, norm_eq_abs, Fin.sum_univ_two, Fin.isValue, cons_val_zero,
abs_ofReal, _root_.sq_abs, cons_val_one, head_cons, map_zero, ne_eq, OfNat.ofNat_ne_zero,
not_false_eq_true, zero_pow, add_zero]
field_simp [mul_pow]
lemma IsMinOn_iff_of_μSq_nonneg {μ2 : ℝ} (hμ2 : 0 ≤ μ2) :
IsMinOn (fun (φ, x) => potential μ2 𝓵 φ x) Set.univ (φ, x) ↔
‖φ‖_H ^ 2 x = μ2 /(2 * 𝓵) := by
apply Iff.intro <;> rw [← eq_bound_iff μ2 h𝓵 φ]
· intro h
obtain ⟨φm, xm, hφ⟩ := bound_reached_of_μSq_nonneg h𝓵 hμ2
have hm := isMinOn_univ_iff.mp h (φm, xm)
simp only at hm
rw [hφ] at hm
exact (Real.partialOrder.le_antisymm _ _ (bounded_below μ2 h𝓵 φ x) hm).symm
· exact eq_bound_IsMinOn μ2 h𝓵 φ x
lemma IsMinOn_iff_of_μSq_nonpos {μ2 : ℝ} (hμ2 : μ2 ≤ 0) :
IsMinOn (fun (φ, x) => potential μ2 𝓵 φ x) Set.univ (φ, x) ↔ φ x = 0 := by
apply Iff.intro <;> rw [← eq_bound_iff_of_μSq_nonpos h𝓵 hμ2 φ]
· intro h
have h0 := isMinOn_univ_iff.mp h 0
have h1 := bounded_below_of_μSq_nonpos h𝓵 hμ2 φ x
simp only at h0
rw [(eq_bound_iff_of_μSq_nonpos h𝓵 hμ2 0 0 ).mpr (by rfl)] at h0
exact (Real.partialOrder.le_antisymm _ _ h1 h0).symm
· exact eq_bound_IsMinOn_of_μSq_nonpos h𝓵 hμ2 φ x
end MinimumOfPotential
end potential
end HiggsField
end StandardModel
end

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

@ -1,345 +0,0 @@
/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license.
Authors: Joseph Tooby-Smith
-/
import HepLean.StandardModel.Basic
import HepLean.StandardModel.Representations
import Mathlib.Data.Complex.Exponential
import Mathlib.Tactic.Polyrith
import Mathlib.Geometry.Manifold.Instances.Real
import Mathlib.RepresentationTheory.Basic
import Mathlib.Analysis.InnerProductSpace.Basic
import Mathlib.Analysis.InnerProductSpace.Adjoint
import Mathlib.Geometry.Manifold.ContMDiff.Product
import Mathlib.Algebra.QuadraticDiscriminant
import Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
/-!
# The Higgs vector space
This file defines the target vector space of the Higgs boson, the potential on it,
and the representation of the SM gauge group acting on it.
This file is a import of `SM.HiggsBoson.Basic`.
## References
- We use conventions given in: https://pdg.lbl.gov/2019/reviews/rpp2019-rev-higgs-boson.pdf
-/
universe v u
namespace StandardModel
noncomputable section
open Manifold
open Matrix
open Complex
open ComplexConjugate
/-- The complex vector space in which the Higgs field takes values. -/
abbrev HiggsVec := EuclideanSpace ℂ (Fin 2)
/-- The continuous linear map from the vector space `higgsVec` to `(Fin 2 → ℂ)` achieved by
casting vectors. -/
def higgsVecToFin2ℂ : HiggsVec →L[ℝ] (Fin 2 → ℂ) where
toFun x := x
map_add' x y := by simp
map_smul' a x := by simp
lemma smooth_higgsVecToFin2ℂ : Smooth 𝓘(ℝ, HiggsVec) 𝓘(ℝ, Fin 2 → ℂ) higgsVecToFin2ℂ :=
ContinuousLinearMap.smooth higgsVecToFin2ℂ
namespace HiggsVec
/-- The Higgs representation as a homomorphism from the gauge group to unitary `2×2`-matrices. -/
@[simps!]
noncomputable def higgsRepUnitary : GaugeGroup →* unitaryGroup (Fin 2) ℂ where
toFun g := repU1 g.2.2 * fundamentalSU2 g.2.1
map_mul' := by
intro ⟨_, a2, a3⟩ ⟨_, b2, b3⟩
change repU1 (a3 * b3) * fundamentalSU2 (a2 * b2) = _
rw [repU1.map_mul, fundamentalSU2.map_mul, mul_assoc, mul_assoc,
← mul_assoc (repU1 b3) _ _, repU1_fundamentalSU2_commute]
repeat rw [mul_assoc]
map_one' := by simp
/-- An orthonormal basis of higgsVec. -/
noncomputable def orthonormBasis : OrthonormalBasis (Fin 2) ℂ HiggsVec :=
EuclideanSpace.basisFun (Fin 2) ℂ
/-- Takes in a `2×2`-matrix and returns a linear map of `higgsVec`. -/
noncomputable def matrixToLin : Matrix (Fin 2) (Fin 2) ℂ →* (HiggsVec →L[ℂ] HiggsVec) where
toFun g := LinearMap.toContinuousLinearMap
$ Matrix.toLin orthonormBasis.toBasis orthonormBasis.toBasis g
map_mul' g h := ContinuousLinearMap.coe_inj.mp $
Matrix.toLin_mul orthonormBasis.toBasis orthonormBasis.toBasis orthonormBasis.toBasis g h
map_one' := ContinuousLinearMap.coe_inj.mp $ Matrix.toLin_one orthonormBasis.toBasis
lemma matrixToLin_star (g : Matrix (Fin 2) (Fin 2) ℂ) :
matrixToLin (star g) = star (matrixToLin g) :=
ContinuousLinearMap.coe_inj.mp $ Matrix.toLin_conjTranspose orthonormBasis orthonormBasis g
lemma matrixToLin_unitary (g : unitaryGroup (Fin 2) ℂ) :
matrixToLin g ∈ unitary (HiggsVec →L[ℂ] HiggsVec) := by
rw [@unitary.mem_iff, ← matrixToLin_star, ← matrixToLin.map_mul, ← matrixToLin.map_mul,
mem_unitaryGroup_iff.mp g.prop, mem_unitaryGroup_iff'.mp g.prop, matrixToLin.map_one]
simp
/-- The natural homomorphism from unitary `2×2` complex matrices to unitary transformations
of `higgsVec`. -/
noncomputable def unitaryToLin : unitaryGroup (Fin 2) ℂ →* unitary (HiggsVec →L[ℂ] HiggsVec) where
toFun g := ⟨matrixToLin g, matrixToLin_unitary g⟩
map_mul' g h := by simp
map_one' := by simp
/-- The inclusion of unitary transformations on `higgsVec` into all linear transformations. -/
@[simps!]
def unitToLinear : unitary (HiggsVec →L[ℂ] HiggsVec) →* HiggsVec →ₗ[ℂ] HiggsVec :=
DistribMulAction.toModuleEnd ℂ HiggsVec
/-- The representation of the gauge group acting on `higgsVec`. -/
@[simps!]
def rep : Representation ℂ GaugeGroup HiggsVec :=
unitToLinear.comp (unitaryToLin.comp higgsRepUnitary)
lemma higgsRepUnitary_mul (g : GaugeGroup) (φ : HiggsVec) :
(higgsRepUnitary g).1 *ᵥ φ = g.2.2 ^ 3 • (g.2.1.1 *ᵥ φ) := by
simp [higgsRepUnitary_apply_coe, smul_mulVec_assoc]
lemma rep_apply (g : GaugeGroup) (φ : HiggsVec) : rep g φ = g.2.2 ^ 3 • (g.2.1.1 *ᵥ φ) :=
higgsRepUnitary_mul g φ
lemma norm_invariant (g : GaugeGroup) (φ : HiggsVec) : ‖rep g φ‖ = ‖φ‖ :=
ContinuousLinearMap.norm_map_of_mem_unitary (unitaryToLin (higgsRepUnitary g)).2 φ
section potentialDefn
variable (μSq lambda : ℝ)
local notation "λ" => lambda
/-- The higgs potential for `higgsVec`, i.e. for constant higgs fields. -/
def potential (φ : HiggsVec) : ℝ := - μSq * ‖φ‖ ^ 2 + λ * ‖φ‖ ^ 4
lemma potential_invariant (φ : HiggsVec) (g : GaugeGroup) :
potential μSq (λ) (rep g φ) = potential μSq (λ) φ := by
simp only [potential, neg_mul, norm_invariant]
lemma potential_as_quad (φ : HiggsVec) :
λ * ‖φ‖ ^ 2 * ‖φ‖ ^ 2 + (- μSq ) * ‖φ‖ ^ 2 + (- potential μSq (λ) φ) = 0 := by
simp [potential]; ring
end potentialDefn
section potentialProp
variable {lambda : ℝ}
variable (μSq : ℝ)
variable (hLam : 0 < lambda)
local notation "λ" => lambda
lemma potential_snd_term_nonneg (φ : HiggsVec) :
0 ≤ λ * ‖φ‖ ^ 4 := by
rw [mul_nonneg_iff]
apply Or.inl
simp_all only [ge_iff_le, norm_nonneg, pow_nonneg, and_true]
exact le_of_lt hLam
lemma zero_le_potential_discrim (φ : HiggsVec) :
0 ≤ discrim (λ) (- μSq ) (- potential μSq (λ) φ) := by
have h1 := potential_as_quad μSq (λ) φ
rw [quadratic_eq_zero_iff_discrim_eq_sq] at h1
· simp only [h1, ne_eq, div_eq_zero_iff, OfNat.ofNat_ne_zero, or_false]
exact sq_nonneg (2 * lambda * ‖φ‖ ^ 2 + -μSq)
· exact ne_of_gt hLam
lemma potential_eq_zero_sol (φ : HiggsVec)
(hV : potential μSq (λ) φ = 0) : φ = 0 ∨ ‖φ‖ ^ 2 = μSq / λ := by
have h1 := potential_as_quad μSq (λ) φ
rw [hV] at h1
have h2 : ‖φ‖ ^ 2 * (lambda * ‖φ‖ ^ 2 + -μSq ) = 0 := by
linear_combination h1
simp at h2
cases' h2 with h2 h2
simp_all
apply Or.inr
field_simp at h2 ⊢
ring_nf
linear_combination h2
lemma potential_eq_zero_sol_of_μSq_nonpos (hμSq : μSq ≤ 0)
(φ : HiggsVec) (hV : potential μSq (λ) φ = 0) : φ = 0 := by
cases' (potential_eq_zero_sol μSq hLam φ hV) with h1 h1
exact h1
by_cases hμSqZ : μSq = 0
simpa [hμSqZ] using h1
refine ((?_ : ¬ 0 ≤ μSq / λ) (?_)).elim
· simp_all [div_nonneg_iff]
intro h
exact lt_imp_lt_of_le_imp_le (fun _ => h) (lt_of_le_of_ne hμSq hμSqZ)
· rw [← h1]
exact sq_nonneg ‖φ‖
lemma potential_bounded_below (φ : HiggsVec) :
- μSq ^ 2 / (4 * (λ)) ≤ potential μSq (λ) φ := by
have h1 := zero_le_potential_discrim μSq hLam φ
simp [discrim] at h1
ring_nf at h1
rw [← neg_le_iff_add_nonneg'] at h1
have h3 : (λ) * potential μSq (λ) φ * 4 = (4 * λ) * potential μSq (λ) φ := by
ring
rw [h3] at h1
have h2 := (div_le_iff' (by simp [hLam] : 0 < 4 * λ )).mpr h1
ring_nf at h2 ⊢
exact h2
lemma potential_bounded_below_of_μSq_nonpos {μSq : ℝ}
(hμSq : μSq ≤ 0) (φ : HiggsVec) : 0 ≤ potential μSq (λ) φ := by
refine add_nonneg ?_ (potential_snd_term_nonneg hLam φ)
field_simp [mul_nonpos_iff]
simp_all [ge_iff_le, norm_nonneg, pow_nonneg, and_self, or_true]
lemma potential_eq_bound_discrim_zero (φ : HiggsVec)
(hV : potential μSq (λ) φ = - μSq ^ 2 / (4 * λ)) :
discrim (λ) (- μSq) (- potential μSq (λ) φ) = 0 := by
field_simp [discrim, hV]
lemma potential_eq_bound_higgsVec_sq (φ : HiggsVec)
(hV : potential μSq (λ) φ = - μSq ^ 2 / (4 * (λ))) :
‖φ‖ ^ 2 = μSq / (2 * λ) := by
have h1 := potential_as_quad μSq (λ) φ
rw [quadratic_eq_zero_iff_of_discrim_eq_zero _
(potential_eq_bound_discrim_zero μSq hLam φ hV)] at h1
simp_rw [h1, neg_neg]
exact ne_of_gt hLam
lemma potential_eq_bound_iff (φ : HiggsVec) :
potential μSq (λ) φ = - μSq ^ 2 / (4 * (λ)) ↔ ‖φ‖ ^ 2 = μSq / (2 * (λ)) :=
Iff.intro (potential_eq_bound_higgsVec_sq μSq hLam φ)
(fun h ↦ by
have hv : ‖φ‖ ^ 4 = ‖φ‖ ^ 2 * ‖φ‖ ^ 2 := by ring_nf
field_simp [potential, hv, h]
ring_nf)
lemma potential_eq_bound_iff_of_μSq_nonpos {μSq : ℝ}
(hμSq : μSq ≤ 0) (φ : HiggsVec) : potential μSq (λ) φ = 0 ↔ φ = 0 :=
Iff.intro (fun h ↦ potential_eq_zero_sol_of_μSq_nonpos μSq hLam hμSq φ h)
(fun h ↦ by simp [potential, h])
lemma potential_eq_bound_IsMinOn (φ : HiggsVec)
(hv : potential μSq lambda φ = - μSq ^ 2 / (4 * lambda)) :
IsMinOn (potential μSq lambda) Set.univ φ := by
rw [isMinOn_univ_iff, hv]
exact fun x ↦ potential_bounded_below μSq hLam x
lemma potential_eq_bound_IsMinOn_of_μSq_nonpos {μSq : ℝ}
(hμSq : μSq ≤ 0) (φ : HiggsVec) (hv : potential μSq lambda φ = 0) :
IsMinOn (potential μSq lambda) Set.univ φ := by
rw [isMinOn_univ_iff, hv]
exact fun x ↦ potential_bounded_below_of_μSq_nonpos hLam hμSq x
lemma potential_bound_reached_of_μSq_nonneg {μSq : ℝ} (hμSq : 0 ≤ μSq) :
∃ (φ : HiggsVec), potential μSq lambda φ = - μSq ^ 2 / (4 * lambda) := by
use ![√(μSq/(2 * lambda)), 0]
refine (potential_eq_bound_iff μSq hLam _).mpr ?_
simp [PiLp.norm_sq_eq_of_L2]
field_simp [mul_pow]
lemma IsMinOn_potential_iff_of_μSq_nonneg {μSq : ℝ} (hμSq : 0 ≤ μSq) :
IsMinOn (potential μSq lambda) Set.univ φ ↔ ‖φ‖ ^ 2 = μSq /(2 * lambda) := by
apply Iff.intro <;> rw [← potential_eq_bound_iff μSq hLam φ]
· intro h
obtain ⟨φm, hφ⟩ := potential_bound_reached_of_μSq_nonneg hLam hμSq
have hm := isMinOn_univ_iff.mp h φm
rw [hφ] at hm
exact (Real.partialOrder.le_antisymm _ _ (potential_bounded_below μSq hLam φ) hm).symm
· exact potential_eq_bound_IsMinOn μSq hLam φ
lemma IsMinOn_potential_iff_of_μSq_nonpos {μSq : ℝ} (hμSq : μSq ≤ 0) :
IsMinOn (potential μSq lambda) Set.univ φ ↔ φ = 0 := by
apply Iff.intro <;> rw [← potential_eq_bound_iff_of_μSq_nonpos hLam hμSq φ]
· intro h
have h0 := isMinOn_univ_iff.mp h 0
have h1 := potential_bounded_below_of_μSq_nonpos hLam hμSq φ
rw [(potential_eq_bound_iff_of_μSq_nonpos hLam hμSq 0).mpr (by rfl)] at h0
exact (Real.partialOrder.le_antisymm _ _ h1 h0).symm
· exact potential_eq_bound_IsMinOn_of_μSq_nonpos hLam hμSq φ
end potentialProp
/-- Given a Higgs vector, a rotation matrix which puts the first component of the
vector to zero, and the second component to a real -/
def rotateMatrix (φ : HiggsVec) : Matrix (Fin 2) (Fin 2) ℂ :=
![![φ 1 /‖φ‖ , - φ 0 /‖φ‖], ![conj (φ 0) / ‖φ‖ , conj (φ 1) / ‖φ‖] ]
lemma rotateMatrix_star (φ : HiggsVec) :
star φ.rotateMatrix =
![![conj (φ 1) /‖φ‖ , φ 0 /‖φ‖], ![- conj (φ 0) / ‖φ‖ , φ 1 / ‖φ‖] ] := by
simp_rw [star, rotateMatrix, conjTranspose]
ext i j
fin_cases i <;> fin_cases j <;> simp [conj_ofReal]
lemma rotateMatrix_det {φ : HiggsVec} (hφ : φ ≠ 0) : (rotateMatrix φ).det = 1 := by
have h1 : (‖φ‖ : ℂ) ≠ 0 := ofReal_inj.mp.mt (norm_ne_zero_iff.mpr hφ)
field_simp [rotateMatrix, det_fin_two]
rw [← ofReal_mul, ← sq, ← @real_inner_self_eq_norm_sq]
simp [PiLp.inner_apply, Complex.inner, neg_mul, sub_neg_eq_add,
Fin.sum_univ_two, ofReal_add, ofReal_mul, mul_conj, mul_comm, add_comm]
lemma rotateMatrix_unitary {φ : HiggsVec} (hφ : φ ≠ 0) :
(rotateMatrix φ) ∈ unitaryGroup (Fin 2) ℂ := by
rw [mem_unitaryGroup_iff', rotateMatrix_star, rotateMatrix]
erw [mul_fin_two, one_fin_two]
have : (‖φ‖ : ℂ) ≠ 0 := ofReal_inj.mp.mt (norm_ne_zero_iff.mpr hφ)
ext i j
fin_cases i <;> fin_cases j <;> field_simp
<;> rw [← ofReal_mul, ← sq, ← @real_inner_self_eq_norm_sq]
· simp [PiLp.inner_apply, Complex.inner, neg_mul, sub_neg_eq_add,
Fin.sum_univ_two, ofReal_add, ofReal_mul, mul_conj, mul_comm, add_comm]
· ring_nf
· ring_nf
· simp [PiLp.inner_apply, Complex.inner, neg_mul, sub_neg_eq_add,
Fin.sum_univ_two, ofReal_add, ofReal_mul, mul_conj, mul_comm]
lemma rotateMatrix_specialUnitary {φ : HiggsVec} (hφ : φ ≠ 0) :
(rotateMatrix φ) ∈ specialUnitaryGroup (Fin 2) ℂ :=
mem_specialUnitaryGroup_iff.mpr ⟨rotateMatrix_unitary hφ, rotateMatrix_det hφ⟩
/-- Given a Higgs vector, an element of the gauge group which puts the first component of the
vector to zero, and the second component to a real -/
def rotateGuageGroup {φ : HiggsVec} (hφ : φ ≠ 0) : GaugeGroup :=
⟨1, ⟨(rotateMatrix φ), rotateMatrix_specialUnitary hφ⟩, 1⟩
lemma rotateGuageGroup_apply {φ : HiggsVec} (hφ : φ ≠ 0) :
rep (rotateGuageGroup hφ) φ = ![0, ofReal ‖φ‖] := by
rw [rep_apply]
simp only [rotateGuageGroup, rotateMatrix, one_pow, one_smul,
Nat.succ_eq_add_one, Nat.reduceAdd, ofReal_eq_coe]
ext i
fin_cases i
· simp only [mulVec, Fin.zero_eta, Fin.isValue, cons_val', empty_val', cons_val_fin_one,
cons_val_zero, cons_dotProduct, vecHead, vecTail, Nat.succ_eq_add_one, Nat.reduceAdd,
Function.comp_apply, Fin.succ_zero_eq_one, dotProduct_empty, add_zero]
ring_nf
· simp only [Fin.mk_one, Fin.isValue, cons_val_one, head_cons, mulVec, Fin.isValue,
cons_val', empty_val', cons_val_fin_one, vecHead, cons_dotProduct, vecTail, Nat.succ_eq_add_one,
Nat.reduceAdd, Function.comp_apply, Fin.succ_zero_eq_one, dotProduct_empty, add_zero]
have : (‖φ‖ : ℂ) ≠ 0 := ofReal_inj.mp.mt (norm_ne_zero_iff.mpr hφ)
field_simp
rw [← ofReal_mul, ← sq, ← @real_inner_self_eq_norm_sq]
simp [PiLp.inner_apply, Complex.inner, neg_mul, sub_neg_eq_add,
Fin.sum_univ_two, ofReal_add, ofReal_mul, mul_conj, mul_comm]
theorem rotate_fst_zero_snd_real (φ : HiggsVec) :
∃ (g : GaugeGroup), rep g φ = ![0, ofReal ‖φ‖] := by
by_cases h : φ = 0
· use ⟨1, 1, 1⟩
simp [h]
ext i
fin_cases i <;> rfl
· use rotateGuageGroup h
exact rotateGuageGroup_apply h
end HiggsVec
end
end StandardModel

1
HepLean/StandardModel/Representations.lean
View file

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

13
README.md
View file

@ -3,6 +3,7 @@
[![](https://img.shields.io/badge/Read_The-Docs-green)](https://heplean.github.io/HepLean/)
[![](https://img.shields.io/badge/PRs-Welcome-green)](https://github.com/HEPLean/HepLean/pulls)
[![](https://img.shields.io/badge/Lean-Zulip-green)](https://leanprover.zulipchat.com)
[![](https://img.shields.io/badge/TODO-List-green)](https://heplean.github.io/HepLean/TODOList)
[![](https://img.shields.io/badge/Lean-v4.9.0-blue)](https://github.com/leanprover/lean4/releases/tag/v4.9.0)
A project to digitalize high energy physics.
@ -17,12 +18,12 @@ A project to digitalize high energy physics.
## Areas of high energy physics with some coverage in HepLean
[![](https://img.shields.io/badge/The_CKM_Matrix-blue)](https://heplean.github.io/HepLean/HepLean/FlavorPhysics/CKMMatrix/Basic.html)
[![](https://img.shields.io/badge/Higgs_Field-blue)](https://heplean.github.io/HepLean/HepLean/StandardModel/HiggsBoson/Basic.html)
[![](https://img.shields.io/badge/2HDM-blue)](https://heplean.github.io/HepLean/HepLean/BeyondTheStandardModel/TwoHDM/Basic.html)
[![](https://img.shields.io/badge/Lorentz_Group-blue)](https://heplean.github.io/HepLean/HepLean/SpaceTime/LorentzGroup/Basic.html)
[![](https://img.shields.io/badge/Anomaly_Cancellation-blue)](https://heplean.github.io/HepLean/HepLean/AnomalyCancellation/Basic.html)
[![](https://img.shields.io/badge/Feynman_diagrams-blue)](https://heplean.github.io/HepLean/HepLean/FeynmanDiagrams/PhiFour/Basic.html)
[![](https://img.shields.io/badge/The_CKM_Matrix-blue)](https://heplean.github.io/HepLean/docs/HepLean/FlavorPhysics/CKMMatrix/Basic.html)
[![](https://img.shields.io/badge/Higgs_Field-blue)](https://heplean.github.io/HepLean/docs/HepLean/StandardModel/HiggsBoson/Basic.html)
[![](https://img.shields.io/badge/2HDM-blue)](https://heplean.github.io/HepLean/docs/HepLean/BeyondTheStandardModel/TwoHDM/Basic.html)
[![](https://img.shields.io/badge/Lorentz_Group-blue)](https://heplean.github.io/HepLean/docs/HepLean/SpaceTime/LorentzGroup/Basic.html)
[![](https://img.shields.io/badge/Anomaly_Cancellation-blue)](https://heplean.github.io/HepLean/docs/HepLean/AnomalyCancellation/Basic.html)
[![](https://img.shields.io/badge/Feynman_diagrams-blue)](https://heplean.github.io/HepLean/docs/HepLean/FeynmanDiagrams/PhiFour/Basic.html)
## Where to learn more
- Read the associated paper:

2
docs/_layouts/default.html
View file

@ -2,6 +2,7 @@
<html lang="{{ site.lang | default: "en-US" }}">
<head>
<meta charset="UTF-8">
<meta name="google-site-verification" content="Ki8LwioLnvbMPpP_U5Sjw6eTN71GoLqAF0UzevmNoJY" />
{% seo %}
<link rel="preconnect" href="https://fonts.gstatic.com">
@ -26,6 +27,7 @@
<a href="{{ site.github.zip_url }}" class="btn">Download .zip</a>
<a href="{{ site.github.tar_url }}" class="btn">Download .tar.gz</a>
{% endif %}
<a href="https://heplean.github.io/HepLean/TODOList" class="btn">TODO List</a>
</header>
<main id="content" class="main-content" role="main">

12
docs/references.bib
View file

@ -34,6 +34,18 @@
year = "2020"
}
@Article{ ParticleDataGroup:2018ovx,
author = "Tanabashi, M. and others",
collaboration = "Particle Data Group",
title = "{Review of Particle Physics}",
doi = "10.1103/PhysRevD.98.030001",
journal = "Phys. Rev. D",
volume = "98",
number = "3",
pages = "030001",
year = "2018"
}
@Article{ raynor2021graphical,
title = {Graphical combinatorics and a distributive law for modular
operads},

8
lakefile.toml
View file

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

58
scripts/README.md Normal file
View file

@ -0,0 +1,58 @@
# Scripts associated with HepLean
## lint-style.py and lint-style.sh
Taken from Mathlib's linters. These perform text-based linting of the code.
These are to be slowly replaced with code written in Lean.
## double_line_lint
Checks for double empty lines in HepLean.
Passing this linter is currently not required to pass CI on github.
Run using
```
lake exe double_line_lint
```
## check_file_imports.lean
Checks all files are correctly imported into `HepLean.lean`.
Run using
```
lake exe check_file_imports
```
## type_former_lint.lean
Checks whether the name of definitions which form a type or prop starts with a capital letter.
Run using
```
lake exe type_former_lint
```
## lint-all.sh
Performs all linting checks on HepLean.
Run using
```
./scripts/lint-all.sh
```
## Other useful commands
- To build HepLean use
```
lake exe cache get
lake build
```
- To update HepLean's dependencies use
```
lake update
```

6
scripts/build.sh
View file

@ -1,6 +0,0 @@
#!/usr/bin/env bash
lake exe cache get
lake build

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

98
scripts/find_TODOs.lean Normal file
View file

@ -0,0 +1,98 @@
/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license.
Authors: Joseph Tooby-Smith
-/
import Lean
import Batteries.Data.String.Matcher
import Mathlib.Init.Data.Nat.Notation
/-!
# TODO finder
This program finds all instances of `/<!> TODO: ...` (without the `<>`) in HepLean 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 HepLeanTODOItem : Type := Array String → Array (String × ℕ)
/-- Checks if a . -/
def TODOFinder : HepLeanTODOItem := fun lines ↦ Id.run do
let enumLines := (lines.toList.enumFrom 1)
let todos := enumLines.filterMap (fun (lno1, l1) ↦
if l1.startsWith "/-! TODO:" then
some ((l1.replace "/-! TODO: " "").replace "-/" "", lno1)
else none)
todos.toArray
structure TODOContext where
/-- The underlying `message`. -/
statement : String
/-- The line number -/
lineNumber : ℕ
/-- The file path -/
path : FilePath
def printTODO (todos : Array TODOContext) : IO Unit := do
for e in todos do
IO.println (s!"{e.path}:{e.lineNumber}: {e.statement}")
def filePathToGitPath (S : FilePath) (n : ℕ) : String :=
"https://github.com/HEPLean/HepLean/blob/master/"++
(S.toString.replace "." "/").replace "/lean" ".lean"
++ "#L" ++ toString n
def docTODO (todos : Array TODOContext) : IO String := do
let mut out := ""
for e in todos do
out := out ++ (s!" - [{e.statement}]("++ filePathToGitPath e.path e.lineNumber ++ ")\n")
return out
def hepLeanLintFile (path : FilePath) : IO String := do
let lines ← IO.FS.lines path
let allOutput := (Array.map (fun lint ↦
(Array.map (fun (e, n) ↦ TODOContext.mk e n path)) (lint lines)))
#[TODOFinder]
let errors := allOutput.flatten
printTODO errors
docTODO errors
def todoFileHeader : String := s!"
# TODO List
This is an automatically generated list of TODOs appearing as `/-! TODO:...` in HepLean.
Please feel free to contribute to the completion of these tasks.
"
def main (args : 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 out : String := ""
for imp in hepLeanMod.imports do
if imp.module == `Init then continue
let filePath := (mkFilePath (imp.module.toString.split (· == '.'))).addExtension "lean"
let l ← hepLeanLintFile filePath
if l != "" then
out := out ++ "\n### " ++ imp.module.toString ++ "\n"
out := out ++ l
let fileOut : System.FilePath := {toString := "./docs/TODOList.md"}
/- Below here is concerned with writing out to the docs. -/
if "mkFile" ∈ args then
IO.println (s!"TODOList file made.")
IO.FS.writeFile fileOut (todoFileHeader ++ out)
return 0

4
scripts/update-lean-mathlib.sh
View file

@ -1,4 +0,0 @@
#!/usr/bin/env bash
lake update