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

refactor: Lint

Browse source
This commit is contained in:
jstoobysmith 2024-04-19 10:08:56 -04:00
parent e710c9278e
commit 12a568b45f
5 changed files with 44 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

3
HepLean.lean
View file

@ -36,11 +36,14 @@ import HepLean.AnomalyCancellation.SMNu.Basic
import HepLean.AnomalyCancellation.SMNu.FamilyMaps
import HepLean.AnomalyCancellation.SMNu.NoGrav.Basic
import HepLean.AnomalyCancellation.SMNu.Ordinary.Basic
import HepLean.AnomalyCancellation.SMNu.Ordinary.DimSevenPlane
import HepLean.AnomalyCancellation.SMNu.Ordinary.FamilyMaps
import HepLean.AnomalyCancellation.SMNu.Permutations
import HepLean.AnomalyCancellation.SMNu.PlusU1.BMinusL
import HepLean.AnomalyCancellation.SMNu.PlusU1.Basic
import HepLean.AnomalyCancellation.SMNu.PlusU1.BoundPlaneDim
import HepLean.AnomalyCancellation.SMNu.PlusU1.FamilyMaps
import HepLean.AnomalyCancellation.SMNu.PlusU1.HyperCharge
import HepLean.AnomalyCancellation.SMNu.PlusU1.PlaneNonSols
import HepLean.AnomalyCancellation.SMNu.PlusU1.QuadSol
import HepLean.AnomalyCancellation.SMNu.PlusU1.QuadSolToSol

3
HepLean/AnomalyCancellation/LinearMaps.lean
View file

@ -149,7 +149,7 @@ lemma map_add₂ (f : BiLinearSymm V) (S : V) (T1 T2 : V) :
f (S, T1 + T2) = f (S, T1) + f (S, T2) := by
rw [f.swap, f.map_add₁, f.swap T1 S, f.swap T2 S]
/-- Fixing the second input vectors, the resulting linear map. -/
def toLinear₁ (f : BiLinearSymm V) (T : V) : V →ₗ[ℚ] ℚ where
toFun S := f (S, T)
map_add' S1 S2 := by
@ -301,6 +301,7 @@ lemma map_add₃ (f : TriLinearSymm V) (S T L1 L2 : V) :
f (S, T, L1 + L2) = f (S, T, L1) + f (S, T, L2) := by
rw [f.swap₃, f.map_add₁, f.swap₃, f.swap₃ L2 T S]
/-- Fixing the second and third input vectors, the resulting linear map. -/
def toLinear₁ (f : TriLinearSymm V) (T L : V) : V →ₗ[ℚ] ℚ where
toFun S := f (S, T, L)
map_add' S1 S2 := by

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

