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

Merge branch 'master' into simp_replace

Browse source
This commit is contained in:
jstoobysmith 2024-09-03 15:17:18 -04:00
commit c07f8444a1
16 changed files with 109 additions and 192 deletions
Download patch file Download diff file Expand all files Collapse all files

16
HepLean/AnomalyCancellation/GroupActions.lean
View file

@ -45,12 +45,8 @@ def linSolMap {χ : ACCSystem} (G : ACCSystemGroupAction χ) (g : G.group) :
toFun S := ⟨G.rep g S.val, by
intro i
rw [G.linearInvariant, S.linearSol]⟩
map_add' S T := by
apply ACCSystemLinear.LinSols.ext
exact (G.rep g).map_add' _ _
map_smul' a S := by
apply ACCSystemLinear.LinSols.ext
exact (G.rep g).map_smul' _ _
map_add' S T := ACCSystemLinear.LinSols.ext ((G.rep g).map_add' _ _)
map_smul' a S := ACCSystemLinear.LinSols.ext ((G.rep g).map_smul' _ _)
/-- The representation acting on the vector space of solutions to the linear ACCs. -/
@[simps!]
@ -58,16 +54,12 @@ def linSolRep {χ : ACCSystem} (G : ACCSystemGroupAction χ) :
Representation ℚ G.group χ.LinSols where
toFun := G.linSolMap
map_mul' g1 g2 := by
apply LinearMap.ext
intro S
apply ACCSystemLinear.LinSols.ext
refine LinearMap.ext fun S ↦ ACCSystemLinear.LinSols.ext ?_
change (G.rep (g1 * g2)) S.val = _
rw [G.rep.map_mul]
rfl
map_one' := by
apply LinearMap.ext
intro S
apply ACCSystemLinear.LinSols.ext
refine LinearMap.ext fun S ↦ ACCSystemLinear.LinSols.ext ?_
change (G.rep.toFun 1) S.val = _
rw [G.rep.map_one']
rfl

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

@ -74,8 +74,7 @@ lemma sum_δ₁_δ₂ (S : Fin (2 * n.succ) → ℚ) :
· intro i
simp only [mem_univ, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv]
· exact fun _ _=> rfl
rw [h1]
rw [Fin.sum_univ_add, Finset.sum_add_distrib]
rw [h1, Fin.sum_univ_add, Finset.sum_add_distrib]
rfl
lemma sum_δ₁_δ₂' (S : Fin (2 * n.succ) → ℚ) :
@ -85,8 +84,7 @@ lemma sum_δ₁_δ₂' (S : Fin (2 * n.succ) → ℚ) :
· intro i
simp only [mem_univ, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv]
· exact fun _ _ => rfl
rw [h1]
rw [Fin.sum_univ_add, Finset.sum_add_distrib]
rw [h1, Fin.sum_univ_add, Finset.sum_add_distrib]
rfl
lemma sum_δ!₁_δ!₂ (S : Fin (2 * n.succ) → ℚ) :

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

@ -162,12 +162,8 @@ def bijectionQEZero : {S : linearParameters // S.Q' ≠ 0 ∧ S.E' ≠ 0} ≃
{S : (SMNoGrav 1).LinSols // Q S.val (0 : Fin 1) ≠ 0 ∧ E S.val (0 : Fin 1) ≠ 0} where
toFun S := ⟨bijection S, S.2⟩
invFun S := ⟨bijection.symm S, S.2⟩
left_inv S := by
apply Subtype.ext
exact bijection.left_inv S.1
right_inv S := by
apply Subtype.ext
exact bijection.right_inv S.1
left_inv S := Subtype.ext (bijection.left_inv S.1)
right_inv S := Subtype.ext (bijection.right_inv S.1)
lemma grav (S : linearParameters) :
accGrav S.asCharges = 0 ↔ S.E' = 6 * S.Q' := by

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

@ -40,8 +40,8 @@ def toSpeciesEquiv : (SMνCharges n).Charges ≃ (Fin 6 → Fin n → ℚ) :=
@[simps!]
def toSpecies (i : Fin 6) : (SMνCharges n).Charges →ₗ[ℚ] (SMνSpecies n).Charges where
toFun S := toSpeciesEquiv S i
map_add' _ _ := by rfl
map_smul' _ _ := by rfl
map_add' _ _ := rfl
map_smul' _ _ := rfl
lemma charges_eq_toSpecies_eq (S T : (SMνCharges n).Charges) :
S = T ↔ ∀ i, toSpecies i S = toSpecies i T := by
@ -194,7 +194,8 @@ def accYY : (SMνCharges n).Charges →ₗ[ℚ] ℚ where
map_add' S T := by
simp only
repeat rw [map_add]
simp [Pi.add_apply, mul_add]
simp only [SMνSpecies_numberCharges, ACCSystemCharges.chargesAddCommMonoid_add, toSpecies_apply,
Fin.isValue, mul_add]
repeat erw [Finset.sum_add_distrib]
ring
map_smul' a S := by
@ -232,8 +233,7 @@ def quadBiLin : BiLinearSymm (SMνCharges n).Charges := BiLinearSymm.mk₂
intro a S T
simp only
rw [Finset.mul_sum]
apply Fintype.sum_congr
intro i
refine Fintype.sum_congr _ _ fun i ↦ ?_
repeat erw [map_smul]
simp [HSMul.hSMul, SMul.smul]
ring)
@ -241,8 +241,7 @@ def quadBiLin : BiLinearSymm (SMνCharges n).Charges := BiLinearSymm.mk₂
intro S T R
simp only
rw [← Finset.sum_add_distrib]
apply Fintype.sum_congr
intro i
refine Fintype.sum_congr _ _ fun i ↦ ?_
repeat erw [map_add]
simp only [ACCSystemCharges.chargesAddCommMonoid_add, toSpecies_apply, Fin.isValue, neg_mul,
one_mul]
@ -250,8 +249,7 @@ def quadBiLin : BiLinearSymm (SMνCharges n).Charges := BiLinearSymm.mk₂
(by
intro S T
simp only [SMνSpecies_numberCharges, toSpecies_apply, Fin.isValue, neg_mul, one_mul]
apply Fintype.sum_congr
intro i
refine Fintype.sum_congr _ _ fun i ↦ ?_
ring)
lemma quadBiLin_decomp (S T : (SMνCharges n).Charges) :
@ -298,8 +296,7 @@ def cubeTriLin : TriLinearSymm (SMνCharges n).Charges := TriLinearSymm.mk₃
intro a S T R
simp only
rw [Finset.mul_sum]
apply Fintype.sum_congr
intro i
refine Fintype.sum_congr _ _ fun i ↦ ?_
repeat erw [map_smul]
simp [HSMul.hSMul, SMul.smul]
ring)
@ -307,22 +304,19 @@ def cubeTriLin : TriLinearSymm (SMνCharges n).Charges := TriLinearSymm.mk₃
intro S T R L
simp only
rw [← Finset.sum_add_distrib]
apply Fintype.sum_congr
intro i
refine Fintype.sum_congr _ _ fun i ↦ ?_
repeat erw [map_add]
simp only [ACCSystemCharges.chargesAddCommMonoid_add, toSpecies_apply, Fin.isValue]
ring)
(by
intro S T L
simp only [SMνSpecies_numberCharges, toSpecies_apply, Fin.isValue]
apply Fintype.sum_congr
intro i
refine Fintype.sum_congr _ _ fun i ↦ ?_
ring)
(by
intro S T L
simp only [SMνSpecies_numberCharges, toSpecies_apply, Fin.isValue]
apply Fintype.sum_congr
intro i
refine Fintype.sum_congr _ _ fun i ↦ ?_
ring)
lemma cubeTriLin_decomp (S T R : (SMνCharges n).Charges) :

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

