Merge pull request #248 from HEPLean/Add_more_Docs

refactor: Update naming for ACC Planes

HepLean/AnomalyCancellation/PureU1/Basic.lean

@@ -127,7 +127,7 @@ lemma pureU1_last {n : ℕ} (S : (PureU1 n.succ).LinSols) :
   rw [Fin.sum_univ_castSucc] at hS
   linear_combination hS
 
-/-- Two solutions to the Linear ACCs for `n.succ` areq equal if their first  `n` charges are
+/-- Two solutions to the Linear ACCs for `n.succ` areq equal if their first `n` charges are
   equal. -/
 lemma pureU1_anomalyFree_ext {n : ℕ} {S T : (PureU1 n.succ).LinSols}
     (h : ∀ (i : Fin n), S.val i.castSucc = T.val i.castSucc) : S = T := by
@@ -150,8 +150,7 @@ lemma sum_of_charges {n : ℕ} (f : Fin k → (PureU1 n).Charges) (j : Fin n) :
   · rfl
   · rename_i k hl
     rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
-    have hlt := hl (f ∘ Fin.castSucc)
-    erw [← hlt]
+    erw [← hl (f ∘ Fin.castSucc)]
     rfl
 
 /-- The `j`th charge of a sum of solutions to the linear ACC is equal to the sum of
@@ -162,8 +161,7 @@ lemma sum_of_anomaly_free_linear {n : ℕ} (f : Fin k → (PureU1 n).LinSols) (j
   · rfl
   · rename_i k hl
     rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
-    have hlt := hl (f ∘ Fin.castSucc)
-    erw [← hlt]
+    erw [← hl (f ∘ Fin.castSucc)]
     rfl
 
 end PureU1

HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean

@@ -91,36 +91,41 @@ lemma lineInCubicPerm_permute {S : (PureU1 (2 * n.succ)).LinSols}
 lemma lineInCubicPerm_swap {S : (PureU1 (2 * n.succ)).LinSols}
     (LIC : LineInCubicPerm S) :
     ∀ (j : Fin n) (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = Pa g f),
-      (S.val (δ!₂ j) - S.val (δ!₁ j))
+      (S.val (evenShiftSnd j) - S.val (evenShiftFst j))
       * accCubeTriLinSymm (P g) (P g) (basis!AsCharges j) = 0 := by
   intro j g f h
-  let S' := (FamilyPermutations (2 * n.succ)).linSolRep (pairSwap (δ!₁ j) (δ!₂ j)) S
-  have hSS' : ((FamilyPermutations (2 * n.succ)).linSolRep (pairSwap (δ!₁ j) (δ!₂ j))) S = S' := rfl
+  let S' := (FamilyPermutations (2 * n.succ)).linSolRep
+    (pairSwap (evenShiftFst j) (evenShiftSnd j)) S
+  have hSS' : ((FamilyPermutations (2 * n.succ)).linSolRep
+    (pairSwap (evenShiftFst j) (evenShiftSnd j))) S = S' := rfl
   obtain ⟨g', f', hall⟩ := span_basis_swap! j hSS' g f h
   have h1 := line_in_cubic_P_P_P! (lineInCubicPerm_self LIC) g f h
   have h2 := line_in_cubic_P_P_P!
-    (lineInCubicPerm_self (lineInCubicPerm_permute LIC (pairSwap (δ!₁ j) (δ!₂ j)))) g' f' hall.1
+    (lineInCubicPerm_self (lineInCubicPerm_permute LIC
+    (pairSwap (evenShiftFst j) (evenShiftSnd j)))) g' f' hall.1
   rw [hall.2.1, hall.2.2] at h2
   rw [accCubeTriLinSymm.map_add₃, h1, accCubeTriLinSymm.map_smul₃] at h2
   simpa using h2
 
 lemma P_P_P!_accCube' {S : (PureU1 (2 * n.succ.succ)).LinSols}
     (f : Fin n.succ.succ → ℚ) (g : Fin n.succ → ℚ) (hS : S.val = Pa f g) :
     accCubeTriLinSymm (P f) (P f) (basis!AsCharges (Fin.last n)) =
-    - (S.val (δ!₂ (Fin.last n)) + S.val (δ!₁ (Fin.last n))) * (2 * S.val δ!₄ +
-    S.val (δ!₂ (Fin.last n)) + S.val (δ!₁ (Fin.last n))) := by
+    - (S.val (evenShiftSnd (Fin.last n)) + S.val (evenShiftFst (Fin.last n))) *
+    (2 * S.val evenShiftLast +
+    S.val (evenShiftSnd (Fin.last n)) + S.val (evenShiftFst (Fin.last n))) := by
   rw [P_P_P!_accCube f (Fin.last n)]
