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

Merge pull request #20 from HEPLean/jstoobysmith/minor_refactors

Browse source 
Minor refactors
This commit is contained in:
Joseph Tooby-Smith 2024-05-09 13:20:50 -04:00 • committed by GitHub
commit 1b951994ae
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 20 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -54,7 +54,8 @@ lemma accGrav_Q_zero {S : (SMNoGrav 1).Sols} (hQ : Q S.val (0 : Fin 1) = 0) :
simp_all
linear_combination 3 * h2
lemma accGrav_Q_neq_zero {S : (SMNoGrav 1).Sols} (hQ : Q S.val (0 : Fin 1) ≠ 0) :
lemma accGrav_Q_neq_zero {S : (SMNoGrav 1).Sols} (hQ : Q S.val (0 : Fin 1) ≠ 0)
(FLTThree : FermatLastTheoremWith ℚ 3) :
accGrav S.val = 0 := by
have hE := E_zero_iff_Q_zero.mpr.mt hQ
let S' := linearParametersQENeqZero.bijection.symm ⟨S.1.1, And.intro hQ hE⟩
@ -64,13 +65,14 @@ lemma accGrav_Q_neq_zero {S : (SMNoGrav 1).Sols} (hQ : Q S.val (0 : Fin 1) ≠ 0
change _ = S.val at hS'
rw [← hS'] at hC
rw [← hS']
exact S'.grav_of_cubic hC
exact S'.grav_of_cubic hC FLTThree
/-- Any solution to the ACCs without gravity satifies the gravitational ACC. -/
theorem accGravSatisfied {S : (SMNoGrav 1).Sols} : accGrav S.val = 0 := by
theorem accGravSatisfied {S : (SMNoGrav 1).Sols} (FLTThree : FermatLastTheoremWith ℚ 3) :
accGrav S.val = 0 := by
by_cases hQ : Q S.val (0 : Fin 1)= 0
exact accGrav_Q_zero hQ
exact accGrav_Q_neq_zero hQ
exact accGrav_Q_neq_zero hQ FLTThree
end One

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

@ -285,9 +285,9 @@ lemma cubic (S : linearParametersQENeqZero) :
simp_all
rw [add_eq_zero_iff_eq_neg]
lemma FLTThree : FermatLastTheoremWith ℚ 3 := by sorry
lemma cubic_v_or_w_zero (S : linearParametersQENeqZero) (h : accCube (bijection S).1.val = 0) :
lemma cubic_v_or_w_zero (S : linearParametersQENeqZero) (h : accCube (bijection S).1.val = 0)
(FLTThree : FermatLastTheoremWith ℚ 3) :
S.v = 0 ∨ S.w = 0 := by
rw [S.cubic] at h
have h1 : (-1)^3 = (-1 : ℚ):= by rfl
@ -335,9 +335,10 @@ lemma cube_w_zero (S : linearParametersQENeqZero) (h : accCube (bijection S).1.v
simp_all
linear_combination h'
lemma cube_w_v (S : linearParametersQENeqZero) (h : accCube (bijection S).1.val = 0) :
lemma cube_w_v (S : linearParametersQENeqZero) (h : accCube (bijection S).1.val = 0)
(FLTThree : FermatLastTheoremWith ℚ 3) :
(S.v = -1 ∧ S.w = 0) ∨ (S.v = 0 ∧ S.w = -1) := by
have h' := cubic_v_or_w_zero S h
have h' := cubic_v_or_w_zero S h FLTThree
cases' h' with hx hx
simp [hx]
exact cubic_v_zero S h hx
@ -357,10 +358,11 @@ lemma grav (S : linearParametersQENeqZero) : accGrav (bijection S).1.val = 0 ↔
rw [h]
ring
lemma grav_of_cubic (S : linearParametersQENeqZero) (h : accCube (bijection S).1.val = 0) :
lemma grav_of_cubic (S : linearParametersQENeqZero) (h : accCube (bijection S).1.val = 0)
(FLTThree : FermatLastTheoremWith ℚ 3) :
accGrav (bijection S).1.val = 0 := by
rw [grav]
have h' := cube_w_v S h
have h' := cube_w_v S h FLTThree
cases' h' with h h
rw [h.1, h.2]
simp only [add_zero]

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

@ -108,7 +108,7 @@ lemma phaseShiftRelation_trans {U V W : unitaryGroup (Fin 3) ℂ} :
rw [add_comm k e, add_comm l f, add_comm m g]
lemma phaseShiftEquivRelation : Equivalence phaseShiftRelation where
lemma phaseShiftRelation_equiv : Equivalence phaseShiftRelation where
refl := phaseShiftRelation_refl
symm := phaseShiftRelation_symm
trans := phaseShiftRelation_trans
@ -149,7 +149,7 @@ scoped[CKMMatrix] notation (name := ts_element) "[" V "]ts" => V.1 2 1
/-- The `tb`th element of the CKM matrix. -/
scoped[CKMMatrix] notation (name := tb_element) "[" V "]tb" => V.1 2 2
instance CKMMatrixSetoid : Setoid CKMMatrix := ⟨phaseShiftRelation, phaseShiftEquivRelation⟩
instance CKMMatrixSetoid : Setoid CKMMatrix := ⟨phaseShiftRelation, phaseShiftRelation_equiv⟩
/-- The matrix obtained from `V` by shifting the phases of the fermions. -/
@[simps!]

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

@ -614,7 +614,7 @@ lemma eq_standParam_of_ubOnePhaseCond {V : CKMMatrix} (hV : ubOnePhaseCond V) :
theorem exists_δ₁₃ (V : CKMMatrix) :
∃ (δ₃ : ℝ), V ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₃ := by
obtain ⟨U, hU⟩ := fstRowThdColRealCond_holds_up_to_equiv V
have hUV : ⟦U⟧ = ⟦V⟧ := (Quotient.eq.mpr (phaseShiftEquivRelation.symm hU.1))
have hUV : ⟦U⟧ = ⟦V⟧ := (Quotient.eq.mpr (phaseShiftRelation_equiv.symm hU.1))
by_cases ha : [V]ud ≠ 0 ∨ [V]us ≠ 0
· have haU : [U]ud ≠ 0 ∨ [U]us ≠ 0 := by -- should be much simplier
by_contra hn
@ -638,8 +638,8 @@ theorem exists_δ₁₃ (V : CKMMatrix) :
exact ha
simpa [not_or, VAbs] using h1
have ⟨U2, hU2⟩ := ubOnePhaseCond_hold_up_to_equiv_of_ub_one haU hU.2
have hUVa2 : V ≈ U2 := phaseShiftEquivRelation.trans hU.1 hU2.1
have hUV2 : ⟦U2⟧ = ⟦V⟧ := (Quotient.eq.mpr (phaseShiftEquivRelation.symm hUVa2))
have hUVa2 : V ≈ U2 := phaseShiftRelation_equiv.trans hU.1 hU2.1
have hUV2 : ⟦U2⟧ = ⟦V⟧ := (Quotient.eq.mpr (phaseShiftRelation_equiv.symm hUVa2))
have hx := eq_standParam_of_ubOnePhaseCond hU2.2
use 0
rw [← hUV2, ← hx]
@ -661,7 +661,7 @@ theorem eq_standardParameterization_δ₃ (V : CKMMatrix) :
simp
rw [h1]
rw [mulExpδ₁₃_on_param_eq_zero_iff, Vs_zero_iff_cos_sin_zero] at h
refine phaseShiftEquivRelation.trans hδ₃ ?_
refine phaseShiftRelation_equiv.trans hδ₃ ?_
rcases h with h | h | h | h | h | h
exact on_param_cos_θ₁₂_eq_zero δ₁₃' h
exact on_param_cos_θ₁₃_eq_zero δ₁₃' h