@ -8,7 +8,6 @@ import HepLean.AnomalyCancellation.SMNu.Basic
# Family maps for the Standard Model for RHN ACCs
We define the a series of maps between the charges for different numbers of families.
-/
universe v u
@ -25,15 +24,12 @@ def chargesMapOfSpeciesMap {n m : ℕ} (f : (SMνSpecies n).Charges →ₗ[ℚ]
map_add' S T := by
rw [charges_eq_toSpecies_eq]
intro i
rw [map_add]
rw [toSMSpecies_toSpecies_inv, toSMSpecies_toSpecies_inv, toSMSpecies_toSpecies_inv]
rw [map_add]
rw [map_add, toSMSpecies_toSpecies_inv, toSMSpecies_toSpecies_inv, toSMSpecies_toSpecies_inv,
map_add]
map_smul' a S := by
rw [charges_eq_toSpecies_eq]
intro i
rw [map_smul]
rw [toSMSpecies_toSpecies_inv, toSMSpecies_toSpecies_inv]
rw [map_smul]
rw [map_smul, toSMSpecies_toSpecies_inv, toSMSpecies_toSpecies_inv, map_smul]
rfl
lemma chargesMapOfSpeciesMap_toSpecies {n m : ℕ}
@ -89,9 +85,9 @@ a universal manor. -/
@[simps!]
def speciesFamilyUniversial (n : ℕ) :
(SMνSpecies 1).Charges →ₗ[ℚ] (SMνSpecies n).Charges where
toFun S _ := S ⟨0, by simp⟩
map_add' S T := rfl
map_smul' a S := rfl
toFun S _ := S ⟨0, Nat.zero_lt_succ 0⟩
map_add' _ _ := rfl
map_smul' _ _ := rfl
/-- The embedding of the `1`-family charges into the `n`-family charges in
a universal manor. -/

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

@ -11,8 +11,8 @@ import HepLean.AnomalyCancellation.GroupActions
We define the ACC system for the Standard Model with right-handed neutrinos and no gravitational
anomaly.
-/
universe v u
namespace SMRHN
@ -29,9 +29,7 @@ def SMNoGrav (n : ℕ) : ACCSystem where
| 0 => @accSU2 n
| 1 => accSU3
numberQuadratic := 0
quadraticACCs := by
intro i
exact Fin.elim0 i
quadraticACCs := fun i ↦ Fin.elim0 i
cubicACC := accCube
namespace SMNoGrav
@ -48,8 +46,7 @@ lemma SU3Sol (S : (SMNoGrav n).LinSols) : accSU3 S.val = 0 := by
simp at hS
exact hS 1
lemma cubeSol (S : (SMNoGrav n).Sols) : accCube S.val = 0 := by
exact S.cubicSol
lemma cubeSol (S : (SMNoGrav n).Sols) : accCube S.val = 0 := S.cubicSol
/-- An element of `charges` which satisfies the linear ACCs
gives us a element of `LinSols`. -/
@ -64,10 +61,7 @@ def chargeToLinear (S : (SMNoGrav n).Charges) (hSU2 : accSU2 S = 0) (hSU3 : accS
/-- An element of `LinSols` which satisfies the quadratic ACCs
gives us a element of `QuadSols`. -/
def linearToQuad (S : (SMNoGrav n).LinSols) : (SMNoGrav n).QuadSols :=
⟨S, by
intro i
exact Fin.elim0 i⟩
def linearToQuad (S : (SMNoGrav n).LinSols) : (SMNoGrav n).QuadSols := ⟨S, fun i ↦ Fin.elim0 i⟩
/-- An element of `QuadSols` which satisfies the quadratic ACCs
gives us a element of `LinSols`. -/
@ -100,13 +94,13 @@ def perm (n : ℕ) : ACCSystemGroupAction (SMNoGrav n) where
rep := repCharges
linearInvariant := by
intro i
simp at i
simp only [SMNoGrav_numberLinear] at i
match i with
| 0 => exact accSU2_invariant
| 1 => exact accSU3_invariant
quadInvariant := by
intro i
simp at i
simp only [SMNoGrav_numberQuadratic] at i
exact Fin.elim0 i
cubicInvariant := accCube_invariant

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

@ -10,11 +10,9 @@ import HepLean.AnomalyCancellation.GroupActions
# ACC system for SM with RHN (without hypercharge).
We define the ACC system for the Standard Model (without hypercharge) with right-handed neutrinos.
-/
universe v u
namespace SMRHN
open SMνCharges
open SMνACCs
@ -30,9 +28,7 @@ def SM (n : ℕ) : ACCSystem where
| 1 => accSU2
| 2 => accSU3
numberQuadratic := 0
quadraticACCs := by
intro i
exact Fin.elim0 i
quadraticACCs := fun i ↦ Fin.elim0 i
cubicACC := accCube
namespace SM
@ -54,8 +50,7 @@ lemma SU3Sol (S : (SM n).LinSols) : accSU3 S.val = 0 := by
simp at hS
exact hS 2
lemma cubeSol (S : (SM n).Sols) : accCube S.val = 0 := by
exact S.cubicSol
lemma cubeSol (S : (SM n).Sols) : accCube S.val = 0 := S.cubicSol
/-- An element of `charges` which satisfies the linear ACCs
gives us a element of `LinSols`. -/
@ -72,9 +67,7 @@ def chargeToLinear (S : (SM n).Charges) (hGrav : accGrav S = 0)
/-- An element of `LinSols` which satisfies the quadratic ACCs
gives us a element of `QuadSols`. -/
def linearToQuad (S : (SM n).LinSols) : (SM n).QuadSols :=
⟨S, by
intro i
exact Fin.elim0 i⟩
⟨S, fun i ↦ Fin.elim0 i⟩
/-- An element of `QuadSols` which satisfies the quadratic ACCs
gives us a element of `Sols`. -/

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

@ -12,7 +12,6 @@ We give an example of a 7 dimensional plane on which every point satisfies the A
The main result of this file is `seven_dim_plane_exists` which states that there exists a
7 dimensional plane of charges on which every point satisfies the ACCs.
-/
namespace SMRHN
@ -253,21 +252,14 @@ lemma Bi_Bj_Bk_cubic (i j k : Fin 7) :
theorem B_in_accCube (f : Fin 7 → ℚ) : accCube (∑ i, f i • B i) = 0 := by
change cubeTriLin _ _ _ = 0
rw [cubeTriLin.map_sum₁₂₃]
apply Fintype.sum_eq_zero
intro i
apply Fintype.sum_eq_zero
intro k
apply Fintype.sum_eq_zero
intro l
rw [cubeTriLin.map_smul₁, cubeTriLin.map_smul₂, cubeTriLin.map_smul₃]
rw [Bi_Bj_Bk_cubic]
apply Fintype.sum_eq_zero _ fun i ↦ Fintype.sum_eq_zero _ fun k ↦ Fintype.sum_eq_zero _ fun l ↦ ?_
rw [cubeTriLin.map_smul₁, cubeTriLin.map_smul₂, cubeTriLin.map_smul₃, Bi_Bj_Bk_cubic]
simp
lemma B_sum_is_sol (f : Fin 7 → ℚ) : (SM 3).IsSolution (∑ i, f i • B i) := by
let X := chargeToAF (∑ i, f i • B i) (by
rw [map_sum]
apply Fintype.sum_eq_zero
intro i
apply Fintype.sum_eq_zero _ fun i ↦ ?_
rw [map_smul]
have h : accGrav (B i) = 0 := by
fin_cases i <;> rfl
@ -275,20 +267,16 @@ lemma B_sum_is_sol (f : Fin 7 → ℚ) : (SM 3).IsSolution (∑ i, f i • B i)
exact DistribMulAction.smul_zero (f i))
(by
rw [map_sum]
apply Fintype.sum_eq_zero
intro i
apply Fintype.sum_eq_zero _ fun i ↦ ?_
rw [map_smul]
have h : accSU2 (B i) = 0 := by
fin_cases i <;> rfl
have h : accSU2 (B i) = 0 := by fin_cases i <;> rfl
rw [h]
exact DistribMulAction.smul_zero (f i))
(by
rw [map_sum]
apply Fintype.sum_eq_zero
intro i
apply Fintype.sum_eq_zero _ fun i ↦ ?_
rw [map_smul]
have h : accSU3 (B i) = 0 := by
fin_cases i <;> rfl
have h : accSU3 (B i) = 0 := by fin_cases i <;> rfl
rw [h]
exact DistribMulAction.smul_zero (f i))
(B_in_accCube f)
@ -296,8 +284,7 @@ lemma B_sum_is_sol (f : Fin 7 → ℚ) : (SM 3).IsSolution (∑ i, f i • B i)
rfl
theorem basis_linear_independent : LinearIndependent ℚ B := by
apply Fintype.linearIndependent_iff.mpr
intro f h
refine Fintype.linearIndependent_iff.mpr fun f h ↦ ?_
have h0 := congrFun h (0 : Fin 18)
have h1 := congrFun h (3 : Fin 18)
have h2 := congrFun h (6 : Fin 18)

8
HepLean/AnomalyCancellation/SMNu/Ordinary/FamilyMaps.lean
View file

@ -29,12 +29,8 @@ def familyUniversalLinear (n : ℕ) :
(by rw [familyUniversal_accGrav, gravSol S, mul_zero])
(by rw [familyUniversal_accSU2, SU2Sol S, mul_zero])
(by rw [familyUniversal_accSU3, SU3Sol S, mul_zero])
map_add' S T := by
apply ACCSystemLinear.LinSols.ext
exact (familyUniversal n).map_add' _ _
map_smul' a S := by
apply ACCSystemLinear.LinSols.ext
exact (familyUniversal n).map_smul' _ _
map_add' S T := ACCSystemLinear.LinSols.ext ((familyUniversal n).map_add' _ _)
map_smul' a S := ACCSystemLinear.LinSols.ext ((familyUniversal n).map_smul' _ _)
/-- The family universal maps on `QuadSols`. -/
def familyUniversalQuad (n : ℕ) :

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

