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

refactor: replace some simp with exact

Browse source
This commit is contained in:
jstoobysmith 2024-08-30 10:43:29 -04:00
parent 167145acef
commit 81f3566be8
13 changed files with 82 additions and 102 deletions
Download patch file Download diff file Expand all files Collapse all files

18
HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
View file

@ -73,7 +73,7 @@ lemma linEqPropSol_iff_proj_linEqProp (R : MSSMACC.Sols) :
rw [α₁_proj, α₂_proj, h]
simp only [neg_zero, Fin.isValue, Fin.reduceFinMk, zero_mul, and_self]
· rw [h.2.2]
simp
exact Rat.mul_zero ((dot Y₃.val) B₃.val)
/-- A condition which is satisfied if the plane spanned by `R`, `Y₃` and `B₃` lies
entirely in the quadratic surface. -/
@ -119,7 +119,7 @@ lemma inQuadSolProp_iff_proj_inQuadProp (R : MSSMACC.Sols) :
simp only [Fin.isValue, Fin.reduceFinMk, mul_eq_zero,
OfNat.ofNat_ne_zero, or_self, false_or] at h
rw [h.2.1, h.2.2]
simp
exact Prod.mk_eq_zero.mp rfl
/-- A condition which is satisfied if the plane spanned by `R`, `Y₃` and `B₃` lies
entirely in the cubic surface. -/
@ -166,7 +166,7 @@ lemma inCubeSolProp_iff_proj_inCubeProp (R : MSSMACC.Sols) :
simp only [Fin.isValue, Fin.reduceFinMk, mul_eq_zero, OfNat.ofNat_ne_zero, ne_eq,
not_false_eq_true, pow_eq_zero_iff, or_self, false_or] at h
rw [h.2.1, h.2.2]
simp
exact Prod.mk_eq_zero.mp rfl
/-- Those charge assignments perpendicular to `Y₃` and `B₃` which satisfy the condition
`lineEqProp`. -/
@ -215,7 +215,7 @@ lemma toSolNSQuad_eq_planeY₃B₃_on_α (R : MSSMACC.AnomalyFreePerp) :
apply planeY₃B₃_eq
rw [α₁, α₂, α₃]
ring_nf
simp
exact ⟨trivial, trivial, trivial⟩
/-- Given an `R` perpendicular to `Y₃` and `B₃`, an element of `Sols`. This map is
not surjective. -/
@ -243,7 +243,7 @@ lemma toSolNS_proj (T : NotInLineEqSol) : toSolNS (toSolNSProj T.val) = T.val :=
rw [h1]
have h1 := (lineEqPropSol_iff_lineEqCoeff_zero T.val).mpr.mt T.prop
rw [← MulAction.mul_smul, mul_comm, mul_inv_cancel h1]
simp
exact MulAction.one_smul T.1.val
/-- A solution to the ACCs, given an element of `inLineEq × ℚ × ℚ × ℚ`. -/
def inLineEqToSol : InLineEq × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, c₁, c₂, c₃) =>
@ -286,7 +286,7 @@ lemma inLineEqToSol_proj (T : InLineEqSol) : inLineEqToSol (inLineEqProj T) = T.
rw [h1]
have h2 := (inQuadSolProp_iff_quadCoeff_zero T.val).mpr.mt T.prop.2
rw [← MulAction.mul_smul, mul_comm, mul_inv_cancel h2]
simp
exact MulAction.one_smul T.1.val
/-- Given an element of `inQuad × ℚ × ℚ × ℚ`, a solution to the ACCs. -/
def inQuadToSol : InQuad × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, a₁, a₂, a₃) =>
@ -331,7 +331,7 @@ lemma inQuadToSol_proj (T : InQuadSol) : inQuadToSol (inQuadProj T) = T.val := b
rw [h1]
have h2 := (inCubeSolProp_iff_cubicCoeff_zero T.val).mpr.mt T.prop.2.2
rw [← MulAction.mul_smul, mul_comm, mul_inv_cancel h2]
simp
exact MulAction.one_smul T.1.val
/-- Given a element of `inQuadCube × ℚ × ℚ × ℚ`, a solution to the ACCs. -/
def inQuadCubeToSol : InQuadCube × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, b₁, b₂, b₃) =>
@ -371,9 +371,9 @@ lemma inQuadCubeToSol_proj (T : InQuadCubeSol) :
ring_nf
simp only [Fin.isValue, Fin.reduceFinMk, zero_smul, add_zero, zero_add]
rw [← MulAction.mul_smul, mul_comm, mul_inv_cancel]
· simp only [one_smul]
· exact MulAction.one_smul (T.1).val
· rw [show dot Y₃.val B₃.val = 108 by rfl]
simp
exact Ne.symm (OfNat.zero_ne_ofNat 108)
/-- A solution from an element of `MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ`. We will
show that this map is a surjection. -/

