Merge pull request #20 from HEPLean/jstoobysmith/minor_refactors

Minor refactors
HEPLean · May 9, 2024 · 1b95199 · 1b95199
2 parents 388c824 + 0619e74
commit 1b95199
Show file tree

Hide file tree

Showing 4 changed files with 20 additions and 16 deletions.
diff --git a/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean b/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean
@@ -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

diff --git a/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean b/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
@@ -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]

diff --git a/HepLean/FlavorPhysics/CKMMatrix/Basic.lean b/HepLean/FlavorPhysics/CKMMatrix/Basic.lean
@@ -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!]

diff --git a/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean b/HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean
@@ -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