@ -10,7 +10,6 @@ import Mathlib.RepresentationTheory.Basic
# Permutations of SM charges with RHN.
We define the group of permutations for the SM charges with RHN.
-/
universe v u
@ -54,8 +53,7 @@ def repCharges {n : ℕ} : Representation ℚ (PermGroup n) (SMνCharges n).Char
repeat erw [toSMSpecies_toSpecies_inv]
rfl
map_one' := by
apply LinearMap.ext
intro S
refine LinearMap.ext fun S => ?_
rw [charges_eq_toSpecies_eq]
intro i
erw [toSMSpecies_toSpecies_inv]
@ -75,32 +73,26 @@ lemma toSpecies_sum_invariant (m : ℕ) (f : PermGroup n) (S : (SMνCharges n).C
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)
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)
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
(by simpa using toSpecies_sum_invariant 1 f S)
accSU3_ext (by simpa using toSpecies_sum_invariant 1 f S)
lemma accYY_invariant (f : PermGroup n) (S : (SMνCharges n).Charges) :
accYY (repCharges f S) = accYY S :=
accYY_ext
(by simpa using toSpecies_sum_invariant 1 f S)
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
(toSpecies_sum_invariant 2 f S)
accQuad_ext (toSpecies_sum_invariant 2 f S)
lemma accCube_invariant (f : PermGroup n) (S : (SMνCharges n).Charges) :
accCube (repCharges f S) = accCube S :=
accCube_ext
(by simpa using toSpecies_sum_invariant 3 f S)
accCube_ext (by simpa using toSpecies_sum_invariant 3 f S)
end SMRHN

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