@ -23,7 +23,7 @@ open BigOperators
namespace PlaneSeven
/-- A charge assignment forming one of the basis elements of the plane. -/
def B₀ : (SM 3).charges := toSpeciesEquiv.invFun ( fun s => fun i =>
match s, i with
| 0, 0 => 1
@ -36,6 +36,7 @@ lemma B₀_cubic (S T : (SM 3).charges) : cubeTriLin (B₀, S, T) =
simp [Fin.sum_univ_three, B₀, Fin.divNat, Fin.modNat, finProdFinEquiv]
ring
/-- A charge assignment forming one of the basis elements of the plane. -/
def B₁ : (SM 3).charges := toSpeciesEquiv.invFun ( fun s => fun i =>
match s, i with
| 1, 0 => 1
@ -48,6 +49,7 @@ lemma B₁_cubic (S T : (SM 3).charges) : cubeTriLin (B₁, S, T) =
simp [Fin.sum_univ_three, B₁, Fin.divNat, Fin.modNat, finProdFinEquiv]
ring
/-- A charge assignment forming one of the basis elements of the plane. -/
def B₂ : (SM 3).charges := toSpeciesEquiv.invFun ( fun s => fun i =>
match s, i with
| 2, 0 => 1
@ -60,6 +62,7 @@ lemma B₂_cubic (S T : (SM 3).charges) : cubeTriLin (B₂, S, T) =
simp [Fin.sum_univ_three, B₂, Fin.divNat, Fin.modNat, finProdFinEquiv]
ring
/-- A charge assignment forming one of the basis elements of the plane. -/
def B₃ : (SM 3).charges := toSpeciesEquiv.invFun ( fun s => fun i =>
match s, i with
| 3, 0 => 1
@ -73,6 +76,7 @@ lemma B₃_cubic (S T : (SM 3).charges) : cubeTriLin (B₃, S, T) =
ring_nf
rfl
/-- A charge assignment forming one of the basis elements of the plane. -/
def B₄ : (SM 3).charges := toSpeciesEquiv.invFun ( fun s => fun i =>
match s, i with
| 4, 0 => 1
@ -86,6 +90,7 @@ lemma B₄_cubic (S T : (SM 3).charges) : cubeTriLin (B₄, S, T) =
ring_nf
rfl
/-- A charge assignment forming one of the basis elements of the plane. -/
def B₅ : (SM 3).charges := toSpeciesEquiv.invFun ( fun s => fun i =>
match s, i with
| 5, 0 => 1
@ -99,6 +104,7 @@ lemma B₅_cubic (S T : (SM 3).charges) : cubeTriLin (B₅, S, T) =
ring_nf
rfl
/-- A charge assignment forming one of the basis elements of the plane. -/
def B₆ : (SM 3).charges := toSpeciesEquiv.invFun ( fun s => fun i =>
match s, i with
| 1, 2 => 1
@ -111,6 +117,7 @@ lemma B₆_cubic (S T : (SM 3).charges) : cubeTriLin (B₆, S, T) =
simp [Fin.sum_univ_three, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
ring_nf
/-- The charge assignments forming a basis of the plane. -/
@[simp]
def B : Fin 7 → (SM 3).charges := fun i =>
match i with
@ -191,49 +198,49 @@ lemma Bi_Bj_ne_cubic {i j : Fin 7} (h : i ≠ j) (S : (SM 3).charges) :
exact B₆_Bi_cubic h S
lemma B₀_B₀_Bi_cubic {i : Fin 7} :
cubeTriLin (B 0, B 0, B i) = 0 := by
cubeTriLin (B 0, B 0, B i) = 0 := by
change cubeTriLin (B₀, B₀, B i) = 0
rw [B₀_cubic]
fin_cases i <;>
simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
lemma B₁_B₁_Bi_cubic {i : Fin 7} :
cubeTriLin (B 1, B 1, B i) = 0 := by
cubeTriLin (B 1, B 1, B i) = 0 := by
change cubeTriLin (B₁, B₁, B i) = 0
rw [B₁_cubic]
fin_cases i <;>
simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
lemma B₂_B₂_Bi_cubic {i : Fin 7} :
cubeTriLin (B 2, B 2, B i) = 0 := by
cubeTriLin (B 2, B 2, B i) = 0 := by
change cubeTriLin (B₂, B₂, B i) = 0
rw [B₂_cubic]
fin_cases i <;>
simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
lemma B₃_B₃_Bi_cubic {i : Fin 7} :
cubeTriLin (B 3, B 3, B i) = 0 := by
cubeTriLin (B 3, B 3, B i) = 0 := by
change cubeTriLin (B₃, B₃, B i) = 0
rw [B₃_cubic]
fin_cases i <;>
simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
lemma B₄_B₄_Bi_cubic {i : Fin 7} :
cubeTriLin (B 4, B 4, B i) = 0 := by
cubeTriLin (B 4, B 4, B i) = 0 := by
change cubeTriLin (B₄, B₄, B i) = 0
rw [B₄_cubic]
fin_cases i <;>
simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
lemma B₅_B₅_Bi_cubic {i : Fin 7} :
cubeTriLin (B 5, B 5, B i) = 0 := by
cubeTriLin (B 5, B 5, B i) = 0 := by
change cubeTriLin (B₅, B₅, B i) = 0
rw [B₅_cubic]
fin_cases i <;>
simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
lemma B₆_B₆_Bi_cubic {i : Fin 7} :
cubeTriLin (B 6, B 6, B i) = 0 := by
cubeTriLin (B 6, B 6, B i) = 0 := by
change cubeTriLin (B₆, B₆, B i) = 0
rw [B₆_cubic]
fin_cases i <;>
@ -241,7 +248,7 @@ lemma B₆_B₆_Bi_cubic {i : Fin 7} :
lemma Bi_Bi_Bj_cubic (i j : Fin 7) :
cubeTriLin (B i, B i, B j) = 0 := by
cubeTriLin (B i, B i, B j) = 0 := by
fin_cases i
exact B₀_B₀_Bi_cubic
exact B₁_B₁_Bi_cubic

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

@ -6,7 +6,13 @@ Authors: Joseph Tooby-Smith
import HepLean.AnomalyCancellation.SMNu.PlusU1.Basic
import HepLean.AnomalyCancellation.SMNu.PlusU1.FamilyMaps
import HepLean.AnomalyCancellation.SMNu.PlusU1.PlaneNonSols
/-!
# Bound on plane dimension
We place an upper bound on the dimension of a plane of charges on which every point is a solution.
The upper bound is 7, proven in the theorem `plane_exists_dim_le_7`.
-/
universe v u
namespace SMRHN
@ -16,6 +22,8 @@ open SMνCharges
open SMνACCs
open BigOperators
/-- A proposition which is true if for a given `n` a plane of charges of dimension `n` exists
in which each point is a solution. -/
def existsPlane (n : ℕ) : Prop := ∃ (B : Fin n → (PlusU1 3).charges),
LinearIndependent ℚ B ∧ ∀ (f : Fin n → ℚ), (PlusU1 3).isSolution (∑ i, f i • B i)
@ -33,7 +41,7 @@ lemma exists_plane_exists_basis {n : ℕ} (hE : existsPlane n) :
have h1 : ∑ x : Fin n, -(g (Sum.inr x) • Y (Sum.inr x)) =
∑ x : Fin n, (-g (Sum.inr x)) • Y (Sum.inr x):= by
apply Finset.sum_congr
simp
simp only
intro i _
simp
rw [h1] at hg

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

@ -26,28 +26,40 @@ open BigOperators
namespace ElevenPlane
/-- A charge assignment forming one of the basis elements of the plane. -/
def B₀ : (PlusU1 3).charges := ![1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
/-- A charge assignment forming one of the basis elements of the plane. -/
def B₁ : (PlusU1 3).charges := ![0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
/-- A charge assignment forming one of the basis elements of the plane. -/
def B₂ : (PlusU1 3).charges := ![0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
/-- A charge assignment forming one of the basis elements of the plane. -/
def B₃ : (PlusU1 3).charges := ![0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
/-- A charge assignment forming one of the basis elements of the plane. -/
def B₄ : (PlusU1 3).charges := ![0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
/-- A charge assignment forming one of the basis elements of the plane. -/
def B₅ : (PlusU1 3).charges := ![0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0]
/-- A charge assignment forming one of the basis elements of the plane. -/
def B₆ : (PlusU1 3).charges := ![0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0]
/-- A charge assignment forming one of the basis elements of the plane. -/
def B₇ : (PlusU1 3).charges := ![0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0]
/-- A charge assignment forming one of the basis elements of the plane. -/
def B₈ : (PlusU1 3).charges := ![0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0]
/-- A charge assignment forming one of the basis elements of the plane. -/
def B₉ : (PlusU1 3).charges := ![0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 2, 0]
/-- A charge assignment forming one of the basis elements of the plane. -/
def B₁₀ : (PlusU1 3).charges := ![0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1]
/-- The charge assignment forming a basis of the plane. -/
def B : Fin 11 → (PlusU1 3).charges := fun i =>
match i with
| 0 => B₀
@ -76,7 +88,7 @@ lemma Bi_sum_quad (i : Fin 11) (f : Fin 11 → ℚ) :
rw [quadBiLin.map_smul₂, Bi_Bj_quad hij.symm]
simp
/-- The coefficents of the quadratic equation in our basis. -/
@[simp]
def quadCoeff : Fin 11 → ℚ := ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0]
@ -102,7 +114,7 @@ lemma isSolution_quadCoeff_f_sq_zero (f : Fin 11 → ℚ) (hS : (PlusU1 3).isSol
rw [Fintype.sum_eq_zero_iff_of_nonneg] at hQ
exact congrFun hQ k
intro i
simp
simp only [Pi.zero_apply, quadCoeff]
rw [mul_nonneg_iff]
apply Or.inl
apply And.intro