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

refactor: More simps

Browse source
This commit is contained in:
jstoobysmith 2024-10-12 08:16:24 +00:00
parent 1651b265e7
commit 4a396783ab
17 changed files with 138 additions and 87 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -36,14 +36,14 @@ lemma asCharges_eq_castSucc (j : Fin n) :
lemma asCharges_ne_castSucc {k j : Fin n} (h : k ≠ j) :
asCharges k (Fin.castSucc j) = 0 := by
simp [asCharges]
simp only [asCharges, Nat.succ_eq_add_one, PureU1_numberCharges, Fin.castSucc_inj]
split
· rename_i h1
exact False.elim (h (id (Eq.symm h1)))
· split
· rename_i h1 h2
rw [Fin.ext_iff] at h1 h2
simp at h1 h2
simp only [Fin.coe_castSucc, Fin.val_last] at h1 h2
have hj : j.val < n := by
exact j.prop
simp_all
@ -54,7 +54,7 @@ lemma asCharges_ne_castSucc {k j : Fin n} (h : k ≠ j) :
def asLinSols (j : Fin n) : (PureU1 n.succ).LinSols :=
⟨asCharges j, by
intro i
simp at i
simp only [Nat.succ_eq_add_one, PureU1_numberLinear] at i
match i with
| 0 =>
simp only [Fin.isValue, PureU1_linearACCs, accGrav,

22
HepLean/AnomalyCancellation/PureU1/ConstAbs.lean
View file

@ -34,7 +34,7 @@ lemma constAbs_perm (S : (PureU1 n).Charges) (M :(FamilyPermutations n).group) :
MonoidHom.coe_mk, OneHom.coe_mk, chargeMap_apply]
refine Iff.intro (fun h i j => ?_) (fun h i j => h (M.invFun i) (M.invFun j))
have h2 := h (M.toFun i) (M.toFun j)
simp at h2
simp only [Equiv.toFun_as_coe, Equiv.Perm.inv_apply_self] at h2
exact h2
lemma constAbs_sort {S : (PureU1 n).Charges} (CA : ConstAbs S) : ConstAbs (sort S) := by
@ -93,7 +93,7 @@ lemma is_zero (h0 : S (0 : Fin n.succ) = 0) : S = 0 := by
funext i
have ht := hS.1 i (0 : Fin n.succ)
rw [h0] at ht
simp at ht
simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, pow_eq_zero_iff] at ht
exact ht
/-- A boundary of `S : (PureU1 n.succ).charges` (assumed sorted, constAbs and non-zero)
@ -117,7 +117,8 @@ lemma boundary_split (k : Fin n) : k.succ.val + (n.succ - k.succ.val) = n.succ :
lemma boundary_accGrav' (k : Fin n) : accGrav n.succ S =
∑ i : Fin (k.succ.val + (n.succ - k.succ.val)), S (Fin.cast (boundary_split k) i) := by
simp [accGrav]
simp only [succ_eq_add_one, accGrav, LinearMap.coe_mk, AddHom.coe_mk, Fin.val_succ,
PureU1_numberCharges]
erw [Finset.sum_equiv (Fin.castOrderIso (boundary_split k)).toEquiv]
· intro i
simp only [Fin.val_succ, mem_univ, RelIso.coe_fn_toEquiv]
@ -149,7 +150,7 @@ include hS in
lemma not_hasBoundary_zero_le (hnot : ¬ (HasBoundary S)) (h0 : S (0 : Fin n.succ) < 0) :
∀ i, S (0 : Fin n.succ) = S i := by
intro ⟨i, hi⟩
simp at hnot
simp only [HasBoundary, Boundary, not_exists, not_and, not_lt] at hnot
induction i
· rfl
· rename_i i hii
@ -163,7 +164,7 @@ lemma not_hasBoundry_zero (hnot : ¬ (HasBoundary S)) (i : Fin n.succ) :
S (0 : Fin n.succ) = S i := by
by_cases hi : S (0 : Fin n.succ) < 0
· exact not_hasBoundary_zero_le hS hnot hi i
· simp at hi
· simp only [not_lt] at hi
exact zero_gt hS hi i
include hS in
@ -175,9 +176,9 @@ include hA in
lemma AFL_hasBoundary (h : A.val (0 : Fin n.succ) ≠ 0) : HasBoundary A.val := by
by_contra hn
have h0 := not_hasBoundary_grav hA hn
simp [accGrav] at h0
simp only [succ_eq_add_one, accGrav, LinearMap.coe_mk, AddHom.coe_mk, cast_add, cast_one] at h0
erw [pureU1_linear A] at h0
simp at h0
simp only [zero_eq_mul] at h0
cases' h0
· linarith
· simp_all
@ -187,9 +188,9 @@ lemma AFL_odd_noBoundary {A : (PureU1 (2 * n + 1)).LinSols} (h : ConstAbsSorted
by_contra hn
obtain ⟨k, hk⟩ := hn
have h0 := boundary_accGrav'' h k hk
simp [accGrav] at h0
simp only [succ_eq_add_one, accGrav, LinearMap.coe_mk, AddHom.coe_mk, cast_mul, cast_ofNat] at h0
erw [pureU1_linear A] at h0
simp [hA] at h0
simp only [zero_eq_mul, hA, or_false] at h0
have h1 : 2 * n = 2 * k.val + 1 := by
rw [← @Nat.cast_inj ℚ]
simp only [cast_mul, cast_ofNat, cast_add, cast_one]
@ -212,7 +213,8 @@ lemma AFL_even_Boundary {A : (PureU1 (2 * n.succ)).LinSols} (h : ConstAbsSorted
have h0 := boundary_accGrav'' h k hk
change ∑ i : Fin (succ (Nat.mul 2 n + 1)), A.val i = _ at h0
erw [pureU1_linear A] at h0
simp [hA] at h0
simp only [mul_eq, cast_add, cast_mul, cast_ofNat, cast_one, add_sub_add_right_eq_sub,
succ_eq_add_one, zero_eq_mul, hA, or_false] at h0
rw [← @Nat.cast_inj ℚ]
linear_combination h0 / 2

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

@ -158,8 +158,7 @@ lemma basis!_on_δ!₁_self (j : Fin n) : basis!AsCharges j (δ!₁ j) = 1 := by
lemma basis_on_δ₁_other {k j : Fin n.succ} (h : k ≠ j) :
basisAsCharges k (δ₁ j) = 0 := by
simp [basisAsCharges]
simp [δ₁, δ₂]
simp only [basisAsCharges, succ_eq_add_one, PureU1_numberCharges, δ₁, succ_eq_add_one, δ₂]
split
· rename_i h1
rw [Fin.ext_iff] at h1

2
HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean
View file

@ -63,7 +63,7 @@ lemma parameterizationCharge_cube (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (
/-- The construction of a `Sol` from a `Fin n.succ → ℚ`, a `Fin n → ℚ` and a `ℚ`. -/
def parameterization (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (a : ℚ) :
(PureU1 (2 * n.succ)).Sols :=
⟨⟨parameterizationAsLinear g f a, by intro i; simp at i; exact Fin.elim0 i⟩,
⟨⟨parameterizationAsLinear g f a, fun i => Fin.elim0 i⟩,
parameterizationCharge_cube g f a⟩
lemma anomalyFree_param {S : (PureU1 (2 * n.succ)).Sols}

22
HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean
View file

@ -74,7 +74,8 @@ lemma lineInPlaneCond_eq_last' {S : (PureU1 (n.succ.succ)).LinSols} (hS : LineIn
linear_combination h1S
have h2 := pureU1_last S
rw [Fin.sum_univ_castSucc] at h2
simp [h1] at h2
simp only [Nat.succ_eq_add_one, h1, Fin.succ_last, neg_add_rev, Finset.sum_const,
Finset.card_univ, Fintype.card_fin, nsmul_eq_mul] at h2
field_simp at h2
linear_combination h2
@ -85,7 +86,7 @@ lemma lineInPlaneCond_eq_last {S : (PureU1 (n.succ.succ.succ.succ.succ)).LinSols
by_contra hn
have h := lineInPlaneCond_eq_last' hS hn
rw [sq_eq_sq_iff_eq_or_eq_neg] at hn
simp [or_not] at hn
simp only [Nat.succ_eq_add_one, Fin.succ_last, not_or] at hn
have hx : ((2 : ℚ) - ↑(n + 3)) ≠ 0 := by
rw [Nat.cast_add]
simp only [Nat.cast_ofNat, ne_eq]
@ -95,8 +96,8 @@ lemma lineInPlaneCond_eq_last {S : (PureU1 (n.succ.succ.succ.succ.succ)).LinSols
have ht : S.val ((Fin.last n.succ.succ.succ).succ) =
- S.val ((Fin.last n.succ.succ.succ).castSucc) := by
rw [← mul_right_inj' hx]
simp [Nat.succ_eq_add_one]
simp at h
simp only [Nat.cast_add, Nat.cast_ofNat, Nat.succ_eq_add_one, Fin.succ_last, mul_neg]
simp only [Nat.cast_add, Nat.cast_ofNat, Nat.succ_eq_add_one, neg_sub] at h
rw [h]
ring
simp_all
@ -115,7 +116,7 @@ theorem linesInPlane_constAbs {S : (PureU1 (n.succ.succ.succ.succ.succ)).LinSols
intro i j
by_cases hij : i ≠ j
· exact linesInPlane_eq_sq hS i j hij
· simp at hij
· simp only [Nat.succ_eq_add_one, PureU1_numberCharges, ne_eq, Decidable.not_not] at hij
rw [hij]
lemma linesInPlane_four (S : (PureU1 4).Sols) (hS : LineInPlaneCond S.1.1) :
@ -124,10 +125,10 @@ lemma linesInPlane_four (S : (PureU1 4).Sols) (hS : LineInPlaneCond S.1.1) :
by_contra hn
have hLin := pureU1_linear S.1.1
have hcube := pureU1_cube S
simp at hLin hcube
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, PureU1_numberCharges] at hLin hcube
rw [Fin.sum_univ_four] at hLin hcube
rw [sq_eq_sq_iff_eq_or_eq_neg] at hn
simp [not_or] at hn
simp only [Fin.isValue, not_or] at hn
have l012 := hS 0 1 2 (ne_of_beq_false rfl) (ne_of_beq_false rfl) (ne_of_beq_false rfl)
have l013 := hS 0 1 3 (ne_of_beq_false rfl) (ne_of_beq_false rfl) (ne_of_beq_false rfl)
have l023 := hS 0 2 3 (ne_of_beq_false rfl) (ne_of_beq_false rfl) (ne_of_beq_false rfl)
@ -141,8 +142,9 @@ lemma linesInPlane_four (S : (PureU1 4).Sols) (hS : LineInPlaneCond S.1.1) :
rw [← h1, h3] at hcube
have h4 : S.val (2 : Fin 4) ^ 3 = 0 := by
linear_combination -1 * hcube / 24
simp at h4
simp_all
simp only [Fin.isValue, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff] at h4
simp_all only [neg_mul, neg_neg, add_left_eq_self, add_right_eq_self, not_true_eq_false,
false_and]
· by_cases h3 : S.val (0 : Fin 4) = - S.val (2 : Fin 4)
· simp_all
have h4 : S.val (1 : Fin 4) = - S.val (2 : Fin 4) := by
@ -174,7 +176,7 @@ lemma linesInPlane_constAbs_four (S : (PureU1 4).Sols)
intro i j
by_cases hij : i ≠ j
· exact linesInPlane_eq_sq_four hS i j hij
· simp at hij
· simp only [PureU1_numberCharges, ne_eq, Decidable.not_not] at hij
rw [hij]
theorem linesInPlane_constAbs_AF (S : (PureU1 (n.succ.succ.succ.succ)).Sols)

5
HepLean/AnomalyCancellation/PureU1/LowDim/One.lean
View file

@ -24,9 +24,10 @@ namespace One
theorem solEqZero (S : (PureU1 1).LinSols) : S = 0 := by
apply ACCSystemLinear.LinSols.ext
have hLin := pureU1_linear S
simp at hLin
simp only [succ_eq_add_one, reduceAdd, PureU1_numberCharges, univ_unique, Fin.default_eq_zero,
Fin.isValue, sum_singleton] at hLin
funext i
simp at i
simp only [PureU1_numberCharges] at i
rw [show i = (0 : Fin 1) from Fin.fin_one_eq_zero i]
exact hLin

4
HepLean/AnomalyCancellation/PureU1/LowDim/Three.lean
View file

@ -25,7 +25,7 @@ lemma cube_for_linSol' (S : (PureU1 3).LinSols) :
3 * S.val (0 : Fin 3) * S.val (1 : Fin 3) * S.val (2 : Fin 3) = 0 ↔
(PureU1 3).cubicACC S.val = 0 := by
have hL := pureU1_linear S
simp at hL
simp only [succ_eq_add_one, reduceAdd, PureU1_numberCharges] at hL
rw [Fin.sum_univ_three] at hL
change _ ↔ accCube _ _ = _
rw [accCube_explicit, Fin.sum_univ_three]
@ -47,7 +47,7 @@ lemma three_sol_zero (S : (PureU1 3).Sols) : S.val (0 : Fin 3) = 0 ∨ S.val (1
def solOfLinear (S : (PureU1 3).LinSols)
(hS : S.val (0 : Fin 3) = 0 ∨ S.val (1 : Fin 3) = 0 ∨ S.val (2 : Fin 3) = 0) :
(PureU1 3).Sols :=
⟨⟨S, by intro i; simp at i; exact Fin.elim0 i⟩,
⟨⟨S, fun i => Fin.elim0 i⟩,
(cube_for_linSol S).mp hS⟩
theorem solOfLinear_surjects (S : (PureU1 3).Sols) :

5
HepLean/AnomalyCancellation/PureU1/LowDim/Two.lean
View file

@ -23,9 +23,10 @@ namespace Two
/-- An equivalence between `LinSols` and `Sols`. -/
def equiv : (PureU1 2).LinSols ≃ (PureU1 2).Sols where
toFun S := ⟨⟨S, by intro i; simp at i; exact Fin.elim0 i⟩, by
toFun S := ⟨⟨S, fun i => Fin.elim0 i⟩, by
have hLin := pureU1_linear S
simp at hLin
simp only [succ_eq_add_one, reduceAdd, PureU1_numberCharges, Fin.sum_univ_two,
Fin.isValue] at hLin
erw [accCube_explicit]
simp only [Fin.sum_univ_two, Fin.isValue]
rw [show S.val (0 : Fin 2) = - S.val (1 : Fin 2) from eq_neg_of_add_eq_zero_left hLin]

4
HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
View file

@ -459,7 +459,7 @@ lemma P_accCube (f : Fin n → ℚ) : accCube (2 * n +1) (P f) = 0 := by
simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, Function.comp_apply, zero_add]
apply Finset.sum_eq_zero
intro i _
simp [P_δ₁, P_δ₂]
simp only [P_δ₁, P_δ₂]
ring
lemma P!_accCube (f : Fin n → ℚ) : accCube (2 * n +1) (P! f) = 0 := by
@ -514,7 +514,7 @@ lemma Pa_zero (f g : Fin n.succ → ℚ) (h : Pa f g = 0) :
change 0 = _ at h1
simp only [neg_zero, succ_eq_add_one, zero_sub, zero_eq_neg] at h1
have h2 := Pa_δa₂ f g ⟨iv, succ_lt_succ_iff.mp hiv⟩
simp [h, h1] at h2
simp only [succ_eq_add_one, h, Fin.succ_mk, Fin.castSucc_mk, h1, add_zero] at h2
exact h2.symm
exact hinduc i.val i.prop

4
HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
View file

@ -108,7 +108,7 @@ lemma P_P_P!_accCube' {S : (PureU1 (2 * n.succ.succ + 1)).LinSols}
have h4 := Pa_δa₄ f g 0
have h2 := Pa_δa₂ f g 0
rw [← hS] at h1 h2 h4
simp at h2
simp only [Nat.succ_eq_add_one, Fin.succ_zero_eq_one, Fin.castSucc_zero] at h2
have h5 : f 1 = S.val (δa₂ 0) + S.val δa₁ + S.val (δa₄ 0) := by
linear_combination -(1 * h1) - 1 * h4 - 1 * h2
rw [h5, δa₄_δ!₂, show (δa₂ (0 : Fin n.succ)) = δ!₁ 0 from rfl, δa₁_δ!₃]
@ -120,7 +120,7 @@ lemma lineInCubicPerm_last_cond {S : (PureU1 (2 * n.succ.succ+1)).LinSols}
obtain ⟨g, f, hfg⟩ := span_basis S
have h1 := lineInCubicPerm_swap LIC 0 g f hfg
rw [P_P_P!_accCube' g f hfg] at h1
simp at h1
simp only [Nat.succ_eq_add_one, mul_eq_zero] at h1
cases h1 <;> rename_i h1
· apply Or.inl
linear_combination h1