@ -67,7 +67,7 @@ lemma on_quadBiLin (S : (PlusU1 n).Charges) :
lemma on_quadBiLin_AFL (S : (PlusU1 n).LinSols) : quadBiLin (BL n).val S.val = 0 := by
rw [on_quadBiLin, YYsol S, SU2Sol S, SU3Sol S]
rfl
simp
lemma add_AFL_quad (S : (PlusU1 n).LinSols) (a b : ℚ) :
accQuad (a • S.val + b • (BL n).val) = a ^ 2 * accQuad S.val := by
@ -86,7 +86,7 @@ def addQuad (S : (PlusU1 n).QuadSols) (a b : ℚ) : (PlusU1 n).QuadSols :=
linearToQuad (a • S.1 + b • (BL n).1.1) (add_quad S a b)
lemma addQuad_zero (S : (PlusU1 n).QuadSols) (a : ℚ) : addQuad S a 0 = a • S := by
simp [addQuad, linearToQuad]
simp only [addQuad, linearToQuad, zero_smul, add_zero]
rfl
lemma on_cubeTriLin (S : (PlusU1 n).Charges) :
@ -100,7 +100,7 @@ lemma on_cubeTriLin (S : (PlusU1 n).Charges) :
lemma on_cubeTriLin_AFL (S : (PlusU1 n).LinSols) :
cubeTriLin (BL n).val (BL n).val S.val = 0 := by
rw [on_cubeTriLin, gravSol S, SU3Sol S]
rfl
simp
lemma add_AFL_cube (S : (PlusU1 n).LinSols) (a b : ℚ) :
accCube (a • S.val + b • (BL n).val) =

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

