diff --git a/.DS_Store b/.DS_Store
deleted file mode 100644
index 23f4574..0000000
Binary files a/.DS_Store and /dev/null differ
diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
index 2d58d3e..08b43fb 100644
--- a/.github/workflows/docs.yml
+++ b/.github/workflows/docs.yml
@@ -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: |
diff --git a/.gitignore b/.gitignore
index d701102..acf3987 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,4 +1,5 @@
/build
/lake-packages/*
.lake/packages/*
-.lake/build
\ No newline at end of file
+.lake/build
+.DS_Store
diff --git a/HepLean.lean b/HepLean.lean
index cca5867..5099331 100644
--- a/HepLean.lean
+++ b/HepLean.lean
@@ -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
diff --git a/HepLean/AnomalyCancellation/Basic.lean b/HepLean/AnomalyCancellation/Basic.lean
index c44b98f..1a298cf 100644
--- a/HepLean/AnomalyCancellation/Basic.lean
+++ b/HepLean/AnomalyCancellation/Basic.lean
@@ -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
diff --git a/HepLean/AnomalyCancellation/MSSMNu/Basic.lean b/HepLean/AnomalyCancellation/MSSMNu/Basic.lean
index cbf418d..58632ea 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/Basic.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/Basic.lean
@@ -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,
diff --git a/HepLean/AnomalyCancellation/MSSMNu/HyperCharge.lean b/HepLean/AnomalyCancellation/MSSMNu/HyperCharge.lean
index 64c6f32..00cd77d 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/HyperCharge.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/HyperCharge.lean
@@ -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
diff --git a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/Basic.lean b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/Basic.lean
index 7442533..721e6e6 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/Basic.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/Basic.lean
@@ -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
diff --git a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean
index a871c11..9832ed2 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/PlaneWithY3B3.lean
@@ -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
diff --git a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
index 9958263..659f847 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
@@ -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
diff --git a/HepLean/AnomalyCancellation/PureU1/Basic.lean b/HepLean/AnomalyCancellation/PureU1/Basic.lean
index bca8160..b5ab703 100644
--- a/HepLean/AnomalyCancellation/PureU1/Basic.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Basic.lean
@@ -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
diff --git a/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean
index f9bbcc4..746e2d6 100644
--- a/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean
+++ b/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean
@@ -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
diff --git a/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean b/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean
index a5e4004..3189e4c 100644
--- a/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean
+++ b/HepLean/AnomalyCancellation/PureU1/ConstAbs.lean
@@ -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)
diff --git a/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
index 994c01c..cdbf343 100644
--- a/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
@@ -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)
diff --git a/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean b/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean
index aa58459..db11575 100644
--- a/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean
@@ -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)) :
diff --git a/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean b/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean
index 97f0209..4cfb260 100644
--- a/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean
+++ b/HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean
@@ -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
diff --git a/HepLean/AnomalyCancellation/PureU1/LowDim/Three.lean b/HepLean/AnomalyCancellation/PureU1/LowDim/Three.lean
index 15552a3..be0d389 100644
--- a/HepLean/AnomalyCancellation/PureU1/LowDim/Three.lean
+++ b/HepLean/AnomalyCancellation/PureU1/LowDim/Three.lean
@@ -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
diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
index c6132d0..5af2a8e 100644
--- a/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
@@ -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
diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean b/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
index 477c597..3cc030f 100644
--- a/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
@@ -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) ,
diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean b/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean
index 1ded1c6..56ddddd 100644
--- a/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean
@@ -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
diff --git a/HepLean/AnomalyCancellation/PureU1/Permutations.lean b/HepLean/AnomalyCancellation/PureU1/Permutations.lean
index 084e2ce..b20fb59 100644
--- a/HepLean/AnomalyCancellation/PureU1/Permutations.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Permutations.lean
@@ -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
diff --git a/HepLean/AnomalyCancellation/PureU1/Sort.lean b/HepLean/AnomalyCancellation/PureU1/Sort.lean
index 3438d32..eccf84b 100644
--- a/HepLean/AnomalyCancellation/PureU1/Sort.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Sort.lean
@@ -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
diff --git a/HepLean/AnomalyCancellation/PureU1/VectorLike.lean b/HepLean/AnomalyCancellation/PureU1/VectorLike.lean
index 29d6daa..d0d9ce0 100644
--- a/HepLean/AnomalyCancellation/PureU1/VectorLike.lean
+++ b/HepLean/AnomalyCancellation/PureU1/VectorLike.lean
@@ -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
diff --git a/HepLean/AnomalyCancellation/SM/Basic.lean b/HepLean/AnomalyCancellation/SM/Basic.lean
index 81f6804..f067f5e 100644
--- a/HepLean/AnomalyCancellation/SM/Basic.lean
+++ b/HepLean/AnomalyCancellation/SM/Basic.lean
@@ -319,5 +319,4 @@ lemma accCube_ext {S T : (SMCharges n).Charges}
rfl
repeat rw [h1]
-
end SMACCs
diff --git a/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean b/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean
index a14233f..c8d46eb 100644
--- a/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean
+++ b/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean
@@ -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
diff --git a/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean b/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
index 43ddbd0..126bf37 100644
--- a/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
+++ b/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
@@ -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
diff --git a/HepLean/AnomalyCancellation/SM/Permutations.lean b/HepLean/AnomalyCancellation/SM/Permutations.lean
index 5c6af44..0dda836 100644
--- a/HepLean/AnomalyCancellation/SM/Permutations.lean
+++ b/HepLean/AnomalyCancellation/SM/Permutations.lean
@@ -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
diff --git a/HepLean/AnomalyCancellation/SMNu/Basic.lean b/HepLean/AnomalyCancellation/SMNu/Basic.lean
index e4874a1..625adf9 100644
--- a/HepLean/AnomalyCancellation/SMNu/Basic.lean
+++ b/HepLean/AnomalyCancellation/SMNu/Basic.lean
@@ -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
diff --git a/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean b/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean
index cd4f051..801ae0d 100644
--- a/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean
+++ b/HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean
@@ -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 :=
diff --git a/HepLean/AnomalyCancellation/SMNu/NoGrav/Basic.lean b/HepLean/AnomalyCancellation/SMNu/NoGrav/Basic.lean
index 54a9737..4f854b2 100644
--- a/HepLean/AnomalyCancellation/SMNu/NoGrav/Basic.lean
+++ b/HepLean/AnomalyCancellation/SMNu/NoGrav/Basic.lean
@@ -110,7 +110,6 @@ def perm (n : ℕ) : ACCSystemGroupAction (SMNoGrav n) where
exact Fin.elim0 i
cubicInvariant := accCube_invariant
-
end SMNoGrav
end SMRHN
diff --git a/HepLean/AnomalyCancellation/SMNu/Ordinary/Basic.lean b/HepLean/AnomalyCancellation/SMNu/Ordinary/Basic.lean
index e27eda9..df41764 100644
--- a/HepLean/AnomalyCancellation/SMNu/Ordinary/Basic.lean
+++ b/HepLean/AnomalyCancellation/SMNu/Ordinary/Basic.lean
@@ -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
diff --git a/HepLean/AnomalyCancellation/SMNu/Ordinary/DimSevenPlane.lean b/HepLean/AnomalyCancellation/SMNu/Ordinary/DimSevenPlane.lean
index 04d8315..a8201a3 100644
--- a/HepLean/AnomalyCancellation/SMNu/Ordinary/DimSevenPlane.lean
+++ b/HepLean/AnomalyCancellation/SMNu/Ordinary/DimSevenPlane.lean
@@ -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
diff --git a/HepLean/AnomalyCancellation/SMNu/Permutations.lean b/HepLean/AnomalyCancellation/SMNu/Permutations.lean
index 4306f2a..3a1cb19 100644
--- a/HepLean/AnomalyCancellation/SMNu/Permutations.lean
+++ b/HepLean/AnomalyCancellation/SMNu/Permutations.lean
@@ -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
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean
index 91a2fa4..6e08870 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean
@@ -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
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/Basic.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/Basic.lean
index 250a365..5da3f0e 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/Basic.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/Basic.lean
@@ -37,7 +37,6 @@ def PlusU1 (n : ℕ) : ACCSystem where
namespace PlusU1
-
variable {n : ℕ}
lemma gravSol (S : (PlusU1 n).LinSols) : accGrav S.val = 0 := by
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean
index be6b935..ac6aaa0 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean
@@ -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
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean
index fd84c9b..afb8aa9 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean
@@ -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
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean
index a1d54f8..54c3860 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean
@@ -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
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSol.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSol.lean
index 912464c..e4965c1 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSol.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSol.lean
@@ -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)
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean
index da6f205..7488e75 100644
--- a/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean
@@ -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. -/
diff --git a/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean b/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean
index c6429d7..f395d71 100644
--- a/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean
+++ b/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean
@@ -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
diff --git a/HepLean/FeynmanDiagrams/Basic.lean b/HepLean/FeynmanDiagrams/Basic.lean
index 33fa443..9c41239 100644
--- a/HepLean/FeynmanDiagrams/Basic.lean
+++ b/HepLean/FeynmanDiagrams/Basic.lean
@@ -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
diff --git a/HepLean/FeynmanDiagrams/Instances/ComplexScalar.lean b/HepLean/FeynmanDiagrams/Instances/ComplexScalar.lean
index 6b77219..6c081c2 100644
--- a/HepLean/FeynmanDiagrams/Instances/ComplexScalar.lean
+++ b/HepLean/FeynmanDiagrams/Instances/ComplexScalar.lean
@@ -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
diff --git a/HepLean/FeynmanDiagrams/Instances/Phi4.lean b/HepLean/FeynmanDiagrams/Instances/Phi4.lean
index 06413ec..0c780ad 100644
--- a/HepLean/FeynmanDiagrams/Instances/Phi4.lean
+++ b/HepLean/FeynmanDiagrams/Instances/Phi4.lean
@@ -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
diff --git a/HepLean/FeynmanDiagrams/Momentum.lean b/HepLean/FeynmanDiagrams/Momentum.lean
index 65cb033..51c58b0 100644
--- a/HepLean/FeynmanDiagrams/Momentum.lean
+++ b/HepLean/FeynmanDiagrams/Momentum.lean
@@ -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
diff --git a/HepLean/FlavorPhysics/CKMMatrix/Basic.lean b/HepLean/FlavorPhysics/CKMMatrix/Basic.lean
index 7e6922c..ddcf854 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/Basic.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/Basic.lean
@@ -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
diff --git a/HepLean/FlavorPhysics/CKMMatrix/Invariants.lean b/HepLean/FlavorPhysics/CKMMatrix/Invariants.lean
index 79a7e70..9b9b024 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/Invariants.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/Invariants.lean
@@ -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
diff --git a/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean b/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean
index 974f81d..29c9bbf 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean
@@ -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
diff --git a/HepLean/FlavorPhysics/CKMMatrix/Relations.lean b/HepLean/FlavorPhysics/CKMMatrix/Relations.lean
index 2dad76b..bbf9dff 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/Relations.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/Relations.lean
@@ -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
diff --git a/HepLean/FlavorPhysics/CKMMatrix/Rows.lean b/HepLean/FlavorPhysics/CKMMatrix/Rows.lean
index e8d7f5b..39e7c15 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/Rows.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/Rows.lean
@@ -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]
diff --git a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean
index 42ab86b..3beb917 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/Basic.lean
@@ -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
diff --git a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean
index 60ce478..ef7c1d3 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean
@@ -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
diff --git a/HepLean/Mathematics/LinearMaps.lean b/HepLean/Mathematics/LinearMaps.lean
index 5fda3b0..d6dbf02 100644
--- a/HepLean/Mathematics/LinearMaps.lean
+++ b/HepLean/Mathematics/LinearMaps.lean
@@ -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]
diff --git a/HepLean/Mathematics/SO3/Basic.lean b/HepLean/Mathematics/SO3/Basic.lean
index ff34705..e31b657 100644
--- a/HepLean/Mathematics/SO3/Basic.lean
+++ b/HepLean/Mathematics/SO3/Basic.lean
@@ -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
diff --git a/HepLean/SpaceTime/Basic.lean b/HepLean/SpaceTime/Basic.lean
index fae801a..9e78437 100644
--- a/HepLean/SpaceTime/Basic.lean
+++ b/HepLean/SpaceTime/Basic.lean
@@ -29,7 +29,6 @@ instance euclideanNormedAddCommGroup : NormedAddCommGroup SpaceTime := Pi.normed
instance euclideanNormedSpace : NormedSpace ℝ SpaceTime := Pi.normedSpace
-
namespace SpaceTime
open Manifold
diff --git a/HepLean/SpaceTime/CliffordAlgebra.lean b/HepLean/SpaceTime/CliffordAlgebra.lean
index 99fec60..94ce6f7 100644
--- a/HepLean/SpaceTime/CliffordAlgebra.lean
+++ b/HepLean/SpaceTime/CliffordAlgebra.lean
@@ -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
diff --git a/HepLean/SpaceTime/LorentzAlgebra/Basic.lean b/HepLean/SpaceTime/LorentzAlgebra/Basic.lean
index 8f14a5d..c585a52 100644
--- a/HepLean/SpaceTime/LorentzAlgebra/Basic.lean
+++ b/HepLean/SpaceTime/LorentzAlgebra/Basic.lean
@@ -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
diff --git a/HepLean/SpaceTime/LorentzAlgebra/Basis.lean b/HepLean/SpaceTime/LorentzAlgebra/Basis.lean
index 45f9f44..36ae0f9 100644
--- a/HepLean/SpaceTime/LorentzAlgebra/Basis.lean
+++ b/HepLean/SpaceTime/LorentzAlgebra/Basis.lean
@@ -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. -/
diff --git a/HepLean/SpaceTime/LorentzGroup/Basic.lean b/HepLean/SpaceTime/LorentzGroup/Basic.lean
index 5c737b5..e47cb6a 100644
--- a/HepLean/SpaceTime/LorentzGroup/Basic.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Basic.lean
@@ -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
diff --git a/HepLean/SpaceTime/LorentzGroup/Boosts.lean b/HepLean/SpaceTime/LorentzGroup/Boosts.lean
index 38e46e6..a79f0db 100644
--- a/HepLean/SpaceTime/LorentzGroup/Boosts.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Boosts.lean
@@ -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
diff --git a/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean b/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean
index ea7c655..be1963c 100644
--- a/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Orthochronous.lean
@@ -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)⟩
diff --git a/HepLean/SpaceTime/LorentzGroup/Proper.lean b/HepLean/SpaceTime/LorentzGroup/Proper.lean
index 2457446..e7bc25d 100644
--- a/HepLean/SpaceTime/LorentzGroup/Proper.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Proper.lean
@@ -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
diff --git a/HepLean/SpaceTime/LorentzGroup/Rotations.lean b/HepLean/SpaceTime/LorentzGroup/Rotations.lean
index 5172b3f..feee657 100644
--- a/HepLean/SpaceTime/LorentzGroup/Rotations.lean
+++ b/HepLean/SpaceTime/LorentzGroup/Rotations.lean
@@ -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
diff --git a/HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean b/HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean
index 6fbdcb5..eeb7385 100644
--- a/HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean
+++ b/HepLean/SpaceTime/LorentzVector/AsSelfAdjointMatrix.lean
@@ -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 :
diff --git a/HepLean/SpaceTime/LorentzVector/Basic.lean b/HepLean/SpaceTime/LorentzVector/Basic.lean
index c3d2a5a..060e348 100644
--- a/HepLean/SpaceTime/LorentzVector/Basic.lean
+++ b/HepLean/SpaceTime/LorentzVector/Basic.lean
@@ -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
diff --git a/HepLean/SpaceTime/LorentzVector/NormOne.lean b/HepLean/SpaceTime/LorentzVector/NormOne.lean
index 2866976..905e448 100644
--- a/HepLean/SpaceTime/LorentzVector/NormOne.lean
+++ b/HepLean/SpaceTime/LorentzVector/NormOne.lean
@@ -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
diff --git a/HepLean/SpaceTime/MinkowskiMetric.lean b/HepLean/SpaceTime/MinkowskiMetric.lean
index 884945e..5711fbf 100644
--- a/HepLean/SpaceTime/MinkowskiMetric.lean
+++ b/HepLean/SpaceTime/MinkowskiMetric.lean
@@ -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
diff --git a/HepLean/SpaceTime/SL2C/Basic.lean b/HepLean/SpaceTime/SL2C/Basic.lean
index d24152c..352fe81 100644
--- a/HepLean/SpaceTime/SL2C/Basic.lean
+++ b/HepLean/SpaceTime/SL2C/Basic.lean
@@ -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
diff --git a/HepLean/StandardModel/Basic.lean b/HepLean/StandardModel/Basic.lean
index 4f67a57..f145c99 100644
--- a/HepLean/StandardModel/Basic.lean
+++ b/HepLean/StandardModel/Basic.lean
@@ -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 ℂ
diff --git a/HepLean/StandardModel/HiggsBoson/Basic.lean b/HepLean/StandardModel/HiggsBoson/Basic.lean
index 62a19ec..6ec0721 100644
--- a/HepLean/StandardModel/HiggsBoson/Basic.lean
+++ b/HepLean/StandardModel/HiggsBoson/Basic.lean
@@ -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
diff --git a/HepLean/StandardModel/HiggsBoson/GaugeAction.lean b/HepLean/StandardModel/HiggsBoson/GaugeAction.lean
new file mode 100644
index 0000000..2abcd4c
--- /dev/null
+++ b/HepLean/StandardModel/HiggsBoson/GaugeAction.lean
@@ -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
diff --git a/HepLean/StandardModel/HiggsBoson/PointwiseInnerProd.lean b/HepLean/StandardModel/HiggsBoson/PointwiseInnerProd.lean
new file mode 100644
index 0000000..0f53792
--- /dev/null
+++ b/HepLean/StandardModel/HiggsBoson/PointwiseInnerProd.lean
@@ -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
diff --git a/HepLean/StandardModel/HiggsBoson/Potential.lean b/HepLean/StandardModel/HiggsBoson/Potential.lean
new file mode 100644
index 0000000..44d4ce7
--- /dev/null
+++ b/HepLean/StandardModel/HiggsBoson/Potential.lean
@@ -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
diff --git a/HepLean/StandardModel/HiggsBoson/TargetSpace.lean b/HepLean/StandardModel/HiggsBoson/TargetSpace.lean
deleted file mode 100644
index 350d2b5..0000000
--- a/HepLean/StandardModel/HiggsBoson/TargetSpace.lean
+++ /dev/null
@@ -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
diff --git a/HepLean/StandardModel/Representations.lean b/HepLean/StandardModel/Representations.lean
index 4500ee5..4fe843c 100644
--- a/HepLean/StandardModel/Representations.lean
+++ b/HepLean/StandardModel/Representations.lean
@@ -53,5 +53,4 @@ lemma repU1_fundamentalSU2_commute (u1 : unitary ℂ) (g : specialUnitaryGroup (
apply Subtype.ext
simp
-
end StandardModel
diff --git a/README.md b/README.md
index f2e2ca1..9225176 100644
--- a/README.md
+++ b/README.md
@@ -3,6 +3,7 @@
[](https://heplean.github.io/HepLean/)
[](https://github.com/HEPLean/HepLean/pulls)
[](https://leanprover.zulipchat.com)
+[](https://heplean.github.io/HepLean/TODOList)
[](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://heplean.github.io/HepLean/HepLean/FlavorPhysics/CKMMatrix/Basic.html)
-[](https://heplean.github.io/HepLean/HepLean/StandardModel/HiggsBoson/Basic.html)
-[](https://heplean.github.io/HepLean/HepLean/BeyondTheStandardModel/TwoHDM/Basic.html)
-[](https://heplean.github.io/HepLean/HepLean/SpaceTime/LorentzGroup/Basic.html)
-[](https://heplean.github.io/HepLean/HepLean/AnomalyCancellation/Basic.html)
-[](https://heplean.github.io/HepLean/HepLean/FeynmanDiagrams/PhiFour/Basic.html)
+[](https://heplean.github.io/HepLean/docs/HepLean/FlavorPhysics/CKMMatrix/Basic.html)
+[](https://heplean.github.io/HepLean/docs/HepLean/StandardModel/HiggsBoson/Basic.html)
+[](https://heplean.github.io/HepLean/docs/HepLean/BeyondTheStandardModel/TwoHDM/Basic.html)
+[](https://heplean.github.io/HepLean/docs/HepLean/SpaceTime/LorentzGroup/Basic.html)
+[](https://heplean.github.io/HepLean/docs/HepLean/AnomalyCancellation/Basic.html)
+[](https://heplean.github.io/HepLean/docs/HepLean/FeynmanDiagrams/PhiFour/Basic.html)
## Where to learn more
- Read the associated paper:
diff --git a/docs/_layouts/default.html b/docs/_layouts/default.html
index c2a5f25..36cfa29 100644
--- a/docs/_layouts/default.html
+++ b/docs/_layouts/default.html
@@ -2,6 +2,7 @@
+
{% seo %}
@@ -26,6 +27,7 @@
Download .zip
Download .tar.gz
{% endif %}
+ TODO List
diff --git a/docs/references.bib b/docs/references.bib
index 6022c68..44c329a 100644
--- a/docs/references.bib
+++ b/docs/references.bib
@@ -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},
diff --git a/lakefile.toml b/lakefile.toml
index f873798..bf4acda 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -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"
\ No newline at end of file
diff --git a/scripts/README.md b/scripts/README.md
new file mode 100644
index 0000000..2b6e300
--- /dev/null
+++ b/scripts/README.md
@@ -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
+```
\ No newline at end of file
diff --git a/scripts/build.sh b/scripts/build.sh
deleted file mode 100755
index 9312991..0000000
--- a/scripts/build.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-#!/usr/bin/env bash
-
-
-
-lake exe cache get
-lake build
\ No newline at end of file
diff --git a/scripts/double_line_lint.lean b/scripts/double_line_lint.lean
new file mode 100644
index 0000000..3b04875
--- /dev/null
+++ b/scripts/double_line_lint.lean
@@ -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
diff --git a/scripts/find_TODOs.lean b/scripts/find_TODOs.lean
new file mode 100644
index 0000000..3b73281
--- /dev/null
+++ b/scripts/find_TODOs.lean
@@ -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
diff --git a/scripts/update-lean-mathlib.sh b/scripts/update-lean-mathlib.sh
deleted file mode 100755
index 43fdc71..0000000
--- a/scripts/update-lean-mathlib.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-#!/usr/bin/env bash
-
-lake update
-