12
HepLean/AnomalyCancellation/PureU1/Basic.lean
View file

@ -138,7 +138,7 @@ lemma pureU1_anomalyFree_ext {n : ℕ} {S T : (PureU1 n.succ).LinSols}
rw [hi, pureU1_last, pureU1_last]
simp only [neg_inj]
apply Finset.sum_congr
· simp only
· rfl
· exact fun j _ => h j
namespace PureU1
@ -146,23 +146,21 @@ namespace PureU1
lemma sum_of_charges {n : ℕ} (f : Fin k → (PureU1 n).Charges) (j : Fin n) :
(∑ i : Fin k, (f i)) j = ∑ i : Fin k, (f i) j := by
induction k
· simp only [univ_eq_empty, sum_empty]
rfl
· rfl
· rename_i k hl
rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
have hlt := hl (f ∘ Fin.castSucc)
erw [← hlt]
simp
rfl
lemma sum_of_anomaly_free_linear {n : ℕ} (f : Fin k → (PureU1 n).LinSols) (j : Fin n) :
(∑ i : Fin k, (f i)).1 j = (∑ i : Fin k, (f i).1 j) := by
induction k
· simp only [univ_eq_empty, sum_empty, ACCSystemLinear.linSolsAddCommMonoid_zero_val]
rfl
· rfl
· rename_i k hl
rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
have hlt := hl (f ∘ Fin.castSucc)
erw [← hlt]
simp
rfl
end PureU1

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