@ -10,7 +10,6 @@ import HepLean.AnomalyCancellation.GroupActions
# ACC system for SM with RHN
We define the ACC system for the Standard Model with right-handed neutrinos.
-/
universe v u

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

@ -24,17 +24,22 @@ 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)
LinearIndependent ℚ B ∧ ∀ (f : Fin n → ℚ), (PlusU1 3).IsSolution (∑ i, f i • B i)
lemma exists_plane_exists_basis {n : ℕ} (hE : ExistsPlane n) :
∃ (B : Fin 11 ⊕ Fin n → (PlusU1 3).Charges), LinearIndependent ℚ B := by
obtain ⟨E, hE1, hE2⟩ := hE
obtain ⟨B, hB1, hB2⟩ := eleven_dim_plane_of_no_sols_exists
let Y := Sum.elim B E
use Y
refine Fintype.linearIndependent_iff.mpr (fun g hg => ?_)
rw [Fintype.sum_sum_type, add_eq_zero_iff_eq_neg, ← Finset.sum_neg_distrib] at hg
rw [Finset.sum_congr rfl (fun i _ => (neg_smul (g (Sum.inr i)) (Y (Sum.inr i))).symm)] at hg
refine ⟨Y, Fintype.linearIndependent_iff.mpr fun g hg ↦ ?_⟩
rw [@Fintype.sum_sum_type, @add_eq_zero_iff_eq_neg, ← @Finset.sum_neg_distrib] at hg
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 only
intro i _
simp
rw [h1] at hg
have h2 : ∑ a₁ : Fin 11, g (Sum.inl a₁) • Y (Sum.inl a₁) = 0 := by
apply hB2
erw [hg]

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

