diff --git a/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean b/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean index d8c924d2..e24ce3a1 100644 --- 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 index 320dba17..d34340aa 100644 --- 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 index 7cadf48e..36cba929 100644 --- 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 index 4b50bba2..10017e48 100644 --- 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