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

feat: replace FLT sorry with assumptions

Browse source
This commit is contained in:
jstoobysmith 2024-05-08 15:42:54 -04:00
parent 388c824463
commit 70cafbf41e
2 changed files with 14 additions and 10 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]