@ -61,7 +61,7 @@ lemma lt_eq {k i : Fin n.succ} (hk : S k ≤ 0) (hik : i ≤ k) : S i = S k := b
lemma val_le_zero {i : Fin n.succ} (hi : S i ≤ 0) : S i = S (0 : Fin n.succ) := by
symm
apply lt_eq hS hi
simp
exact Fin.zero_le i
lemma gt_eq {k i: Fin n.succ} (hk : 0 ≤ S k) (hik : k ≤ i) : S i = S k := by
have hSS := hS.2 k i hik
@ -73,8 +73,7 @@ lemma gt_eq {k i: Fin n.succ} (hk : 0 ≤ S k) (hik : k ≤ i) : S i = S k := by
lemma zero_gt (h0 : 0 ≤ S (0 : Fin n.succ)) (i : Fin n.succ) : S (0 : Fin n.succ) = S i := by
symm
refine gt_eq hS h0 ?_
simp
refine gt_eq hS h0 (Fin.zero_le i)
lemma opposite_signs_eq_neg {i j : Fin n.succ} (hi : S i ≤ 0) (hj : 0 ≤ S j) : S i = - S j := by
have hSS := hS.1 i j
@ -98,7 +97,7 @@ is defined as a element of `k ∈ Fin n` such that `S k.castSucc` and `S k.succ`
def Boundary (S : (PureU1 n.succ).Charges) (k : Fin n) : Prop := S k.castSucc < 0 ∧ 0 < S k.succ
lemma boundary_castSucc {k : Fin n} (hk : Boundary S k) : S k.castSucc = S (0 : Fin n.succ) :=
(lt_eq hS (le_of_lt hk.left) (by simp : 0 ≤ k.castSucc)).symm
(lt_eq hS (le_of_lt hk.left) (Fin.zero_le k.castSucc : 0 ≤ k.castSucc)).symm
lemma boundary_succ {k : Fin n} (hk : Boundary S k) : S k.succ = - S (0 : Fin n.succ) := by
have hn := boundary_castSucc hS hk
@ -114,8 +113,7 @@ lemma boundary_accGrav' (k : Fin n) : accGrav n.succ S =
erw [Finset.sum_equiv (Fin.castOrderIso (boundary_split k)).toEquiv]
· intro i
simp only [Fin.val_succ, mem_univ, RelIso.coe_fn_toEquiv]
· intro i
simp
· exact fun _ _ => rfl
lemma boundary_accGrav'' (k : Fin n) (hk : Boundary S k) :
accGrav n.succ S = (2 * ↑↑k + 1 - ↑n) * S (0 : Fin n.succ) := by
@ -126,7 +124,7 @@ lemma boundary_accGrav'' (k : Fin n) (hk : Boundary S k) :
apply lt_eq hS (le_of_lt hk.left) (by rw [Fin.le_def]; simp; omega)
have hsnd (i : Fin (n.succ - k.succ.val)) :
S (Fin.cast (boundary_split k) (Fin.natAdd (k.succ.val) i)) = S k.succ := by
apply gt_eq hS (le_of_lt hk.right) (by rw [Fin.le_def]; simp)
apply gt_eq hS (le_of_lt hk.right) (by rw [Fin.le_def]; exact le.intro rfl)
simp only [hfst, hsnd]
simp only [Fin.val_succ, sum_const, card_fin, nsmul_eq_mul, cast_add, cast_one,
succ_sub_succ_eq_sub, Fin.is_le', cast_sub]
@ -145,7 +143,7 @@ lemma not_hasBoundary_zero_le (hnot : ¬ (HasBoundary S)) (h0 : S (0 : Fin n.suc
induction i
· rfl
· rename_i i hii
have hnott := hnot ⟨i, by {simp at hi; linarith}⟩
have hnott := hnot ⟨i, succ_lt_succ_iff.mp hi⟩
have hii := hii (by omega)
erw [← hii] at hnott
exact (val_le_zero hS (hnott h0)).symm
@ -265,7 +263,7 @@ theorem boundary_value_even (S : (PureU1 (2 * n.succ)).LinSols) (hs : ConstAbs S
have h2 := ConstAbsSorted.AFL_even_above (sortAFL S) hS
rw [sortAFL_val] at h1 h2
rw [h1, h2]
simp
exact (InvolutiveNeg.neg_neg (sort S.val _)).symm
end ConstAbs

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

@ -56,8 +56,7 @@ lemma ext_δ (S T : Fin (2 * n.succ) → ℚ) (h1 : ∀ i, S (δ₁ i) = T (δ
by_cases hi : i.val < n.succ
· let j : Fin n.succ := ⟨i, hi⟩
have h2 := h1 j
have h3 : δ₁ j = i := by
simp [δ₁, Fin.ext_iff]
have h3 : δ₁ j = i := rfl
rw [h3] at h2
exact h2
· let j : Fin n.succ := ⟨i - n.succ, by omega⟩
@ -74,8 +73,7 @@ lemma sum_δ₁_δ₂ (S : Fin (2 * n.succ) → ℚ) :
rw [Finset.sum_equiv (Fin.castOrderIso (split_equal n.succ)).symm.toEquiv]
intro i
simp only [mem_univ, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv]
intro i
simp
exact fun _ _=> rfl
rw [h1]
rw [Fin.sum_univ_add, Finset.sum_add_distrib]
rfl
@ -86,8 +84,7 @@ lemma sum_δ₁_δ₂' (S : Fin (2 * n.succ) → ℚ) :
rw [Finset.sum_equiv (Fin.castOrderIso (split_equal n.succ)).symm.toEquiv]
intro i
simp only [mem_univ, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv]
intro i
simp
exact fun _ _ => rfl
rw [h1]
rw [Fin.sum_univ_add, Finset.sum_add_distrib]
rfl
@ -98,8 +95,7 @@ lemma sum_δ!₁_δ!₂ (S : Fin (2 * n.succ) → ℚ) :
rw [Finset.sum_equiv (Fin.castOrderIso (n_cond₂ n)).symm.toEquiv]
intro i
simp only [mem_univ, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv]
intro i
simp
exact fun _ _ => rfl
rw [h1]
rw [Fin.sum_univ_add, Fin.sum_univ_add, Fin.sum_univ_add, Finset.sum_add_distrib]
simp only [univ_unique, Fin.default_eq_zero, Fin.isValue, sum_singleton, Function.comp_apply]
@ -367,10 +363,10 @@ lemma P_δ₁ (f : Fin n.succ → ℚ) (j : Fin n.succ) : P f (δ₁ j) = f j :=
simp [HSMul.hSMul, SMul.smul]
rw [Finset.sum_eq_single j]
· rw [basis_on_δ₁_self]
simp only [mul_one]
exact Rat.mul_one (f j)
· intro k _ hkj
rw [basis_on_δ₁_other hkj]
simp only [mul_zero]
exact Rat.mul_zero (f k)
· simp only [mem_univ, not_true_eq_false, _root_.mul_eq_zero, IsEmpty.forall_iff]
lemma P!_δ!₁ (f : Fin n → ℚ) (j : Fin n) : P! f (δ!₁ j) = f j := by
@ -378,10 +374,10 @@ lemma P!_δ!₁ (f : Fin n → ℚ) (j : Fin n) : P! f (δ!₁ j) = f j := by
simp [HSMul.hSMul, SMul.smul]
rw [Finset.sum_eq_single j]
· rw [basis!_on_δ!₁_self]
simp only [mul_one]
exact Rat.mul_one (f j)
· intro k _ hkj
rw [basis!_on_δ!₁_other hkj]
simp only [mul_zero]
exact Rat.mul_zero (f k)
· simp only [mem_univ, not_true_eq_false, _root_.mul_eq_zero, IsEmpty.forall_iff]
lemma Pa_δ!₁ (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (j : Fin n) :
@ -404,10 +400,10 @@ lemma P!_δ!₂ (f : Fin n → ℚ) (j : Fin n) : P! f (δ!₂ j) = - f j := by
simp [HSMul.hSMul, SMul.smul]
rw [Finset.sum_eq_single j]
· rw [basis!_on_δ!₂_self]
simp only [mul_neg, mul_one]
exact mul_neg_one (f j)
· intro k _ hkj
rw [basis!_on_δ!₂_other hkj]
simp only [mul_zero]
exact Rat.mul_zero (f k)
· simp
lemma Pa_δ!₂ (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (j : Fin n) :
@ -425,7 +421,7 @@ lemma Pa_δ!₃ (f : Fin n.succ → ℚ) (g : Fin n → ℚ) : Pa f g (δ!₃) =
rw [Pa]
simp only [ACCSystemCharges.chargesAddCommMonoid_add]
rw [P!_δ!₃, δ!₃_δ₁0, P_δ₁]
simp
exact Rat.add_zero (f 0)
lemma P!_δ!₄ (f : Fin n → ℚ) : P! f (δ!₄) = 0 := by
rw [P!, sum_of_charges]
@ -435,7 +431,7 @@ lemma Pa_δ!₄ (f : Fin n.succ → ℚ) (g : Fin n → ℚ) : Pa f g (δ!₄) =
rw [Pa]
simp only [ACCSystemCharges.chargesAddCommMonoid_add]
rw [P!_δ!₄, δ!₄_δ₂Last, P_δ₂]
simp
exact Rat.add_zero (-f (Fin.last n))
lemma P_δ₁_δ₂ (f : Fin n.succ → ℚ) : P f ∘ δ₂ = - P f ∘ δ₁ := by
funext j
@ -525,8 +521,7 @@ lemma Pa_zero (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (h : Pa f g = 0) :
change 0 = _ at h2
simp at h2
rw [h2] at h1
simp at h1
exact h1.symm
exact self_eq_add_left.mp h1
exact hinduc i.val i.prop
lemma Pa_zero! (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (h : Pa f g = 0) :
@ -554,13 +549,13 @@ lemma P'_val (f : Fin n.succ → ℚ) : (P' f).val = P f := by
simp [P', P]
funext i
rw [sum_of_anomaly_free_linear, sum_of_charges]
simp [HSMul.hSMul]
rfl
lemma P!'_val (f : Fin n → ℚ) : (P!' f).val = P! f := by
simp [P!', P!]
funext i
rw [sum_of_anomaly_free_linear, sum_of_charges]
simp [HSMul.hSMul]
rfl
theorem basis_linear_independent : LinearIndependent ℚ (@basis n) := by
apply Fintype.linearIndependent_iff.mpr

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

@ -124,9 +124,9 @@ lemma linesInPlane_four (S : (PureU1 4).Sols) (hS : LineInPlaneCond S.1.1) :
rw [Fin.sum_univ_four] at hLin hcube
rw [sq_eq_sq_iff_eq_or_eq_neg] at hn
simp [not_or] at hn
have l012 := hS 0 1 2 (by simp) (by simp) (by simp)
have l013 := hS 0 1 3 (by simp) (by simp) (by simp)
have l023 := hS 0 2 3 (by simp) (by simp) (by simp)
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)
simp_all [LineInPlaneProp]
have h1 : S.val (2 : Fin 4) = S.val (3 : Fin 4) := by
linear_combination l012 / 2 + -1 * l013 / 2
@ -158,7 +158,7 @@ lemma linesInPlane_four (S : (PureU1 4).Sols) (hS : LineInPlaneCond S.1.1) :
lemma linesInPlane_eq_sq_four {S : (PureU1 4).Sols}
(hS : LineInPlaneCond S.1.1) : ∀ (i j : Fin 4) (_ : i ≠ j),
ConstAbsProp (S.val i, S.val j) := by
refine Prop_two ConstAbsProp (by simp : (0 : Fin 4) ≠ 1) ?_
refine Prop_two ConstAbsProp Fin.zero_ne_one ?_
intro M
let S' := (FamilyPermutations 4).solAction.toFun S M
have hS' : LineInPlaneCond S'.1.1 :=

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

@ -86,7 +86,7 @@ lemma δa₂_δ₁ (j : Fin n) : δa₂ j = δ₁ j.succ := by
lemma δa₂_δ!₁ (j : Fin n) : δa₂ j = δ!₁ j.castSucc := by
rw [Fin.ext_iff]
simp [δa₂, δ!₁]
rfl
lemma δa₃_δ₃ : @δa₃ n = δ₃ := by
rw [Fin.ext_iff]
@ -103,8 +103,7 @@ lemma δa₄_δ₂ (j : Fin n.succ) : δa₄ j = δ₂ j := by
lemma δa₄_δ!₂ (j : Fin n.succ) : δa₄ j = δ!₂ j := by
rw [Fin.ext_iff]
simp [δa₄, δ!₂]
omega
rfl
lemma δ₂_δ!₂ (j : Fin n) : δ₂ j = δ!₂ j := by
rw [Fin.ext_iff]
@ -117,8 +116,7 @@ lemma sum_δ (S : Fin (2 * n + 1) → ℚ) :
rw [Finset.sum_equiv (Fin.castOrderIso (split_odd n)).symm.toEquiv]
intro i
simp only [mem_univ, Fin.symm_castOrderIso, RelIso.coe_fn_toEquiv]
intro i
simp
exact fun _ _ => rfl
rw [h1]
rw [Fin.sum_univ_add, Fin.sum_univ_add]
simp only [univ_unique, Fin.default_eq_zero, Fin.isValue, sum_singleton, Function.comp_apply]
@ -133,8 +131,7 @@ lemma sum_δ! (S : Fin (2 * n + 1) → ℚ) :
rw [Finset.sum_equiv (Fin.castOrderIso (split_odd! n)).symm.toEquiv]
intro i
simp only [mem_univ, Fin.castOrderIso, RelIso.coe_fn_toEquiv]
intro i
simp
exact fun _ _ => rfl
rw [h1]
rw [Fin.sum_univ_add, Fin.sum_univ_add]
simp only [univ_unique, Fin.default_eq_zero, Fin.isValue, sum_singleton, Function.comp_apply]
@ -363,10 +360,10 @@ lemma P_δ₁ (f : Fin n → ℚ) (j : Fin n) : P f (δ₁ j) = f j := by
simp [HSMul.hSMul, SMul.smul]
rw [Finset.sum_eq_single j]
· rw [basis_on_δ₁_self]
simp only [mul_one]
exact Rat.mul_one (f j)
· intro k _ hkj
rw [basis_on_δ₁_other hkj]
simp only [mul_zero]
exact Rat.mul_zero (f k)
· simp only [mem_univ, not_true_eq_false, _root_.mul_eq_zero, IsEmpty.forall_iff]
lemma P!_δ!₁ (f : Fin n → ℚ) (j : Fin n) : P! f (δ!₁ j) = f j := by
@ -374,10 +371,10 @@ lemma P!_δ!₁ (f : Fin n → ℚ) (j : Fin n) : P! f (δ!₁ j) = f j := by
simp [HSMul.hSMul, SMul.smul]
rw [Finset.sum_eq_single j]
· rw [basis!_on_δ!₁_self]
simp only [mul_one]
exact Rat.mul_one (f j)
· intro k _ hkj
rw [basis!_on_δ!₁_other hkj]
simp only [mul_zero]
exact Rat.mul_zero (f k)
· simp only [mem_univ, not_true_eq_false, _root_.mul_eq_zero, IsEmpty.forall_iff]
lemma P_δ₂ (f : Fin n → ℚ) (j : Fin n) : P f (δ₂ j) = - f j := by
@ -385,10 +382,10 @@ lemma P_δ₂ (f : Fin n → ℚ) (j : Fin n) : P f (δ₂ j) = - f j := by
simp [HSMul.hSMul, SMul.smul]
rw [Finset.sum_eq_single j]
· rw [basis_on_δ₂_self]
simp only [mul_neg, mul_one]
exact mul_neg_one (f j)
· intro k _ hkj
rw [basis_on_δ₂_other hkj]
simp only [mul_zero]
exact Rat.mul_zero (f k)
· simp
lemma P!_δ!₂ (f : Fin n → ℚ) (j : Fin n) : P! f (δ!₂ j) = - f j := by
@ -396,10 +393,10 @@ lemma P!_δ!₂ (f : Fin n → ℚ) (j : Fin n) : P! f (δ!₂ j) = - f j := by
simp [HSMul.hSMul, SMul.smul]
rw [Finset.sum_eq_single j]
· rw [basis!_on_δ!₂_self]
simp only [mul_neg, mul_one]
exact mul_neg_one (f j)
· intro k _ hkj
rw [basis!_on_δ!₂_other hkj]
simp only [mul_zero]
exact Rat.mul_zero (f k)
· simp
lemma P_δ₃ (f : Fin n → ℚ) : P f (δ₃) = 0 := by
@ -416,7 +413,7 @@ lemma Pa_δa₁ (f g : Fin n.succ → ℚ) : Pa f g δa₁ = f 0 := by
nth_rewrite 1 [δa₁_δ₁]
rw [δa₁_δ!₃]
rw [P_δ₁, P!_δ!₃]
simp
exact Rat.add_zero (f 0)
lemma Pa_δa₂ (f g : Fin n.succ → ℚ) (j : Fin n) : Pa f g (δa₂ j) = f j.succ + g j.castSucc := by
rw [Pa]
@ -431,7 +428,7 @@ lemma Pa_δa₃ (f g : Fin n.succ → ℚ) : Pa f g (δa₃) = g (Fin.last n) :=
nth_rewrite 1 [δa₃_δ₃]
rw [δa₃_δ!₁]
rw [P_δ₃, P!_δ!₁]
simp
exact Rat.zero_add (g (Fin.last n))
lemma Pa_δa₄ (f g : Fin n.succ → ℚ) (j : Fin n.succ) : Pa f g (δa₄ j) = - f j - g j := by
rw [Pa]
@ -542,21 +539,22 @@ lemma P'_val (f : Fin n → ℚ) : (P' f).val = P f := by
simp [P', P]
funext i
rw [sum_of_anomaly_free_linear, sum_of_charges]
simp [HSMul.hSMul]
rfl
lemma P!'_val (f : Fin n → ℚ) : (P!' f).val = P! f := by
simp [P!', P!]
funext i
rw [sum_of_anomaly_free_linear, sum_of_charges]
simp [HSMul.hSMul]
rfl
theorem basis_linear_independent : LinearIndependent ℚ (@basis n) := by
apply Fintype.linearIndependent_iff.mpr
intro f h
change P' f = 0 at h
have h1 : (P' f).val = 0 := by
simp [h]
rfl
have h1 : (P' f).val = 0 :=
(AddSemiconjBy.eq_zero_iff (ACCSystemLinear.LinSols.val 0)
(congrFun (congrArg HAdd.hAdd (congrArg ACCSystemLinear.LinSols.val (id (Eq.symm h))))
(ACCSystemLinear.LinSols.val 0))).mp rfl
rw [P'_val] at h1
exact P_zero f h1
@ -564,9 +562,10 @@ theorem basis!_linear_independent : LinearIndependent ℚ (@basis! n) := by
apply Fintype.linearIndependent_iff.mpr
intro f h
change P!' f = 0 at h
have h1 : (P!' f).val = 0 := by
simp [h]
rfl
have h1 : (P!' f).val = 0 :=
(AddSemiconjBy.eq_zero_iff (ACCSystemLinear.LinSols.val 0)
(congrFun (congrArg HAdd.hAdd (congrArg ACCSystemLinear.LinSols.val (id (Eq.symm h))))
(ACCSystemLinear.LinSols.val 0))).mp rfl
rw [P!'_val] at h1
exact P!_zero f h1
@ -574,9 +573,10 @@ theorem basisa_linear_independent : LinearIndependent ℚ (@basisa n.succ) := by
apply Fintype.linearIndependent_iff.mpr
intro f h
change Pa' f = 0 at h
have h1 : (Pa' f).val = 0 := by
simp [h]
rfl
have h1 : (Pa' f).val = 0 :=
(AddSemiconjBy.eq_zero_iff (ACCSystemLinear.LinSols.val 0)
(congrFun (congrArg HAdd.hAdd (congrArg ACCSystemLinear.LinSols.val (id (Eq.symm h))))
(ACCSystemLinear.LinSols.val 0))).mp rfl
rw [Pa'_P'_P!'] at h1
change (P' (f ∘ Sum.inl)).val + (P!' (f ∘ Sum.inr)).val = 0 at h1
rw [P!'_val, P'_val] at h1

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

@ -73,15 +73,8 @@ lemma lineInCubicPerm_self {S : (PureU1 (2 * n + 1)).LinSols} (hS : LineInCubicP
/-- If `lineInCubicPerm S`, then `lineInCubicPerm (M S)` for all permutations `M`. -/
lemma lineInCubicPerm_permute {S : (PureU1 (2 * n + 1)).LinSols}
(hS : LineInCubicPerm S) (M' : (FamilyPermutations (2 * n + 1)).group) :
LineInCubicPerm ((FamilyPermutations (2 * n + 1)).linSolRep M' S) := by
rw [LineInCubicPerm]
intro M
have ht : ((FamilyPermutations (2 * n + 1)).linSolRep M)
((FamilyPermutations (2 * n + 1)).linSolRep M' S)
= (FamilyPermutations (2 * n + 1)).linSolRep (M * M') S := by
simp [(FamilyPermutations (2 * n.succ)).linSolRep.map_mul']
rw [ht]
exact hS (M * M')
LineInCubicPerm ((FamilyPermutations (2 * n + 1)).linSolRep M' S) :=
fun M => hS (M * M')
lemma lineInCubicPerm_swap {S : (PureU1 (2 * n.succ + 1)).LinSols}
(LIC : LineInCubicPerm S) :
@ -108,10 +101,7 @@ lemma P_P_P!_accCube' {S : (PureU1 (2 * n.succ.succ + 1)).LinSols}
rw [P_P_P!_accCube f 0]
rw [← Pa_δa₁ f g]
rw [← hS]
have ht : δ!₁ (0 : Fin n.succ.succ) = δ₁ 1 := by
simp [δ!₁, δ₁]
rw [Fin.ext_iff]
simp
have ht : δ!₁ (0 : Fin n.succ.succ) = δ₁ 1 := rfl
nth_rewrite 1 [ht]
rw [P_δ₁]
have h1 := Pa_δa₁ f g
@ -125,7 +115,7 @@ lemma P_P_P!_accCube' {S : (PureU1 (2 * n.succ.succ + 1)).LinSols}
rw [δa₄_δ!₂]
have h0 : (δa₂ (0 : Fin n.succ)) = δ!₁ 0 := by
rw [δa₂_δ!₁]
simp
exact ht
rw [h0, δa₁_δ!₃]
ring
@ -149,9 +139,9 @@ lemma lineInCubicPerm_last_perm {S : (PureU1 (2 * n.succ.succ + 1)).LinSols}
(LIC : LineInCubicPerm S) : LineInPlaneCond S := by
refine @Prop_three (2 * n.succ.succ + 1) LineInPlaneProp S (δ!₂ 0) (δ!₁ 0)
δ!₃ ?_ ?_ ?_ ?_
· simp [Fin.ext_iff, δ!₂, δ!₁]
· simp [Fin.ext_iff, δ!₂, δ!₃]
· simp [Fin.ext_iff, δ!₁, δ!₃]
· exact ne_of_beq_false rfl
· exact ne_of_beq_false rfl
· exact ne_of_beq_false rfl
· exact fun M => lineInCubicPerm_last_cond (lineInCubicPerm_permute LIC M)
lemma lineInCubicPerm_constAbs {S : (PureU1 (2 * n.succ.succ + 1)).LinSols}

1
HepLean/AnomalyCancellation/SM/FamilyMaps.lean
View file

@ -44,7 +44,6 @@ def speciesFamilyProj {m n : ℕ} (h : n ≤ m) :
toFun S := S ∘ Fin.castLE h
map_add' _ _ := rfl
map_smul' _ _ := rfl
--rw [show Rat.cast a = a from rfl]
/-- The projection of the `m`-family charges onto the first `n`-family charges. -/
def familyProjection {m n : ℕ} (h : n ≤ m) : (SMCharges m).Charges →ₗ[ℚ] (SMCharges n).Charges :=

2
HepLean/AnomalyCancellation/SMNu/Basic.lean
View file

@ -56,7 +56,7 @@ lemma toSMSpecies_toSpecies_inv (i : Fin 6) (f : Fin 6 → Fin n → ℚ) :
simp
lemma toSpecies_one (S : (SMνCharges 1).Charges) (j : Fin 6) :
toSpecies j S ⟨0, by simp⟩ = S j := by
toSpecies j S ⟨0, zero_lt_succ 0⟩ = S j := by
match j with
| 0 => rfl
| 1 => rfl

2
HepLean/AnomalyCancellation/SMNu/FamilyMaps.lean
View file

@ -141,7 +141,7 @@ lemma sum_familyUniversal_three {n : ℕ} (S : (SMνCharges 1).Charges)
simp only [SMνSpecies_numberCharges, toSpecies_apply, Fin.zero_eta, Fin.isValue]
rw [Finset.mul_sum]
apply Finset.sum_congr
· simp only
· rfl
· intro i _
erw [toSpecies_familyUniversal]
simp only [SMνSpecies_numberCharges, Fin.zero_eta, Fin.isValue, toSpecies_apply]

6
HepLean/AnomalyCancellation/SMNu/Ordinary/DimSevenPlane.lean
View file

@ -279,7 +279,7 @@ lemma B_sum_is_sol (f : Fin 7 → ℚ) : (SM 3).IsSolution (∑ i, f i • B i)
have h : accGrav (B i) = 0 := by
fin_cases i <;> rfl
rw [h]
simp)
exact DistribMulAction.smul_zero (f i))
(by
rw [map_sum]
apply Fintype.sum_eq_zero
@ -288,7 +288,7 @@ lemma B_sum_is_sol (f : Fin 7 → ℚ) : (SM 3).IsSolution (∑ i, f i • B i)
have h : accSU2 (B i) = 0 := by
fin_cases i <;> rfl
rw [h]
simp)
exact DistribMulAction.smul_zero (f i))
(by
rw [map_sum]
apply Fintype.sum_eq_zero
@ -297,7 +297,7 @@ lemma B_sum_is_sol (f : Fin 7 → ℚ) : (SM 3).IsSolution (∑ i, f i • B i)
have h : accSU3 (B i) = 0 := by
fin_cases i <;> rfl
rw [h]
simp)
exact DistribMulAction.smul_zero (f i))
(B_in_accCube f)
use X
rfl

2
HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean
View file

@ -80,7 +80,7 @@ lemma add_AFL_quad (S : (PlusU1 n).LinSols) (a b : ℚ) :
lemma add_quad (S : (PlusU1 n).QuadSols) (a b : ℚ) :
accQuad (a • S.val + b • (BL n).val) = 0 := by
rw [add_AFL_quad, quadSol S]
simp
exact Rat.mul_zero (a ^ 2)
/-- The `QuadSol` obtained by adding $B-L$ to a `QuadSol`. -/
def addQuad (S : (PlusU1 n).QuadSols) (a b : ℚ) : (PlusU1 n).QuadSols :=

2
HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean
View file

@ -106,7 +106,7 @@ lemma quadSolToSolInv_1 (S : (PlusU1 n).Sols) :
lemma quadSolToSolInv_α₁_α₂_zero (S : (PlusU1 n).Sols) (h : α₁ S.1 = 0) :
α₁ (quadSolToSolInv S).1 = 0 ∧ α₂ (quadSolToSolInv S).1 = 0 := by
rw [quadSolToSolInv_1, α₂_AF S, h]
simp
exact Prod.mk_eq_zero.mp rfl
lemma quadSolToSolInv_α₁_α₂_neq_zero (S : (PlusU1 n).Sols) (h : α₁ S.1 ≠ 0) :
¬ (α₁ (quadSolToSolInv S).1 = 0 ∧ α₂ (quadSolToSolInv S).1 = 0) := by