@ -65,8 +65,7 @@ lemma on_quadBiLin (S : (PlusU1 n).Charges) :
simp
lemma on_quadBiLin_AFL (S : (PlusU1 n).LinSols) : quadBiLin (Y n).val S.val = 0 := by
rw [on_quadBiLin]
rw [YYsol S]
rw [on_quadBiLin, 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
@ -77,16 +76,14 @@ lemma add_AFL_quad (S : (PlusU1 n).LinSols) (a b : ℚ) :
lemma add_quad (S : (PlusU1 n).QuadSols) (a b : ℚ) :
accQuad (a • S.val + b • (Y n).val) = 0 := by
rw [add_AFL_quad, quadSol S]
simp
rw [add_AFL_quad, quadSol S]; simp
/-- The `QuadSol` obtained by adding hypercharge to a `QuadSol`. -/
def addQuad (S : (PlusU1 n).QuadSols) (a b : ℚ) : (PlusU1 n).QuadSols :=
linearToQuad (a • S.1 + b • (Y n).1.1) (add_quad S a b)
lemma addQuad_zero (S : (PlusU1 n).QuadSols) (a : ℚ) : addQuad S a 0 = a • S := by
simp [addQuad, linearToQuad]
rfl
simp only [addQuad, linearToQuad, zero_smul, add_zero]; rfl
lemma on_cubeTriLin (S : (PlusU1 n).Charges) :
cubeTriLin (Y n).val (Y n).val S = 6 * accYY S := by
@ -98,8 +95,7 @@ lemma on_cubeTriLin (S : (PlusU1 n).Charges) :
lemma on_cubeTriLin_AFL (S : (PlusU1 n).LinSols) :
cubeTriLin (Y n).val (Y n).val S.val = 0 := by
rw [on_cubeTriLin, YYsol S]
rfl
rw [on_cubeTriLin, YYsol S]; simp
lemma on_cubeTriLin' (S : (PlusU1 n).Charges) :
cubeTriLin (Y n).val S S = 6 * accQuad S := by
@ -111,7 +107,7 @@ lemma on_cubeTriLin' (S : (PlusU1 n).Charges) :
lemma on_cubeTriLin'_ALQ (S : (PlusU1 n).QuadSols) :
cubeTriLin (Y n).val S.val S.val = 0 := by
rw [on_cubeTriLin', quadSol S, mul_zero]
rw [on_cubeTriLin', quadSol S]; simp
lemma add_AFL_cube (S : (PlusU1 n).LinSols) (a b : ℚ) :
accCube (a • S.val + b • (Y n).val) =
@ -125,15 +121,12 @@ lemma add_AFL_cube (S : (PlusU1 n).LinSols) (a b : ℚ) :
lemma add_AFQ_cube (S : (PlusU1 n).QuadSols) (a b : ℚ) :
accCube (a • S.val + b • (Y n).val) = a ^ 3 * accCube S.val := by
rw [add_AFL_cube]
rw [cubeTriLin.swap₃]
rw [on_cubeTriLin'_ALQ]
rw [add_AFL_cube, cubeTriLin.swap₃, on_cubeTriLin'_ALQ]
ring
lemma add_AF_cube (S : (PlusU1 n).Sols) (a b : ℚ) :
accCube (a • S.val + b • (Y n).val) = 0 := by
rw [add_AFQ_cube]
rw [cubeSol S]
rw [add_AFQ_cube, cubeSol S]
simp
/-- The `Sol` obtained by adding hypercharge to a `Sol`. -/

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

@ -80,8 +80,7 @@ lemma Bi_Bj_quad {i j : Fin 11} (hi : i ≠ j) : quadBiLin (B i) (B j) = 0 := by
lemma Bi_sum_quad (i : Fin 11) (f : Fin 11 → ℚ) :
quadBiLin (B i) (∑ k, f k • B k) = f i * quadBiLin (B i) (B i) := by
rw [quadBiLin.map_sum₂]
rw [Fintype.sum_eq_single i]
rw [quadBiLin.map_sum₂, Fintype.sum_eq_single i]
· rw [quadBiLin.map_smul₂]
· intro k hij
rw [quadBiLin.map_smul₂, Bi_Bj_quad hij.symm]
@ -99,8 +98,7 @@ lemma on_accQuad (f : Fin 11 → ℚ) :
accQuad (∑ i, f i • B i) = ∑ i, quadCoeff i * (f i)^2 := by
change quadBiLin _ _ = _
rw [quadBiLin.map_sum₁]
apply Fintype.sum_congr
intro i
refine Fintype.sum_congr _ _ fun i ↦ ?_
rw [quadBiLin.map_smul₁, Bi_sum_quad, quadCoeff_eq_bilinear]
ring
@ -108,14 +106,12 @@ lemma isSolution_quadCoeff_f_sq_zero (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSol
(k : Fin 11) : quadCoeff k * (f k)^2 = 0 := by
obtain ⟨S, hS⟩ := hS
have hQ := quadSol S.1
rw [hS, on_accQuad] at hQ
rw [Fintype.sum_eq_zero_iff_of_nonneg] at hQ
rw [hS, on_accQuad, Fintype.sum_eq_zero_iff_of_nonneg] at hQ
· exact congrFun hQ k
· intro i
simp only [Pi.zero_apply, quadCoeff]
rw [mul_nonneg_iff]
apply Or.inl
apply And.intro
apply Or.inl (And.intro _ _)
fin_cases i <;> rfl
exact sq_nonneg (f i)
@ -174,39 +170,31 @@ lemma isSolution_grav (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f
have hx := isSolution_sum_part f hS
obtain ⟨S, hS'⟩ := hS
have hg := gravSol S.toLinSols
rw [hS'] at hg
rw [hx] at hg
rw [accGrav.map_add, accGrav.map_smul, accGrav.map_smul] at hg
rw [show accGrav B₉ = 3 by rfl] at hg
rw [show accGrav B₁₀ = 1 by rfl] at hg
rw [hS', hx, accGrav.map_add, accGrav.map_smul, accGrav.map_smul, show accGrav B₉ = 3 by rfl,
show accGrav B₁₀ = 1 by rfl] at hg
simp at hg
linear_combination hg
lemma isSolution_sum_part' (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i • B i)) :
∑ i, f i • B i = f 9 • B₉ + (- 3 * f 9) • B₁₀ := by
rw [isSolution_sum_part f hS]
rw [isSolution_grav f hS]
rw [isSolution_sum_part f hS, isSolution_grav f hS]
lemma isSolution_f9 (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i • B i)) :
f 9 = 0 := by
have hx := isSolution_sum_part' f hS
obtain ⟨S, hS'⟩ := hS
have hc := cubeSol S
rw [hS'] at hc
rw [hx] at hc
rw [hS', hx] at hc
change cubeTriLin.toCubic _ = _ at hc
rw [cubeTriLin.toCubic_add] at hc
erw [accCube.map_smul] at hc
erw [accCube.map_smul (- 3 * f 9) B₁₀] at hc
rw [cubeTriLin.map_smul₁, cubeTriLin.map_smul₁, cubeTriLin.map_smul₂, cubeTriLin.map_smul₂,
cubeTriLin.map_smul₃, cubeTriLin.map_smul₃] at hc
rw [show accCube B₉ = 9 by rfl] at hc
rw [show accCube B₁₀ = 1 by rfl] at hc
rw [show cubeTriLin B₉ B₉ B₁₀ = 0 by rfl] at hc
rw [show cubeTriLin B₁₀ B₁₀ B₉ = 0 by rfl] at hc
rw [show accCube B₉ = 9 by rfl, show accCube B₁₀ = 1 by rfl, show cubeTriLin B₉ B₉ B₁₀ = 0 by rfl,
show cubeTriLin B₁₀ B₁₀ B₉ = 0 by rfl] at hc
simp at hc
have h1 : f 9 ^ 3 * 9 + (-(3 * f 9)) ^ 3 = - 18 * f 9 ^ 3 := by
ring
have h1 : f 9 ^ 3 * 9 + (-(3 * f 9)) ^ 3 = - 18 * f 9 ^ 3 := by ring
rw [h1] at hc
simpa using hc
@ -232,30 +220,19 @@ lemma isSolution_f_zero (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i,
lemma isSolution_only_if_zero (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i, f i • B i)) :
∑ i, f i • B i = 0 := by
rw [isSolution_sum_part f hS]
rw [isSolution_grav f hS]
rw [isSolution_f9 f hS]
rw [isSolution_sum_part f hS, isSolution_grav f hS, isSolution_f9 f hS]
simp
theorem basis_linear_independent : LinearIndependent ℚ B := by
apply Fintype.linearIndependent_iff.mpr
intro f h
let X : (PlusU1 3).Sols := chargeToAF 0 (by rfl) (by rfl) (by rfl) (by rfl) (by rfl) (by rfl)
have hS : (PlusU1 3).IsSolution (∑ i, f i • B i) := by
use X
rw [h]
rfl
exact isSolution_f_zero f hS
theorem basis_linear_independent : LinearIndependent ℚ B :=
Fintype.linearIndependent_iff.mpr fun f h ↦ isSolution_f_zero f
⟨chargeToAF 0 (by rfl) (by rfl) (by rfl) (by rfl) (by rfl) (by rfl), id (Eq.symm h)⟩
end ElevenPlane
theorem eleven_dim_plane_of_no_sols_exists : ∃ (B : Fin 11 → (PlusU1 3).Charges),
LinearIndependent ℚ B ∧
∀ (f : Fin 11 → ℚ), (PlusU1 3).IsSolution (∑ i, f i • B i) → ∑ i, f i • B i = 0 := by
use ElevenPlane.B
apply And.intro
· exact ElevenPlane.basis_linear_independent
· exact ElevenPlane.isSolution_only_if_zero
∀ (f : Fin 11 → ℚ), (PlusU1 3).IsSolution (∑ i, f i • B i) → ∑ i, f i • B i = 0 :=
⟨ElevenPlane.B, ElevenPlane.basis_linear_independent, ElevenPlane.isSolution_only_if_zero⟩
end PlusU1
end SMRHN