-  have h1 := Pa_δ!₄ f g
-  have h2 := Pa_δ!₁ f g (Fin.last n)
-  have h3 := Pa_δ!₂ f g (Fin.last n)
+  have h1 := Pa_evenShiftLast f g
+  have h2 := Pa_evenShiftFst f g (Fin.last n)
+  have h3 := Pa_evenShiftSnd f g (Fin.last n)
   simp only [Fin.succ_last, Nat.succ_eq_add_one] at h1 h2 h3
-  have hl : f (Fin.succ (Fin.last n)) = - Pa f g δ!₄ := by
+  have hl : f (Fin.succ (Fin.last n)) = - Pa f g evenShiftLast := by
     simp_all only [Fin.succ_last, neg_neg]
   erw [hl] at h2
-  have hg : g (Fin.last n) = Pa f g (δ!₁ (Fin.last n)) + Pa f g δ!₄ := by
+  have hg : g (Fin.last n) = Pa f g (evenShiftFst (Fin.last n)) + Pa f g evenShiftLast := by
     linear_combination -(1 * h2)
   have hll : f (Fin.castSucc (Fin.last n)) =
-      - (Pa f g (δ!₂ (Fin.last n)) + Pa f g (δ!₁ (Fin.last n)) + Pa f g δ!₄) := by
+      - (Pa f g (evenShiftSnd (Fin.last n)) + Pa f g (evenShiftFst (Fin.last n))
+      + Pa f g evenShiftLast) := by
     linear_combination h3 - 1 * hg
   rw [← hS] at hl hll
   rw [hl, hll]
@@ -129,7 +134,8 @@ lemma P_P_P!_accCube' {S : (PureU1 (2 * n.succ.succ)).LinSols}
 lemma lineInCubicPerm_last_cond {S : (PureU1 (2 * n.succ.succ)).LinSols}
     (LIC : LineInCubicPerm S) :
     LineInPlaneProp
-    ((S.val (δ!₂ (Fin.last n))), ((S.val (δ!₁ (Fin.last n))), (S.val δ!₄))) := by
+    ((S.val (evenShiftSnd (Fin.last n))), ((S.val (evenShiftFst (Fin.last n))),
+      (S.val evenShiftLast))) := by
   obtain ⟨g, f, hfg⟩ := span_basis S
   have h1 := lineInCubicPerm_swap LIC (Fin.last n) g f hfg
   rw [P_P_P!_accCube' g f hfg] at h1
@@ -144,12 +150,14 @@ lemma lineInCubicPerm_last_cond {S : (PureU1 (2 * n.succ.succ)).LinSols}
 
 lemma lineInCubicPerm_last_perm {S : (PureU1 (2 * n.succ.succ)).LinSols}
     (LIC : LineInCubicPerm S) : LineInPlaneCond S := by
-  refine @Prop_three (2 * n.succ.succ) LineInPlaneProp S (δ!₂ (Fin.last n)) (δ!₁ (Fin.last n))
-    δ!₄ ?_ ?_ ?_ ?_
-  · simp [Fin.ext_iff, δ!₂, δ!₁]
-  · simp [Fin.ext_iff, δ!₂, δ!₄]
-  · simp only [Nat.succ_eq_add_one, δ!₁, δ!₄, Fin.isValue, ne_eq, Fin.ext_iff, Fin.coe_cast,
-    Fin.coe_natAdd, Fin.coe_castAdd, Fin.val_last, Fin.val_eq_zero, add_zero, add_right_inj]
+  refine @Prop_three (2 * n.succ.succ) LineInPlaneProp S
+    (evenShiftSnd (Fin.last n)) (evenShiftFst (Fin.last n))
+    evenShiftLast ?_ ?_ ?_ ?_
+  · simp [Fin.ext_iff, evenShiftSnd, evenShiftFst]
+  · simp [Fin.ext_iff, evenShiftSnd, evenShiftLast]
+  · simp only [Nat.succ_eq_add_one, evenShiftFst, evenShiftLast, Fin.isValue, ne_eq, Fin.ext_iff,
+    Fin.coe_cast, Fin.coe_natAdd, Fin.coe_castAdd, Fin.val_last, Fin.val_eq_zero, add_zero,
+    add_right_inj]
     omega
   · exact fun M => lineInCubicPerm_last_cond (lineInCubicPerm_permute LIC M)