Merge pull request #10 from HEPLean/AnomalyCancellation/PureU1

feat: Pure U(1)

HepLean.lean

@@ -10,6 +10,22 @@ import HepLean.AnomalyCancellation.MSSMNu.Permutations
 import HepLean.AnomalyCancellation.MSSMNu.PlaneY3B3Orthog
 import HepLean.AnomalyCancellation.MSSMNu.SolsParameterization
 import HepLean.AnomalyCancellation.MSSMNu.Y3
+import HepLean.AnomalyCancellation.PureU1.Basic
+import HepLean.AnomalyCancellation.PureU1.BasisLinear
+import HepLean.AnomalyCancellation.PureU1.ConstAbs
+import HepLean.AnomalyCancellation.PureU1.Even.BasisLinear
+import HepLean.AnomalyCancellation.PureU1.Even.LineInCubic
+import HepLean.AnomalyCancellation.PureU1.Even.Parameterization
+import HepLean.AnomalyCancellation.PureU1.LineInPlaneCond
+import HepLean.AnomalyCancellation.PureU1.LowDim.One
+import HepLean.AnomalyCancellation.PureU1.LowDim.Three
+import HepLean.AnomalyCancellation.PureU1.LowDim.Two
+import HepLean.AnomalyCancellation.PureU1.Odd.BasisLinear
+import HepLean.AnomalyCancellation.PureU1.Odd.LineInCubic
+import HepLean.AnomalyCancellation.PureU1.Odd.Parameterization
+import HepLean.AnomalyCancellation.PureU1.Permutations
+import HepLean.AnomalyCancellation.PureU1.Sort
+import HepLean.AnomalyCancellation.PureU1.VectorLike
 import HepLean.AnomalyCancellation.SM.Basic
 import HepLean.AnomalyCancellation.SM.FamilyMaps
 import HepLean.AnomalyCancellation.SM.NoGrav.Basic

HepLean/AnomalyCancellation/PureU1/Basic.lean

@@ -0,0 +1,184 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.AnomalyCancellation.Basic
+import Mathlib.Algebra.Module.Equiv
+import Mathlib.Algebra.BigOperators.Ring
+import Mathlib.Algebra.BigOperators.Fin
+/-!
+# Pure U(1) ACC system.
+
+We define the anomaly cancellation conditions for a pure U(1) gague theory with `n` fermions.
+
+-/
+universe v u
+open Nat
+
+
+open  Finset
+
+namespace PureU1
+open BigOperators
+
+/-- The vector space of charges. -/
+@[simps!]
+def PureU1Charges (n : ℕ) : ACCSystemCharges := ACCSystemChargesMk n
+
+open BigOperators in
+/-- The gravitational anomaly. -/
+def accGrav (n : ℕ) : ((PureU1Charges n).charges →ₗ[ℚ] ℚ) where
+  toFun S := ∑ i : Fin n, S i
+  map_add' S T := Finset.sum_add_distrib
+  map_smul' a S := by
+   simp [HSMul.hSMul, SMul.smul]
+   rw [← Finset.mul_sum]
+
+
+/-- The symmetric trilinear form used to define the cubic anomaly. -/
+@[simps!]
+def accCubeTriLinSymm {n : ℕ} : TriLinearSymm (PureU1Charges n).charges where
+  toFun S := ∑ i, S.1 i * S.2.1 i * S.2.2 i
+  map_smul₁' a S L T := by
+    simp [HSMul.hSMul]
+    rw [Finset.mul_sum]
+    apply Fintype.sum_congr
+    intro i
+    ring
+  map_add₁' S L T R := by
+    simp only [PureU1Charges_numberCharges, ACCSystemCharges.chargesAddCommMonoid_add]
+    rw [← Finset.sum_add_distrib]
+    apply Fintype.sum_congr
+    intro i
+    ring
+  swap₁' S L T := by
+    simp only [PureU1Charges_numberCharges]
+    apply Fintype.sum_congr
+    intro i
+    ring
+  swap₂' S L T := by
+    simp only [PureU1Charges_numberCharges]
+    apply Fintype.sum_congr
+    intro i
+    ring
+
+lemma accCubeTriLinSymm_cast {n m : ℕ} (h : m = n)
+    (S :  (PureU1Charges n).charges × (PureU1Charges n).charges × (PureU1Charges n).charges) :
+    accCubeTriLinSymm S = ∑ i : Fin m,
+      S.1 (Fin.cast h i) * S.2.1 (Fin.cast h i) * S.2.2 (Fin.cast h i) := by
+  rw [← accCubeTriLinSymm.toFun_eq_coe, accCubeTriLinSymm]
+  simp only [PureU1Charges_numberCharges]
+  rw [Finset.sum_equiv (Fin.castIso h).symm.toEquiv]
+  intro i
+  simp only [mem_univ, Fin.symm_castIso, RelIso.coe_fn_toEquiv, Fin.castIso_apply]
+  intro i
+  simp
+
+/-- The cubic anomaly equation. -/
+@[simp]
+def accCube (n : ℕ)  : HomogeneousCubic ((PureU1Charges n).charges) :=
+  (accCubeTriLinSymm).toCubic
+
+
+lemma accCube_explicit (n : ℕ) (S : (PureU1Charges n).charges) :
+    accCube n S = ∑ i : Fin n, S i ^ 3:= by
+  rw [accCube, TriLinearSymm.toCubic]
+  change  accCubeTriLinSymm.toFun (S, S, S) = _
+  rw [accCubeTriLinSymm]
+  simp only [PureU1Charges_numberCharges]
+  apply Finset.sum_congr
+  simp only
+  ring_nf
+  simp
+
+end PureU1
+
+/-- The ACC system for a pure $U(1)$ gauge theory with $n$ fermions. -/
+@[simps!]
+def PureU1 (n : ℕ) : ACCSystem where
+  numberLinear := 1
+  linearACCs := fun i =>
+    match i with
+    | 0 => PureU1.accGrav n
+  numberQuadratic := 0
+  quadraticACCs := Fin.elim0
+  cubicACC := PureU1.accCube n
+
+/-- An equivalence of vector spaces of charges when the number of fermions is equal. -/
+def pureU1EqCharges {n m : ℕ} (h : n = m):
+    (PureU1 n).charges  ≃ₗ[ℚ] (PureU1 m).charges where
+  toFun f := f ∘ Fin.cast h.symm
+  invFun f := f ∘ Fin.cast h
+  map_add' _ _ := rfl
+  map_smul' _ _:= rfl
+  left_inv _ := rfl
+  right_inv _ := rfl
+
+open BigOperators
+
+lemma pureU1_linear {n : ℕ} (S : (PureU1 n.succ).LinSols) :
+    ∑ i, S.val i = 0 := by
+  have hS := S.linearSol
+  simp at hS
+  exact hS 0
+
+lemma pureU1_cube {n : ℕ} (S : (PureU1 n.succ).Sols) :
+    ∑ i, (S.val i) ^ 3 = 0 := by
+  have hS := S.cubicSol
+  erw [PureU1.accCube_explicit] at hS
+  exact hS
+
+lemma pureU1_last {n : ℕ} (S : (PureU1 n.succ).LinSols) :
+    S.val (Fin.last n) = - ∑ i : Fin n, S.val i.castSucc := by
+  have hS := pureU1_linear S
+  simp at hS
+  rw [Fin.sum_univ_castSucc] at hS
+  linear_combination hS
+
+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
+  apply ACCSystemLinear.LinSols.ext
+  funext i
+  by_cases hi : i ≠ Fin.last n
+  have hiCast : ∃ j : Fin n, j.castSucc = i := by
+    exact Fin.exists_castSucc_eq.mpr hi
+  obtain ⟨j, hj⟩ := hiCast
+  rw [← hj]
+  exact h j
+  simp at hi
+  rw [hi]
+  rw [pureU1_last, pureU1_last]
+  simp only [neg_inj]
+  apply Finset.sum_congr
+  simp only
+  intro j _
+  exact h j
+
+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
+  rfl
+  rename_i k hl
+  rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
+  have hlt := hl (f ∘ Fin.castSucc)
+  erw [← hlt]
+  simp
+
+
+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
+  rfl
+  rename_i k hl
+  rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
+  have hlt := hl (f ∘ Fin.castSucc)
+  erw [← hlt]
+  simp
+
+
+end PureU1

HepLean/AnomalyCancellation/PureU1/BasisLinear.lean

@@ -0,0 +1,163 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.AnomalyCancellation.PureU1.Basic
+import Mathlib.Tactic.Polyrith
+import Mathlib.RepresentationTheory.Basic
+/-!
+# Basis of `LinSols`
+
+We give a basis of vector space `LinSols`, and find the rank thereof.
+
+-/
+
+namespace PureU1
+
+open BigOperators
+
+variable {n : ℕ}
+namespace BasisLinear
+
+/-- The basis elements as charges, defined to have a `1` in the `j`th position and a `-1` in the
+last position. -/
+@[simp]
+def asCharges (j : Fin n) : (PureU1 n.succ).charges :=
+ (fun i =>
+  if i = j.castSucc then
+    1
+  else
+    if i = Fin.last n then
+      - 1
+    else
+      0)
+
+lemma asCharges_eq_castSucc (j : Fin n) :
+    asCharges j (Fin.castSucc j) = 1 := by
+  simp [asCharges]
+
+lemma asCharges_ne_castSucc {k j : Fin n} (h : k ≠ j) :
+    asCharges k (Fin.castSucc j) = 0 := by
+  simp [asCharges]
+  split
+  rename_i h1
+  rw [Fin.ext_iff] at h1
+  simp_all
+  rw [Fin.ext_iff] at h
+  simp_all
+  split
+  rename_i h1 h2
+  rw [Fin.ext_iff] at h1 h2
+  simp at h1 h2
+  have hj : j.val < n := by
+    exact j.prop
+  simp_all
+  rfl
+
+/-- The basis elements as `LinSols`. -/
+@[simps!]
+def asLinSols (j : Fin n) : (PureU1 n.succ).LinSols :=
+  ⟨asCharges j, by
+    intro i
+    simp at i
+    match i with
+    | 0 =>
+    simp only [ Fin.isValue, PureU1_linearACCs, accGrav,
+      LinearMap.coe_mk, AddHom.coe_mk, Fin.coe_eq_castSucc]
+    rw [Fin.sum_univ_castSucc]
+    rw [Finset.sum_eq_single j]
+    simp only [asCharges, PureU1_numberCharges, ↓reduceIte]
+    have hn : ¬ (Fin.last n = Fin.castSucc j) := by
+      have hj := j.prop
+      rw [Fin.ext_iff]
+      simp only [Fin.val_last, Fin.coe_castSucc, ne_eq]
+      omega
+    split
+    rename_i ht
+    exact (hn ht).elim
+    rfl
+    intro k _ hkj
+    exact asCharges_ne_castSucc hkj.symm
+    intro hk
+    simp at hk⟩
+
+
+lemma sum_of_vectors {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
+  rfl
+  rename_i k l hl
+  rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
+  have hlt := hl (f ∘ Fin.castSucc)
+  erw [← hlt]
+  simp
+
+/-- The coordinate map for the basis. -/
+noncomputable
+def coordinateMap : ((PureU1 n.succ).LinSols) ≃ₗ[ℚ] Fin n →₀ ℚ where
+  toFun S := Finsupp.equivFunOnFinite.invFun (S.1 ∘ Fin.castSucc)
+  map_add' S T := by
+    simp only [PureU1_numberCharges, ACCSystemLinear.linSolsAddCommMonoid_add_val,
+      Equiv.invFun_as_coe]
+    ext
+    simp
+  map_smul' a S := by
+    simp only [PureU1_numberCharges, Equiv.invFun_as_coe, eq_ratCast, Rat.cast_eq_id, id_eq]
+    ext
+    simp
+    rfl
+  invFun f := ∑ i : Fin n, f i • asLinSols i
+  left_inv S := by
+    simp only [PureU1_numberCharges, Equiv.invFun_as_coe, Finsupp.equivFunOnFinite_symm_apply_toFun,
+      Function.comp_apply]
+    apply pureU1_anomalyFree_ext
+    intro j
+    rw [sum_of_vectors]
+    simp only [HSMul.hSMul, SMul.smul,  PureU1_numberCharges,
+      asLinSols_val, Equiv.toFun_as_coe,
+      Fin.coe_eq_castSucc, mul_ite, mul_one, mul_neg, mul_zero, Equiv.invFun_as_coe]
+    rw [Finset.sum_eq_single j]
+    simp only [asCharges, PureU1_numberCharges, ↓reduceIte, mul_one]
+    intro k _ hkj
+    rw [asCharges_ne_castSucc hkj]
+    simp only [mul_zero]
+    simp
+  right_inv f := by
+    simp only [PureU1_numberCharges, Equiv.invFun_as_coe]
+    ext
+    rename_i j
+    simp only [Finsupp.equivFunOnFinite_symm_apply_toFun, Function.comp_apply]
+    rw [sum_of_vectors]
+    simp only [HSMul.hSMul, SMul.smul, PureU1_numberCharges,
+      asLinSols_val, Equiv.toFun_as_coe,
+      Fin.coe_eq_castSucc, mul_ite, mul_one, mul_neg, mul_zero, Equiv.invFun_as_coe]
+    rw [Finset.sum_eq_single j]
+    simp only [asCharges, PureU1_numberCharges, ↓reduceIte, mul_one]
+    intro k _ hkj
+    rw [asCharges_ne_castSucc hkj]
+    simp only [mul_zero]
+    simp
+
+/-- The basis of `LinSols`.-/
+noncomputable
+def asBasis : Basis (Fin n) ℚ ((PureU1 n.succ).LinSols) where
+  repr := coordinateMap
+
+instance : Module.Finite ℚ ((PureU1 n.succ).LinSols) :=
+   Module.Finite.of_basis asBasis
+
+lemma finrank_AnomalyFreeLinear :
+    FiniteDimensional.finrank ℚ (((PureU1 n.succ).LinSols)) = n := by
+  have h  :=  Module.mk_finrank_eq_card_basis (@asBasis n)
+  simp_all
+  simp [FiniteDimensional.finrank]
+  rw [h]
+  simp_all only [Cardinal.toNat_natCast]
+
+
+end BasisLinear
+
+
+end PureU1

HepLean/AnomalyCancellation/PureU1/ConstAbs.lean

@@ -0,0 +1,282 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.AnomalyCancellation.PureU1.Sort
+import HepLean.AnomalyCancellation.PureU1.VectorLike
+/-!
+# Charges assignments with constant abs
+
+We look at charge assignments in which all charges have the same absolute value.
+
+-/
+universe v u
+
+open Nat
+open  Finset
+open BigOperators
+
+namespace PureU1
+
+variable {n : ℕ}
+
+/-- The condition for two rationals to have the same square (equivalent to same abs). -/
+def constAbsProp : ℚ × ℚ → Prop := fun s => s.1^2 = s.2^2
+
+/-- The condition on a charge assigment `S` to have constant absolute value among charges. -/
+@[simp]
+def constAbs (S : (PureU1 n).charges) : Prop := ∀ i j, (S i) ^ 2 = (S j) ^ 2
+
+lemma constAbs_perm (S : (PureU1 n).charges) (M :(FamilyPermutations n).group) :
+    constAbs ((FamilyPermutations n).rep M S) ↔ constAbs S := by
+  simp only [constAbs, PureU1_numberCharges, FamilyPermutations, permGroup, permCharges,
+    MonoidHom.coe_mk, OneHom.coe_mk, chargeMap_apply]
+  apply Iff.intro
+  intro h i j
+  have h2 := h (M.toFun i) (M.toFun j)
+  simp at h2
+  exact h2
+  intro h i j
+  exact h (M.invFun i) (M.invFun j)
+
+lemma constAbs_sort {S : (PureU1 n).charges} (CA : constAbs S) : constAbs (sort S) := by
+  rw [sort]
+  exact (constAbs_perm S _).mpr CA
+
+/-- The condition for a set of charges to be `sorted`, and have `constAbs`-/
+def constAbsSorted (S : (PureU1 n).charges) : Prop := constAbs S ∧ sorted S
+
+namespace constAbsSorted
+section charges
+
+variable {S : (PureU1 n.succ).charges} {A : (PureU1 n.succ).LinSols}
+variable (hS : constAbsSorted S) (hA : constAbsSorted A.val)
+
+lemma lt_eq  {k i : Fin n.succ} (hk : S k ≤ 0) (hik : i ≤ k) : S i = S k := by
+  have hSS := hS.2 i k hik
+  have ht := hS.1 i k
+  rw [sq_eq_sq_iff_eq_or_eq_neg] at ht
+  cases ht <;> rename_i h
+  exact h
+  linarith
+
+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
+
+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
+  have ht := hS.1 i k
+  rw [sq_eq_sq_iff_eq_or_eq_neg] at ht
+  cases ht <;> rename_i h
+  exact h
+  linarith
+
+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
+
+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
+  rw [sq_eq_sq_iff_eq_or_eq_neg] at hSS
+  cases' hSS with h h
+  simp_all
+  linarith
+  exact h
+
+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
+  exact ht
+
+/-- A boundary of `S : (PureU1 n.succ).charges` (assumed sorted, constAbs and non-zero)
+is defined as a element of `k ∈ Fin n` such that `S k.castSucc` and `S k.succ` are different signs.
+ -/
+@[simp]
+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
+
+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
+  rw [opposite_signs_eq_neg hS (le_of_lt hk.left) (le_of_lt hk.right)] at hn
+  linear_combination -(1 * hn)
+
+lemma boundary_split (k : Fin n) :  k.succ.val + (n.succ - k.succ.val) = n.succ := by
+  omega
+
+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]
+  erw [Finset.sum_equiv (Fin.castIso (boundary_split k)).toEquiv]
+  intro i
+  simp only [Fin.val_succ, mem_univ, RelIso.coe_fn_toEquiv]
+  intro i
+  simp
+  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
+  rw [boundary_accGrav' k]
+  rw [Fin.sum_univ_add]
+  have hfst (i : Fin k.succ.val) :
+      S (Fin.cast (boundary_split k) (Fin.castAdd (n.succ - k.succ.val) i)) = S k.castSucc := by
+    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)
+  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]
+  rw [boundary_castSucc hS hk, boundary_succ hS hk]
+  ring
+
+/-- We say a `S ∈ charges` has a boundry if there exists a `k ∈ Fin n` which is a boundary. -/
+@[simp]
+def hasBoundary (S : (PureU1 n.succ).charges) : Prop :=
+  ∃ (k : Fin n), boundary S k
+
+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
+  induction i
+  rfl
+  rename_i i hii
+  have hnott := hnot ⟨i, by {simp at hi; linarith} ⟩
+  have hii := hii (by omega)
+  erw [← hii] at hnott
+  exact (val_le_zero hS (hnott h0)).symm
+
+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
+  exact zero_gt hS hi i
+
+lemma not_hasBoundary_grav (hnot :  ¬ (hasBoundary S)) :
+    accGrav n.succ S = n.succ * S (0 : Fin n.succ) := by
+  simp [accGrav, ← not_hasBoundry_zero hS hnot]
+
+
+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
+  erw [pureU1_linear A] at h0
+  simp at h0
+  cases' h0
+  linarith
+  simp_all
+
+lemma AFL_odd_noBoundary {A : (PureU1 (2 * n + 1)).LinSols} (h : constAbsSorted A.val)
+    (hA : A.val (0 : Fin (2*n +1)) ≠ 0) : ¬ hasBoundary A.val := by
+  by_contra hn
+  obtain ⟨k, hk⟩ := hn
+  have h0 := boundary_accGrav'' h k hk
+  simp [accGrav] at h0
+  erw [pureU1_linear A] at h0
+  simp [hA] 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]
+    linear_combination - h0
+  omega
+
+lemma AFL_odd_zero {A : (PureU1 (2 * n + 1)).LinSols} (h : constAbsSorted A.val) :
+    A.val (0 : Fin (2 * n + 1)) = 0 := by
+  by_contra hn
+  exact (AFL_odd_noBoundary h hn ) (AFL_hasBoundary h hn)
+
+theorem AFL_odd (A : (PureU1 (2 * n + 1)).LinSols) (h : constAbsSorted A.val) :
+    A = 0 := by
+  apply ACCSystemLinear.LinSols.ext
+  exact  is_zero h (AFL_odd_zero h)
+
+lemma AFL_even_Boundary {A : (PureU1 (2 * n.succ)).LinSols} (h : constAbsSorted A.val)
+    (hA : A.val (0 : Fin (2 * n.succ)) ≠ 0) {k : Fin (2 * n + 1)} (hk : boundary A.val k) :
+    k.val = n := by
+  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
+  rw [← @Nat.cast_inj ℚ]
+  linear_combination h0 / 2
+
+lemma AFL_even_below' {A : (PureU1 (2 * n.succ)).LinSols} (h : constAbsSorted A.val)
+    (hA : A.val  (0 : Fin (2 * n.succ)) ≠ 0) (i : Fin n.succ)  :
+    A.val (Fin.cast (split_equal n.succ)  (Fin.castAdd n.succ i)) = A.val (0 : Fin (2*n.succ)) := by
+  obtain ⟨k, hk⟩ := AFL_hasBoundary h hA
+  rw [← boundary_castSucc h hk]
+  apply lt_eq h (le_of_lt hk.left)
+  rw [Fin.le_def]
+  simp only [PureU1_numberCharges, Fin.coe_cast, Fin.coe_castAdd, mul_eq, Fin.coe_castSucc]
+  rw [AFL_even_Boundary h hA hk]
+  omega
+
+lemma AFL_even_below (A : (PureU1 (2 * n.succ)).LinSols) (h : constAbsSorted A.val)
+    (i : Fin n.succ) :
+    A.val (Fin.cast (split_equal n.succ)  (Fin.castAdd n.succ i))
+    = A.val (0 : Fin (2*n.succ)) := by
+  by_cases hA : A.val (0 : Fin (2*n.succ)) = 0
+  rw [is_zero h hA]
+  simp
+  rfl
+  exact AFL_even_below' h hA i
+
+lemma AFL_even_above' {A : (PureU1 (2 * n.succ)).LinSols} (h : constAbsSorted A.val)
+    (hA : A.val (0 : Fin (2*n.succ)) ≠ 0) (i : Fin n.succ)  :
+    A.val (Fin.cast (split_equal n.succ)  (Fin.natAdd n.succ i)) =
+    - A.val (0 : Fin (2*n.succ)) := by
+  obtain ⟨k, hk⟩ := AFL_hasBoundary h hA
+  rw [← boundary_succ h hk]
+  apply gt_eq h (le_of_lt hk.right)
+  rw [Fin.le_def]
+  simp only [mul_eq, Fin.val_succ, PureU1_numberCharges, Fin.coe_cast, Fin.coe_natAdd]
+  rw [AFL_even_Boundary h hA hk]
+  omega
+
+lemma AFL_even_above (A : (PureU1 (2 * n.succ)).LinSols) (h : constAbsSorted A.val)
+    (i : Fin n.succ) :
+    A.val (Fin.cast (split_equal n.succ)  (Fin.natAdd n.succ i)) =
+    - A.val (0 : Fin (2*n.succ)) := by
+  by_cases hA : A.val (0 : Fin (2*n.succ)) = 0
+  rw [is_zero h hA]
+  simp
+  rfl
+  exact AFL_even_above' h hA i
+
+
+end charges
+
+end constAbsSorted
+
+
+namespace ConstAbs
+
+theorem boundary_value_odd (S : (PureU1 (2 * n + 1)).LinSols) (hs : constAbs S.val) :
+    S = 0 :=
+  have hS := And.intro (constAbs_sort hs) (sort_sorted S.val)
+  sortAFL_zero S (constAbsSorted.AFL_odd (sortAFL S) hS)
+
+
+theorem boundary_value_even (S : (PureU1 (2 * n.succ)).LinSols) (hs : constAbs S.val) :
+    vectorLikeEven S.val := by
+  have hS := And.intro (constAbs_sort hs) (sort_sorted S.val)
+  intro i
+  have h1 := constAbsSorted.AFL_even_below (sortAFL S) hS
+  have h2 := constAbsSorted.AFL_even_above (sortAFL S) hS
+  rw [sortAFL_val] at h1 h2
+  rw [h1, h2]
+  simp
+
+end ConstAbs
+
+end PureU1

HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean

@@ -0,0 +1,759 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.AnomalyCancellation.PureU1.Sort
+import HepLean.AnomalyCancellation.PureU1.BasisLinear
+import HepLean.AnomalyCancellation.PureU1.VectorLike
+import Mathlib.Logic.Equiv.Fin
+/-!
+# Basis of `LinSols` in the even case
+
+We give a basis of `LinSols` in the even case. This basis has the special propoerty
+that splits into two planes on which every point is a solution to the ACCs.
+-/
+universe v u
+
+open Nat
+open  Finset
+open BigOperators
+
+namespace PureU1
+
+variable {n : ℕ}
+
+namespace VectorLikeEvenPlane
+
+lemma n_cond₂ (n : ℕ) : 1 + ((n + n) + 1) = 2 * n.succ := by
+  linarith
+
+section theδs
+
+/-- A helper function for what follows. -/
+def δ₁ (j : Fin n.succ) : Fin (2 * n.succ) := Fin.cast (split_equal n.succ) (Fin.castAdd n.succ j)
+
+/-- A helper function for what follows. -/
+def δ₂ (j : Fin n.succ) : Fin (2 * n.succ) := Fin.cast (split_equal n.succ) (Fin.natAdd n.succ j)
+
+/-- A helper function for what follows. -/
+def δ!₁ (j : Fin n) : Fin (2 * n.succ) := Fin.cast (n_cond₂ n)
+  (Fin.natAdd 1 (Fin.castAdd 1 (Fin.castAdd n j)))
+
+/-- A helper function for what follows. -/
+def δ!₂ (j : Fin n) : Fin (2 * n.succ) := Fin.cast (n_cond₂ n)
+  (Fin.natAdd 1 (Fin.castAdd 1 (Fin.natAdd n j)))
+
+/-- A helper function for what follows. -/
+def δ!₃ : Fin (2 * n.succ) := (Fin.cast (n_cond₂ n) (Fin.castAdd ((n + n) + 1) 0))
+
+/-- A helper function for what follows. -/
+def δ!₄ : Fin (2 * n.succ) := (Fin.cast (n_cond₂ n) (Fin.natAdd 1 (Fin.natAdd (n + n) 0)))
+
+lemma ext_δ (S T : Fin (2 * n.succ) → ℚ) (h1 : ∀ i, S (δ₁ i) = T (δ₁ i))
+    (h2 : ∀ i, S (δ₂ i) = T (δ₂ i))  : S = T := by
+  funext i
+  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]
+  rw [h3] at h2
+  exact h2
+  let j : Fin n.succ := ⟨i - n.succ, by omega⟩
+  have h2 := h2 j
+  have h3 : δ₂ j = i := by
+    simp [δ₂, Fin.ext_iff]
+    omega
+  rw [h3] at h2
+  exact h2
+
+lemma sum_δ₁_δ₂  (S : Fin (2 * n.succ) → ℚ) :
+    ∑ i, S i = ∑ i : Fin n.succ, ((S ∘ δ₁) i + (S ∘ δ₂) i) := by
+  have h1 : ∑ i, S i = ∑ i : Fin (n.succ + n.succ), S (Fin.cast (split_equal n.succ) i) := by
+    rw [Finset.sum_equiv (Fin.castIso (split_equal n.succ)).symm.toEquiv]
+    intro i
+    simp only [mem_univ, Fin.symm_castIso, RelIso.coe_fn_toEquiv, Fin.castIso_apply]
+    intro i
+    simp
+  rw [h1]
+  rw [Fin.sum_univ_add, Finset.sum_add_distrib]
+  rfl
+
+lemma sum_δ₁_δ₂'  (S : Fin (2 * n.succ) → ℚ) :
+    ∑ i, S i = ∑ i : Fin n.succ, ((S ∘ δ₁) i + (S ∘ δ₂) i) := by
+  have h1 : ∑ i, S i = ∑ i : Fin (n.succ + n.succ), S (Fin.cast (split_equal n.succ) i) := by
+    rw [Finset.sum_equiv (Fin.castIso (split_equal n.succ)).symm.toEquiv]
+    intro i
+    simp only [mem_univ, Fin.symm_castIso, RelIso.coe_fn_toEquiv, Fin.castIso_apply]
+    intro i
+    simp
+  rw [h1]
+  rw [Fin.sum_univ_add, Finset.sum_add_distrib]
+  rfl
+
+lemma sum_δ!₁_δ!₂  (S : Fin (2 * n.succ) → ℚ) :
+    ∑ i, S i = S δ!₃ + S δ!₄ + ∑ i : Fin n,  ((S ∘ δ!₁) i + (S ∘ δ!₂) i) := by
+  have h1 : ∑ i, S i = ∑ i : Fin (1 + ((n + n) + 1)), S (Fin.cast (n_cond₂ n) i) := by
+    rw [Finset.sum_equiv (Fin.castIso (n_cond₂ n)).symm.toEquiv]
+    intro i
+    simp only [mem_univ, Fin.symm_castIso, RelIso.coe_fn_toEquiv, Fin.castIso_apply]
+    intro i
+    simp
+  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]
+  repeat rw [Rat.add_assoc]
+  apply congrArg
+  rw [Rat.add_comm]
+  rw [← Rat.add_assoc]
+  nth_rewrite 2 [Rat.add_comm]
+  repeat rw [Rat.add_assoc]
+  nth_rewrite 2 [Rat.add_comm]
+  rfl
+
+lemma δ!₃_δ₁0 : @δ!₃ n = δ₁ 0 := by
+  rfl
+
+lemma δ!₄_δ₂Last: @δ!₄ n = δ₂ (Fin.last n) := by
+  rw [Fin.ext_iff]
+  simp [δ!₄, δ₂]
+  omega
+
+lemma δ!₁_δ₁ (j : Fin n) : δ!₁ j = δ₁ j.succ := by
+  rw [Fin.ext_iff, δ₁, δ!₁]
+  simp only [Fin.coe_cast, Fin.coe_natAdd, Fin.coe_castAdd, Fin.val_succ]
+  ring
+
+lemma δ!₂_δ₂ (j : Fin n) : δ!₂ j = δ₂ j.castSucc := by
+  rw [Fin.ext_iff, δ₂, δ!₂]
+  simp only [Fin.coe_cast, Fin.coe_natAdd, Fin.coe_castAdd, Fin.coe_castSucc]
+  ring_nf
+  rw [Nat.succ_eq_add_one]
+  ring
+
+end theδs
+
+/-- The first part of the basis as charges. -/
+def basisAsCharges (j : Fin n.succ) : (PureU1 (2 * n.succ)).charges :=
+  fun i =>
+  if i = δ₁ j then
+    1
+  else
+    if i = δ₂ j then
+      - 1
+    else
+      0
+
+/-- The second part of the basis as charges. -/
+def basis!AsCharges (j : Fin n) : (PureU1 (2 * n.succ)).charges :=
+  fun i =>
+  if i = δ!₁ j then
+    1
+  else
+    if i = δ!₂ j then
+      - 1
+    else
+      0
+
+lemma basis_on_δ₁_self (j : Fin n.succ) : basisAsCharges j (δ₁ j) = 1 := by
+  simp [basisAsCharges]
+
+lemma basis!_on_δ!₁_self (j : Fin n) : basis!AsCharges j (δ!₁ j) = 1 := by
+  simp [basis!AsCharges]
+
+lemma basis_on_δ₁_other {k j : Fin n.succ} (h : k ≠ j) :
+    basisAsCharges k (δ₁ j) = 0 := by
+  simp [basisAsCharges]
+  simp [δ₁, δ₂]
+  split
+  rename_i h1
+  rw [Fin.ext_iff] at h1
+  simp_all
+  rw [Fin.ext_iff] at h
+  simp_all
+  split
+  rename_i h1 h2
+  simp_all
+  rw [Fin.ext_iff] at h2
+  simp at h2
+  omega
+  rfl
+
+lemma basis_on_other {k : Fin n.succ} {j : Fin (2 * n.succ)} (h1 : j ≠ δ₁ k)  (h2 : j ≠ δ₂ k) :
+    basisAsCharges k j = 0 := by
+  simp [basisAsCharges]
+  simp_all only [ne_eq, ↓reduceIte]
+
+lemma basis!_on_other {k : Fin n} {j : Fin (2 * n.succ)} (h1 : j ≠ δ!₁ k)  (h2 : j ≠ δ!₂ k) :
+    basis!AsCharges k j = 0 := by
+  simp [basis!AsCharges]
+  simp_all only [ne_eq, ↓reduceIte]
+
+
+lemma basis!_on_δ!₁_other {k j : Fin n} (h : k ≠ j) :
+    basis!AsCharges k (δ!₁ j) = 0 := by
+  simp [basis!AsCharges]
+  simp [δ!₁, δ!₂]
+  split
+  rename_i h1
+  rw [Fin.ext_iff] at h1
+  simp_all
+  rw [Fin.ext_iff] at h
+  simp_all
+  split
+  rename_i h1 h2
+  simp_all
+  rw [Fin.ext_iff] at h2
+  simp at h2
+  omega
+  rfl
+
+lemma basis_δ₂_eq_minus_δ₁ (j i : Fin n.succ) :
+    basisAsCharges j (δ₂ i) = - basisAsCharges j (δ₁ i) := by
+  simp [basisAsCharges, δ₂, δ₁]
+  split <;> split
+  any_goals split
+  any_goals split
+  any_goals rfl
+  all_goals rename_i h1 h2
+  all_goals rw [Fin.ext_iff] at h1 h2
+  all_goals simp_all
+  all_goals rename_i h3
+  all_goals rw [Fin.ext_iff] at h3
+  all_goals simp_all
+  all_goals omega
+
+lemma basis!_δ!₂_eq_minus_δ!₁ (j i : Fin n) :
+    basis!AsCharges j (δ!₂ i) = - basis!AsCharges j (δ!₁ i) := by
+  simp [basis!AsCharges, δ!₂, δ!₁]
+  split <;> split
+  any_goals split
+  any_goals split
+  any_goals rfl
+  all_goals rename_i h1 h2
+  all_goals rw [Fin.ext_iff] at h1 h2
+  all_goals simp_all
+  subst h1
+  exact Fin.elim0 i
+  all_goals rename_i h3
+  all_goals rw [Fin.ext_iff] at h3
+  all_goals simp_all
+  all_goals omega
+
+lemma basis_on_δ₂_self (j : Fin n.succ) : basisAsCharges j (δ₂ j) = - 1 := by
+  rw [basis_δ₂_eq_minus_δ₁, basis_on_δ₁_self]
+
+lemma basis!_on_δ!₂_self (j : Fin n) : basis!AsCharges j (δ!₂ j) = - 1 := by
+  rw [basis!_δ!₂_eq_minus_δ!₁, basis!_on_δ!₁_self]
+
+lemma basis_on_δ₂_other {k j : Fin n.succ} (h : k ≠ j) : basisAsCharges k (δ₂ j) = 0 := by
+  rw [basis_δ₂_eq_minus_δ₁, basis_on_δ₁_other h]
+  rfl
+
+lemma basis!_on_δ!₂_other {k j : Fin n} (h : k ≠ j) : basis!AsCharges k (δ!₂ j) = 0 := by
+  rw [basis!_δ!₂_eq_minus_δ!₁, basis!_on_δ!₁_other h]
+  rfl
+
+lemma basis!_on_δ!₃ (j : Fin n) : basis!AsCharges j δ!₃ = 0 := by
+  simp [basis!AsCharges]
+  split <;> rename_i h
+  rw [Fin.ext_iff] at h
+  simp [δ!₃, δ!₁] at h
+  omega
+  split <;> rename_i h2
+  rw [Fin.ext_iff] at h2
+  simp [δ!₃, δ!₂] at h2
+  omega
+  rfl
+
+lemma basis!_on_δ!₄ (j : Fin n) : basis!AsCharges j δ!₄ = 0 := by
+  simp [basis!AsCharges]
+  split <;> rename_i h
+  rw [Fin.ext_iff] at h
+  simp [δ!₄, δ!₁] at h
+  omega
+  split <;> rename_i h2
+  rw [Fin.ext_iff] at h2
+  simp [δ!₄, δ!₂] at h2
+  omega
+  rfl
+
+lemma basis_linearACC (j : Fin n.succ) : (accGrav (2 * n.succ)) (basisAsCharges j) = 0 := by
+  rw [accGrav]
+  simp only [LinearMap.coe_mk, AddHom.coe_mk]
+  rw [sum_δ₁_δ₂]
+  simp [basis_δ₂_eq_minus_δ₁]
+
+lemma basis!_linearACC (j : Fin n) : (accGrav (2 * n.succ)) (basis!AsCharges j) = 0 := by
+  rw [accGrav]
+  simp only [LinearMap.coe_mk, AddHom.coe_mk]
+  rw [sum_δ!₁_δ!₂, basis!_on_δ!₃, basis!_on_δ!₄]
+  simp [basis!_δ!₂_eq_minus_δ!₁]
+
+lemma basis_accCube (j : Fin n.succ) :
+    accCube (2 * n.succ) (basisAsCharges j) = 0 := by
+  rw [accCube_explicit, sum_δ₁_δ₂]
+  apply Finset.sum_eq_zero
+  intro i _
+  simp [basis_δ₂_eq_minus_δ₁]
+  ring
+
+lemma basis!_accCube (j : Fin n) :
+    accCube (2 * n.succ) (basis!AsCharges j) = 0 := by
+  rw [accCube_explicit, sum_δ!₁_δ!₂]
+  rw [basis!_on_δ!₄, basis!_on_δ!₃]
+  simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, add_zero, Function.comp_apply,
+    zero_add]
+  apply Finset.sum_eq_zero
+  intro i _
+  simp [basis!_δ!₂_eq_minus_δ!₁]
+  ring
+
+
+/-- The first part of the basis as `LinSols`. -/
+@[simps!]
+def basis (j : Fin n.succ) : (PureU1 (2 * n.succ)).LinSols :=
+  ⟨basisAsCharges j, by
+    intro i
+    simp at i
+    match i with
+    | 0 =>
+    exact basis_linearACC j⟩
+
+/-- The second part of the basis as `LinSols`. -/
+@[simps!]
+def basis! (j : Fin n) : (PureU1 (2 * n.succ)).LinSols :=
+  ⟨basis!AsCharges j, by
+    intro i
+    simp at i
+    match i with
+    | 0 =>
+    exact basis!_linearACC j⟩
+
+/-- The whole basis as `LinSols`. -/
+def basisa : (Fin n.succ) ⊕ (Fin n) → (PureU1 (2 * n.succ)).LinSols := fun i =>
+  match i with
+  | .inl i => basis i
+  | .inr i => basis! i
+
+/-- Swapping the elements δ!₁ j and δ!₂ j is equivalent to adding a vector basis!AsCharges j. -/
+lemma swap!_as_add {S S' : (PureU1 (2 * n.succ)).LinSols} (j : Fin n)
+    (hS : ((FamilyPermutations (2 * n.succ)).linSolRep
+    (pairSwap (δ!₁ j)  (δ!₂ j))) S = S') :
+    S'.val = S.val + (S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j := by
+  funext i
+  rw [← hS, FamilyPermutations_anomalyFreeLinear_apply]
+  by_cases  hi : i = δ!₁ j
+  subst hi
+  simp [HSMul.hSMul, basis!_on_δ!₁_self, pairSwap_inv_fst]
+  by_cases hi2 : i = δ!₂ j
+  subst hi2
+  simp [HSMul.hSMul, basis!_on_δ!₂_self, pairSwap_inv_snd]
+  simp [HSMul.hSMul]
+  rw [basis!_on_other hi hi2]
+  change  S.val ((pairSwap (δ!₁ j) (δ!₂ j)).invFun i) =_
+  erw [pairSwap_inv_other (Ne.symm hi) (Ne.symm hi2)]
+  simp
+
+/-- A point in the span of the first part of the basis as a charge. -/
+def P (f : Fin n.succ → ℚ) : (PureU1 (2 * n.succ)).charges := ∑ i, f i • basisAsCharges i
+
+/-- A point in the span of the second part of the basis as a charge. -/
+def P! (f : Fin n → ℚ) : (PureU1 (2 * n.succ)).charges := ∑ i, f i • basis!AsCharges i
+
+/-- A point in the span of the basis as a charge. -/
+def Pa (f : Fin n.succ → ℚ) (g : Fin n → ℚ) : (PureU1 (2 * n.succ)).charges := P f + P! g
+
+lemma P_δ₁ (f : Fin n.succ → ℚ) (j : Fin n.succ) : P f (δ₁ j) = f j := by
+  rw [P, sum_of_charges]
+  simp [HSMul.hSMul, SMul.smul]
+  rw [Finset.sum_eq_single j]
+  rw [basis_on_δ₁_self]
+  simp only [mul_one]
+  intro k _ hkj
+  rw [basis_on_δ₁_other hkj]
+  simp only [mul_zero]
+  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
+  rw [P!, sum_of_charges]
+  simp [HSMul.hSMul, SMul.smul]
+  rw [Finset.sum_eq_single j]
+  rw [basis!_on_δ!₁_self]
+  simp only [mul_one]
+  intro k _ hkj
+  rw [basis!_on_δ!₁_other hkj]
+  simp only [mul_zero]
+  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) :
+    Pa f g (δ!₁ j) = f j.succ + g j := by
+  rw [Pa]
+  simp only [ACCSystemCharges.chargesAddCommMonoid_add]
+  rw [P!_δ!₁, δ!₁_δ₁, P_δ₁]
+
+lemma P_δ₂ (f : Fin n.succ → ℚ) (j : Fin n.succ) : P f (δ₂ j) = - f j := by
+  rw [P, sum_of_charges]
+  simp [HSMul.hSMul, SMul.smul]
+  rw [Finset.sum_eq_single j]
+  rw [basis_on_δ₂_self]
+  simp only [mul_neg, mul_one]
+  intro k _ hkj
+  rw [basis_on_δ₂_other hkj]
+  simp only [mul_zero]
+  simp
+
+lemma P!_δ!₂ (f : Fin n → ℚ) (j : Fin n) : P! f (δ!₂ j) = - f j := by
+  rw [P!, sum_of_charges]
+  simp [HSMul.hSMul, SMul.smul]
+  rw [Finset.sum_eq_single j]
+  rw [basis!_on_δ!₂_self]
+  simp only [mul_neg, mul_one]
+  intro k _ hkj
+  rw [basis!_on_δ!₂_other hkj]
+  simp only [mul_zero]
+  simp
+
+lemma Pa_δ!₂ (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (j : Fin n) :
+    Pa f g (δ!₂ j) = - f j.castSucc - g j := by
+  rw [Pa]
+  simp only [ACCSystemCharges.chargesAddCommMonoid_add]
+  rw [P!_δ!₂, δ!₂_δ₂, P_δ₂]
+  ring
+
+lemma P!_δ!₃ (f : Fin n → ℚ) : P! f (δ!₃) = 0 := by
+  rw [P!, sum_of_charges]
+  simp [HSMul.hSMul, SMul.smul, basis!_on_δ!₃]
+
+lemma Pa_δ!₃  (f : Fin n.succ → ℚ) (g : Fin n → ℚ) :  Pa f g (δ!₃) =  f 0 := by
+  rw [Pa]
+  simp only [ACCSystemCharges.chargesAddCommMonoid_add]
+  rw [P!_δ!₃, δ!₃_δ₁0, P_δ₁]
+  simp
+
+lemma P!_δ!₄ (f : Fin n → ℚ) : P! f (δ!₄) = 0 := by
+  rw [P!, sum_of_charges]
+  simp [HSMul.hSMul, SMul.smul, basis!_on_δ!₄]
+
+lemma Pa_δ!₄  (f : Fin n.succ → ℚ) (g : Fin n → ℚ) :  Pa f g (δ!₄) = - f (Fin.last n) := by
+  rw [Pa]
+  simp only [ACCSystemCharges.chargesAddCommMonoid_add]
+  rw [P!_δ!₄, δ!₄_δ₂Last, P_δ₂]
+  simp
+
+lemma P_δ₁_δ₂ (f : Fin n.succ → ℚ)  : P f ∘ δ₂ = - P f ∘ δ₁ := by
+  funext j
+  simp only [PureU1_numberCharges, Function.comp_apply, Pi.neg_apply]
+  rw [P_δ₁, P_δ₂]
+
+lemma P_linearACC (f : Fin n.succ → ℚ) : (accGrav (2 * n.succ)) (P f) = 0 := by
+  rw [accGrav]
+  simp only [LinearMap.coe_mk, AddHom.coe_mk]
+  rw [sum_δ₁_δ₂]
+  simp [P_δ₂, P_δ₁]
+
+lemma P_accCube (f : Fin n.succ → ℚ) : accCube (2 * n.succ) (P f) = 0 := by
+  rw [accCube_explicit, sum_δ₁_δ₂]
+  apply Finset.sum_eq_zero
+  intro i _
+  simp [P_δ₁, P_δ₂]
+  ring
+
+lemma P!_accCube (f : Fin n → ℚ) : accCube (2 * n.succ) (P! f) = 0 := by
+  rw [accCube_explicit, sum_δ!₁_δ!₂, P!_δ!₃, P!_δ!₄]
+  simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, add_zero, Function.comp_apply,
+    zero_add]
+  apply Finset.sum_eq_zero
+  intro i _
+  simp [P!_δ!₁, P!_δ!₂]
+  ring
+
+lemma P_P_P!_accCube (g : Fin n.succ → ℚ) (j : Fin n) :
+    accCubeTriLinSymm.toFun (P g, P g, basis!AsCharges j)
+    = g (j.succ) ^ 2 - g (j.castSucc) ^ 2 := by
+  simp [accCubeTriLinSymm]
+  rw [sum_δ!₁_δ!₂, basis!_on_δ!₃, basis!_on_δ!₄]
+  simp only [mul_zero, add_zero, Function.comp_apply, zero_add]
+  rw [Finset.sum_eq_single j, basis!_on_δ!₁_self, basis!_on_δ!₂_self]
+  simp [δ!₁_δ₁, δ!₂_δ₂]
+  rw [P_δ₁, P_δ₂]
+  ring
+  intro k _ hkj
+  erw [basis!_on_δ!₁_other hkj.symm, basis!_on_δ!₂_other hkj.symm]
+  simp only [mul_zero, add_zero]
+  simp
+
+lemma P_P!_P!_accCube (g : Fin n → ℚ) (j : Fin n.succ) :
+    accCubeTriLinSymm.toFun (P! g, P! g, basisAsCharges j)
+    =  (P! g (δ₁ j))^2 -  (P! g (δ₂ j))^2 := by
+  simp [accCubeTriLinSymm]
+  rw [sum_δ₁_δ₂]
+  simp only [Function.comp_apply]
+  rw [Finset.sum_eq_single j, basis_on_δ₁_self, basis_on_δ₂_self]
+  simp [δ!₁_δ₁, δ!₂_δ₂]
+  ring
+  intro k _ hkj
+  erw [basis_on_δ₁_other hkj.symm, basis_on_δ₂_other hkj.symm]
+  simp only [mul_zero, add_zero]
+  simp
+
+lemma P_zero (f : Fin n.succ → ℚ) (h : P f = 0) : ∀ i, f i = 0 := by
+  intro i
+  erw [← P_δ₁ f]
+  rw [h]
+  rfl
+
+lemma P!_zero (f : Fin n → ℚ) (h : P! f = 0) : ∀ i, f i = 0 := by
+  intro i
+  rw [← P!_δ!₁ f]
+  rw [h]
+  rfl
+
+lemma Pa_zero (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (h : Pa f g = 0) :
+    ∀ i, f i = 0 := by
+  have h₃ := Pa_δ!₃ f g
+  rw [h] at h₃
+  change 0 = f 0 at h₃
+  intro i
+  have hinduc (iv : ℕ) (hiv : iv < n.succ) : f ⟨iv, hiv⟩ = 0 := by
+    induction iv
+    exact h₃.symm
+    rename_i iv hi
+    have hivi : iv < n.succ := by omega
+    have hi2 := hi hivi
+    have h1 := Pa_δ!₁ f g ⟨iv, by omega⟩
+    have h2 := Pa_δ!₂ f g ⟨iv, by omega⟩
+    rw [h] at h1 h2
+    simp at h1 h2
+    erw [hi2] at h2
+    change 0 = _ at h2
+    simp at h2
+    rw [h2] at h1
+    simp at h1
+    exact h1.symm
+  exact hinduc i.val i.prop
+
+lemma Pa_zero! (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (h : Pa f g = 0) :
+    ∀ i, g i = 0 := by
+  have hf := Pa_zero f g h
+  rw [Pa, P] at h
+  simp [hf] at h
+  exact P!_zero g h
+
+/-- A point in the span of the first part of the basis. -/
+def P' (f : Fin n.succ → ℚ) : (PureU1 (2 * n.succ)).LinSols := ∑ i, f i • basis i
+
+/-- A point in the span of the second part of the basis. -/
+def P!' (f : Fin n → ℚ) : (PureU1 (2 * n.succ)).LinSols := ∑ i, f i • basis! i
+
+/-- A point in the span of the whole basis. -/
+def Pa' (f : (Fin n.succ) ⊕ (Fin n) → ℚ) : (PureU1 (2 * n.succ)).LinSols :=
+    ∑ i, f i • basisa i
+
+lemma Pa'_P'_P!' (f : (Fin n.succ) ⊕ (Fin n) → ℚ) :
+    Pa' f = P' (f ∘ Sum.inl) + P!' (f ∘ Sum.inr):= by
+  exact Fintype.sum_sum_type _
+
+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]
+
+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]
+
+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
+  rw [P'_val] at h1
+  exact P_zero f h1
+
+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
+  rw [P!'_val] at h1
+  exact P!_zero f h1
+
+
+theorem basisa_linear_independent : LinearIndependent ℚ (@basisa n) := 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
+  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
+  change Pa (f ∘ Sum.inl) (f ∘ Sum.inr) = 0 at h1
+  have hf := Pa_zero (f ∘ Sum.inl) (f ∘ Sum.inr) h1
+  have hg := Pa_zero! (f ∘ Sum.inl) (f ∘ Sum.inr) h1
+  intro i
+  simp_all
+  cases i
+  simp_all
+  simp_all
+
+lemma Pa'_eq (f f' : (Fin n.succ) ⊕ (Fin n) → ℚ)  : Pa' f = Pa' f' ↔ f = f' := by
+  apply Iff.intro
+  intro h
+  funext i
+  rw [Pa', Pa'] at h
+  have h1 : ∑ i : Fin (succ n) ⊕ Fin n, (f i + (- f' i)) • basisa i = 0 := by
+    simp only [add_smul, neg_smul]
+    rw [Finset.sum_add_distrib]
+    rw [h]
+    rw [← Finset.sum_add_distrib]
+    simp
+  have h2 : ∀ i, (f i + (- f' i)) = 0 := by
+    exact Fintype.linearIndependent_iff.mp (@basisa_linear_independent (n))
+     (fun i => f i + -f' i) h1
+  have h2i := h2 i
+  linarith
+  intro h
+  rw [h]
+
+/-- A helper function for what follows. TODO: replace this with mathlib functions. -/
+def join (g : Fin n.succ → ℚ) (f : Fin n → ℚ) :  (Fin n.succ) ⊕ (Fin n) → ℚ := fun i =>
+  match i with
+  | .inl i => g i
+  | .inr i => f i
+
+lemma join_ext (g g' : Fin n.succ → ℚ) (f f' : Fin n → ℚ) :
+    join g f = join g' f' ↔ g = g' ∧ f = f' := by
+  apply Iff.intro
+  intro h
+  apply And.intro
+  funext i
+  exact congr_fun h (Sum.inl i)
+  funext i
+  exact congr_fun h (Sum.inr i)
+  intro h
+  rw [h.left, h.right]
+
+lemma join_Pa (g g' : Fin n.succ → ℚ) (f f' : Fin n → ℚ) :
+    Pa' (join g f) = Pa' (join g' f') ↔ Pa g f = Pa g' f' := by
+  apply Iff.intro
+  intro h
+  rw [Pa'_eq] at h
+  rw [join_ext] at h
+  rw [h.left, h.right]
+  intro h
+  apply ACCSystemLinear.LinSols.ext
+  rw [Pa'_P'_P!', Pa'_P'_P!']
+  simp [P'_val, P!'_val]
+  exact h
+
+lemma Pa_eq (g g' : Fin n.succ → ℚ) (f f' : Fin n → ℚ) :
+    Pa g f = Pa g' f' ↔ g = g' ∧ f = f' := by
+  rw [← join_Pa]
+  rw [← join_ext]
+  exact Pa'_eq _ _
+
+
+lemma basisa_card :  Fintype.card ((Fin n.succ) ⊕ (Fin n)) =
+    FiniteDimensional.finrank ℚ (PureU1 (2 * n.succ)).LinSols := by
+  erw [BasisLinear.finrank_AnomalyFreeLinear]
+  simp only [Fintype.card_sum, Fintype.card_fin, mul_eq]
+  omega
+
+/-- The basis formed out of our basisa vectors. -/
+noncomputable def basisaAsBasis :
+    Basis (Fin (succ n) ⊕ Fin n) ℚ (PureU1 (2 * succ n)).LinSols :=
+  basisOfLinearIndependentOfCardEqFinrank (@basisa_linear_independent n) basisa_card
+
+
+lemma span_basis (S : (PureU1 (2 * n.succ)).LinSols) :
+    ∃ (g : Fin n.succ → ℚ) (f : Fin n → ℚ), S.val = P g + P! f  := by
+  have h := (mem_span_range_iff_exists_fun ℚ).mp (Basis.mem_span basisaAsBasis S)
+  obtain ⟨f, hf⟩ := h
+  simp [basisaAsBasis] at hf
+  change P' _ + P!' _ = S at hf
+  use f ∘ Sum.inl
+  use f ∘ Sum.inr
+  rw [← hf]
+  simp [P'_val, P!'_val]
+  rfl
+
+lemma P!_in_span (f : Fin n → ℚ) : P! f ∈ Submodule.span ℚ (Set.range basis!AsCharges) := by
+     rw [(mem_span_range_iff_exists_fun ℚ)]
+     use f
+     rfl
+
+lemma smul_basis!AsCharges_in_span (S : (PureU1 (2 * n.succ )).LinSols) (j : Fin n) :
+    (S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j ∈
+    Submodule.span ℚ (Set.range basis!AsCharges) := by
+  apply Submodule.smul_mem
+  apply SetLike.mem_of_subset
+  apply Submodule.subset_span
+  simp_all only [Set.mem_range, exists_apply_eq_apply]
+
+lemma span_basis_swap! {S : (PureU1 (2 * n.succ)).LinSols} (j : Fin n)
+    (hS : ((FamilyPermutations (2 * n.succ)).linSolRep
+    (pairSwap (δ!₁ j) (δ!₂ j))) S = S') (g : Fin n.succ → ℚ) (f : Fin n → ℚ)
+     (h : S.val = P g + P! f):
+    ∃
+    (g' : Fin n.succ → ℚ) (f' : Fin n → ℚ) ,
+     S'.val = P g' + P! f' ∧ P! f' = P! f +
+    (S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j ∧ g' = g := by
+  let X := P! f + (S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j
+  have hX : X ∈  Submodule.span ℚ (Set.range (basis!AsCharges)) := by
+    apply Submodule.add_mem
+    exact (P!_in_span f)
+    exact (smul_basis!AsCharges_in_span S j)
+  have hXsum := (mem_span_range_iff_exists_fun ℚ).mp hX
+  obtain ⟨f', hf'⟩ := hXsum
+  use g
+  use f'
+  change P! f' = _ at hf'
+  erw [hf']
+  simp only [and_self, and_true]
+  change S'.val = P g + (P! f + _)
+  rw [← add_assoc, ← h]
+  apply swap!_as_add at hS
+  exact hS
+
+lemma vectorLikeEven_in_span (S : (PureU1 (2 * n.succ)).LinSols)
+    (hS : vectorLikeEven S.val) :
+   ∃ (M : (FamilyPermutations (2 * n.succ)).group),
+    (FamilyPermutations (2 * n.succ)).linSolRep M S
+    ∈ Submodule.span ℚ (Set.range basis) := by
+  use (Tuple.sort S.val).symm
+  change sortAFL S ∈ Submodule.span ℚ (Set.range basis)
+  rw [mem_span_range_iff_exists_fun ℚ]
+  let f : Fin n.succ → ℚ := fun i => (sortAFL S).val (δ₁ i)
+  use f
+  apply ACCSystemLinear.LinSols.ext
+  rw [sortAFL_val]
+  erw [P'_val]
+  apply ext_δ
+  intro i
+  rw [P_δ₁]
+  rfl
+  intro i
+  rw [P_δ₂]
+  have ht := hS i
+  change sort S.val (δ₁ i) = - sort S.val (δ₂ i) at ht
+  have h : sort S.val (δ₂ i) = - sort S.val (δ₁ i) := by
+    rw [ht]
+    ring
+  rw [h]
+  simp
+  rfl
+
+end VectorLikeEvenPlane
+
+end PureU1

HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean

@@ -0,0 +1,174 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.AnomalyCancellation.PureU1.Basic
+import HepLean.AnomalyCancellation.PureU1.ConstAbs
+import HepLean.AnomalyCancellation.PureU1.Even.BasisLinear
+import HepLean.AnomalyCancellation.PureU1.LineInPlaneCond
+import HepLean.AnomalyCancellation.PureU1.Permutations
+import Mathlib.RepresentationTheory.Basic
+import Mathlib.Tactic.Polyrith
+/-!
+
+# Line In Cubic Even case
+
+We say that a linear solution satisfies the `lineInCubic` property
+if the line through that point and through the two different planes formed by the baisis of
+`LinSols` lies in the cubic.
+
+We show that for a solution all its permutations satsfiy this property, then there exists
+a permutation for which it lies in the plane spanned by the first part of the basis.
+
+The main reference for this file is:
+
+- https://arxiv.org/pdf/1912.04804.pdf
+-/
+
+namespace PureU1
+namespace Even
+
+open BigOperators
+
+variable {n : ℕ}
+open VectorLikeEvenPlane
+
+/-- A  property on `LinSols`, statified if every point on the line between the two planes
+in the basis through that point is in the cubic. -/
+def lineInCubic (S : (PureU1 (2 * n.succ)).LinSols) : Prop :=
+  ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = Pa g f) (a b : ℚ) ,
+  accCube (2 * n.succ) (a • P g + b • P! f) = 0
+
+lemma lineInCubic_expand {S : (PureU1 (2 * n.succ)).LinSols} (h : lineInCubic S) :
+    ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = Pa g f) (a b : ℚ) ,
+    3 * a * b * (a * accCubeTriLinSymm (P g, P g, P! f)
+    + b * accCubeTriLinSymm (P! f, P! f, P g)) = 0 := by
+  intro g f hS a b
+  have h1 := h g f hS a b
+  change accCubeTriLinSymm.toCubic (a • P g + b • P! f) = 0 at h1
+  simp only [TriLinearSymm.toCubic_add] at h1
+  simp only [HomogeneousCubic.map_smul,
+   accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂, accCubeTriLinSymm.map_smul₃] at h1
+  erw [P_accCube, P!_accCube] at h1
+  rw [← h1]
+  ring
+
+/--
+ This lemma states that for a given `S` of type `(PureU1 (2 * n.succ)).AnomalyFreeLinear` and
+ a proof `h` that the line through `S` lies on a cubic curve,
+ for any functions `g : Fin n.succ → ℚ` and `f : Fin n → ℚ`, if `S.val = P g + P! f`,
+ then `accCubeTriLinSymm.toFun (P g, P g, P! f) = 0`.
+-/
+lemma line_in_cubic_P_P_P! {S : (PureU1 (2 * n.succ)).LinSols} (h : lineInCubic S) :
+    ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val =  P g + P! f),
+    accCubeTriLinSymm (P g, P g, P! f) = 0 := by
+  intro g f hS
+  linear_combination 2 / 3 * (lineInCubic_expand h g f hS 1 1) -
+   (lineInCubic_expand h g f hS 1 2) / 6
+
+/-- We say a `LinSol` satifies  `lineInCubicPerm` if all its permutations satsify `lineInCubic`. -/
+def lineInCubicPerm (S : (PureU1 (2 * n.succ)).LinSols) : Prop :=
+  ∀ (M : (FamilyPermutations (2 * n.succ)).group ),
+  lineInCubic ((FamilyPermutations (2 * n.succ)).linSolRep M S)
+
+/-- If `lineInCubicPerm S` then `lineInCubic S`.  -/
+lemma lineInCubicPerm_self {S : (PureU1 (2 * n.succ)).LinSols}
+    (hS : lineInCubicPerm S) : lineInCubic S := hS 1
+
+/-- If `lineInCubicPerm S` then `lineInCubicPerm (M S)` for all permutations `M`. -/
+lemma lineInCubicPerm_permute {S : (PureU1 (2 * n.succ)).LinSols}
+    (hS : lineInCubicPerm S) (M' : (FamilyPermutations (2 * n.succ)).group) :
+    lineInCubicPerm ((FamilyPermutations (2 * n.succ)).linSolRep M' S) := by
+  rw [lineInCubicPerm]
+  intro M
+  change lineInCubic
+    (((FamilyPermutations (2 * n.succ)).linSolRep M *
+    (FamilyPermutations (2 * n.succ)).linSolRep M') S)
+  erw [← (FamilyPermutations (2 * n.succ)).linSolRep.map_mul M M']
+  exact hS (M * M')
+
+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))
+      * accCubeTriLinSymm.toFun (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
+  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
+  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.toFun (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
+  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)
+  simp at h1 h2 h3
+  have hl : f (Fin.succ  (Fin.last (n ))) = - Pa f g δ!₄ := 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
+    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
+    linear_combination h3 - 1 * hg
+  rw [← hS] at hl hll
+  rw [hl, hll]
+  ring
+
+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
+  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
+  simp at h1
+  cases h1 <;> rename_i h1
+  apply Or.inl
+  linear_combination h1
+  cases h1 <;> rename_i h1
+  apply Or.inr
+  apply Or.inl
+  linear_combination -(1 * h1)
+  apply Or.inr
+  apply Or.inr
+  exact h1
+
+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 [Fin.ext_iff, δ!₁, δ!₄]
+  omega
+  intro M
+  exact lineInCubicPerm_last_cond (lineInCubicPerm_permute LIC M)
+
+lemma lineInCubicPerm_constAbs  {S : (PureU1 (2 * n.succ.succ)).Sols}
+    (LIC : lineInCubicPerm S.1.1) : constAbs S.val :=
+  linesInPlane_constAbs_AF S (lineInCubicPerm_last_perm LIC)
+
+theorem  lineInCubicPerm_vectorLike  {S : (PureU1 (2 * n.succ.succ)).Sols}
+    (LIC : lineInCubicPerm S.1.1) : vectorLikeEven S.val :=
+  ConstAbs.boundary_value_even S.1.1 (lineInCubicPerm_constAbs LIC)
+
+theorem lineInCubicPerm_in_plane  (S : (PureU1 (2 * n.succ.succ)).Sols)
+    (LIC : lineInCubicPerm S.1.1) : ∃ (M : (FamilyPermutations (2 * n.succ.succ)).group),
+    (FamilyPermutations (2 * n.succ.succ)).linSolRep M S.1.1
+    ∈ Submodule.span ℚ (Set.range basis) :=
+  vectorLikeEven_in_span S.1.1 (lineInCubicPerm_vectorLike LIC)
+
+end Even
+end PureU1

HepLean/AnomalyCancellation/PureU1/Even/Parameterization.lean

@@ -0,0 +1,173 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.AnomalyCancellation.PureU1.Basic
+import HepLean.AnomalyCancellation.PureU1.ConstAbs
+import HepLean.AnomalyCancellation.PureU1.LineInPlaneCond
+import HepLean.AnomalyCancellation.PureU1.Even.BasisLinear
+import HepLean.AnomalyCancellation.PureU1.Even.LineInCubic
+import HepLean.AnomalyCancellation.PureU1.Permutations
+import Mathlib.RepresentationTheory.Basic
+import Mathlib.Tactic.Polyrith
+/-!
+# Parameterization in even case
+
+Given maps `g : Fin n.succ → ℚ`,  `f : Fin n → ℚ` and `a : ℚ` we form a solution to the anomaly
+equations. We show that every solution can be got in this way, up to permutation, unless it, up to
+permutaiton, lives in the plane spanned by the firt part of the basis vector.
+
+The main reference is:
+
+- https://arxiv.org/pdf/1912.04804.pdf
+
+-/
+
+namespace PureU1
+namespace Even
+
+open BigOperators
+
+variable {n : ℕ}
+open VectorLikeEvenPlane
+
+/-- Given coefficents `g` of a point in `P` and `f` of a point in `P!`, and a rational, we get a
+rational `a ∈ ℚ`, we get a
+point in `(PureU1 (2 * n.succ)).AnomalyFreeLinear`, which we will later show extends to an anomaly
+free point. -/
+def parameterizationAsLinear (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (a : ℚ) :
+    (PureU1 (2 * n.succ)).LinSols :=
+  a • ((accCubeTriLinSymm (P! f, P! f, P g)) • P' g +
+  (- accCubeTriLinSymm (P g, P g, P! f)) • P!' f)
+
+lemma parameterizationAsLinear_val (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (a : ℚ) :
+    (parameterizationAsLinear g f a).val =
+    a • ((accCubeTriLinSymm (P! f, P! f, P g)) • P g +
+    (- accCubeTriLinSymm (P g, P g, P! f)) • P! f) := by
+  rw [parameterizationAsLinear]
+  change a • (_ • (P' g).val + _ • (P!' f).val) = _
+  rw [P'_val, P!'_val]
+
+lemma parameterizationCharge_cube (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (a : ℚ):
+    accCube (2* n.succ) (parameterizationAsLinear g f a).val = 0 := by
+  change accCubeTriLinSymm.toCubic _ = 0
+  rw [parameterizationAsLinear_val, HomogeneousCubic.map_smul,
+    TriLinearSymm.toCubic_add, HomogeneousCubic.map_smul, HomogeneousCubic.map_smul]
+  erw [P_accCube, P!_accCube]
+  rw [accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂,
+   accCubeTriLinSymm.map_smul₃, accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂,
+   accCubeTriLinSymm.map_smul₃]
+  ring
+
+/-- 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⟩,
+  parameterizationCharge_cube g f a⟩
+
+lemma anomalyFree_param {S : (PureU1 (2 * n.succ)).Sols}
+    (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (hS : S.val = P g + P! f) :
+    accCubeTriLinSymm (P g, P g, P! f) = - accCubeTriLinSymm (P! f, P! f, P g) := by
+  have hC := S.cubicSol
+  rw [hS] at hC
+  change (accCube (2 * n.succ)) (P g + P! f) = 0 at hC
+  erw [TriLinearSymm.toCubic_add] at hC
+  erw [P_accCube] at hC
+  erw [P!_accCube] at hC
+  linear_combination hC / 3
+
+/-- A proposition on a solution which is true if `accCubeTriLinSymm (P g, P g, P! f) ≠  0`.
+In this case our parameterization above will be able to recover this point. -/
+def genericCase (S : (PureU1 (2 * n.succ)).Sols) : Prop :=
+  ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = P g + P! f) ,
+  accCubeTriLinSymm (P g, P g, P! f) ≠  0
+
+lemma genericCase_exists (S : (PureU1 (2 * n.succ)).Sols)
+    (hs : ∃ (g : Fin n.succ → ℚ) (f : Fin n → ℚ), S.val = P g + P! f ∧
+    accCubeTriLinSymm (P g, P g, P! f) ≠  0) : genericCase S := by
+  intro g f hS hC
+  obtain ⟨g', f', hS', hC'⟩ := hs
+  rw [hS] at hS'
+  erw [Pa_eq] at hS'
+  rw [hS'.1, hS'.2] at hC
+  exact hC' hC
+
+/-- A proposition on a solution which is true if `accCubeTriLinSymm (P g, P g, P! f) = 0`.-/
+def specialCase  (S : (PureU1 (2 * n.succ)).Sols) : Prop :=
+  ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = P g + P! f) ,
+  accCubeTriLinSymm (P g, P g, P! f) = 0
+
+lemma specialCase_exists (S : (PureU1 (2 * n.succ)).Sols)
+    (hs : ∃ (g : Fin n.succ → ℚ) (f : Fin n → ℚ), S.val = P g + P! f ∧
+    accCubeTriLinSymm (P g, P g, P! f) =  0) : specialCase S := by
+  intro g f hS
+  obtain ⟨g', f', hS', hC'⟩ := hs
+  rw [hS] at hS'
+  erw [Pa_eq] at hS'
+  rw [hS'.1, hS'.2]
+  exact hC'
+
+lemma generic_or_special (S : (PureU1 (2 * n.succ)).Sols) :
+    genericCase S ∨ specialCase S := by
+  obtain ⟨g, f, h⟩ := span_basis S.1.1
+  have h1 :  accCubeTriLinSymm (P g, P g, P! f) ≠  0 ∨
+     accCubeTriLinSymm (P g, P g, P! f) = 0 := by
+    exact ne_or_eq _ _
+  cases h1 <;> rename_i h1
+  exact Or.inl (genericCase_exists S ⟨g, f, h, h1⟩)
+  exact Or.inr (specialCase_exists S ⟨g, f, h, h1⟩)
+
+theorem generic_case {S : (PureU1 (2 * n.succ)).Sols} (h : genericCase S) :
+    ∃ g f a,  S = parameterization g f a := by
+  obtain ⟨g, f, hS⟩ := span_basis S.1.1
+  use g, f, (accCubeTriLinSymm (P! f, P! f, P g))⁻¹
+  rw [parameterization]
+  apply ACCSystem.Sols.ext
+  rw [parameterizationAsLinear_val]
+  change S.val = _ • ( _ • P g + _• P! f)
+  rw [anomalyFree_param _ _ hS]
+  rw [neg_neg, ← smul_add, smul_smul, inv_mul_cancel, one_smul]
+  exact hS
+  have h := h g f hS
+  rw [anomalyFree_param _ _ hS] at h
+  simp at h
+  exact h
+
+
+lemma special_case_lineInCubic {S : (PureU1 (2 * n.succ)).Sols}
+    (h : specialCase S) : lineInCubic S.1.1 := by
+  intro g f hS a b
+  erw [TriLinearSymm.toCubic_add]
+  rw [HomogeneousCubic.map_smul, HomogeneousCubic.map_smul]
+  erw [P_accCube, P!_accCube]
+  have h := h g f hS
+  rw [accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂,
+   accCubeTriLinSymm.map_smul₃, accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂,
+   accCubeTriLinSymm.map_smul₃]
+  rw [h]
+  rw [anomalyFree_param _ _ hS] at h
+  simp at h
+  change accCubeTriLinSymm (P! f, P! f, P g) = 0 at h
+  erw [h]
+  simp
+
+
+lemma special_case_lineInCubic_perm {S : (PureU1 (2 * n.succ)).Sols}
+    (h : ∀ (M : (FamilyPermutations (2 * n.succ)).group),
+    specialCase ((FamilyPermutations (2 * n.succ)).solAction.toFun S M)) :
+    lineInCubicPerm S.1.1 := by
+  intro M
+  exact special_case_lineInCubic (h M)
+
+
+theorem special_case {S : (PureU1 (2 * n.succ.succ)).Sols}
+    (h : ∀ (M : (FamilyPermutations (2 * n.succ.succ)).group),
+    specialCase ((FamilyPermutations (2 * n.succ.succ)).solAction.toFun S M)) :
+    ∃ (M : (FamilyPermutations (2 * n.succ.succ)).group),
+    ((FamilyPermutations (2 * n.succ.succ)).solAction.toFun S M).1.1
+    ∈ Submodule.span ℚ (Set.range basis) :=
+  lineInCubicPerm_in_plane S (special_case_lineInCubic_perm h)
+
+end Even
+end PureU1

HepLean/AnomalyCancellation/PureU1/LineInPlaneCond.lean

@@ -0,0 +1,187 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.AnomalyCancellation.PureU1.Basic
+import HepLean.AnomalyCancellation.PureU1.Permutations
+import HepLean.AnomalyCancellation.PureU1.VectorLike
+import HepLean.AnomalyCancellation.PureU1.ConstAbs
+import Mathlib.Tactic.Polyrith
+import Mathlib.RepresentationTheory.Basic
+/-!
+# Line in plane condition
+
+We say a `LinSol` satifies the `line in plane` condition if for all distinct `i1`, `i2`, `i3` in
+`Fin n`, we have
+`S i1 = S i2`  or  `S i1 = - S i2` or  `2 S i3 + S i1 + S i2 = 0`.
+
+We look at various consequences of this.
+The main reference for this material is
+
+- https://arxiv.org/pdf/1912.04804.pdf
+
+We will show that `n ≥ 4` the `line in plane` condition on solutions inplies the
+`constAbs` condition.
+
+-/
+
+
+namespace PureU1
+
+open BigOperators
+
+variable {n : ℕ}
+
+/-- The proposition on three rationals to satisfy the `linInPlane` condition. -/
+def lineInPlaneProp : ℚ × ℚ × ℚ → Prop := fun s =>
+  s.1 = s.2.1 ∨ s.1 = - s.2.1 ∨ 2 * s.2.2 + s.1 + s.2.1 = 0
+
+/-- The proposition on a `LinSol` to satisfy the `linInPlane` condition. -/
+def lineInPlaneCond (S : (PureU1 (n)).LinSols) : Prop :=
+  ∀ (i1 i2 i3 : Fin (n)) (_ : i1 ≠ i2) (_ : i2 ≠ i3) (_ : i1 ≠ i3),
+  lineInPlaneProp (S.val i1, (S.val i2, S.val i3))
+
+lemma lineInPlaneCond_perm {S : (PureU1 (n)).LinSols} (hS : lineInPlaneCond S)
+    (M : (FamilyPermutations n).group) :
+    lineInPlaneCond ((FamilyPermutations n).linSolRep M S) := by
+  intro i1 i2 i3 h1 h2 h3
+  rw [FamilyPermutations_anomalyFreeLinear_apply, FamilyPermutations_anomalyFreeLinear_apply,
+    FamilyPermutations_anomalyFreeLinear_apply]
+  refine hS (M.invFun i1) (M.invFun i2) (M.invFun i3) ?_ ?_ ?_
+  all_goals simp_all only [ne_eq, Equiv.invFun_as_coe, EmbeddingLike.apply_eq_iff_eq,
+    not_false_eq_true]
+
+
+lemma lineInPlaneCond_eq_last' {S : (PureU1 (n.succ.succ)).LinSols} (hS : lineInPlaneCond S)
+    (h : ¬ (S.val ((Fin.last n).castSucc))^2 = (S.val ((Fin.last n).succ))^2 ) :
+    (2 - n) * S.val (Fin.last (n + 1)) =
+    - (2 - n)* S.val (Fin.castSucc (Fin.last n)) := by
+  erw [sq_eq_sq_iff_eq_or_eq_neg] at h
+  rw [lineInPlaneCond] at hS
+  simp only [lineInPlaneProp] at hS
+  simp [not_or] at h
+  have h1 (i : Fin n) : S.val i.castSucc.castSucc =
+      - (S.val ((Fin.last n).castSucc) +  (S.val ((Fin.last n).succ))) / 2 := by
+    have h1S := hS (Fin.last n).castSucc ((Fin.last n).succ) i.castSucc.castSucc
+      (by simp; rw [Fin.ext_iff]; simp; omega)
+      (by simp; rw [Fin.ext_iff]; simp; omega)
+      (by simp; rw [Fin.ext_iff]; simp; omega)
+    simp_all
+    field_simp
+    linear_combination h1S
+  have h2 := pureU1_last S
+  rw [Fin.sum_univ_castSucc] at h2
+  simp [h1] at h2
+  field_simp at h2
+  linear_combination h2
+
+lemma lineInPlaneCond_eq_last {S : (PureU1 (n.succ.succ.succ.succ.succ)).LinSols}
+    (hS : lineInPlaneCond S) : constAbsProp ((S.val ((Fin.last n.succ.succ.succ).castSucc)),
+    (S.val ((Fin.last n.succ.succ.succ).succ))) := by
+  rw [constAbsProp]
+  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
+  have hx : ((2 : ℚ) - ↑(n + 3))  ≠ 0 := by
+    rw [Nat.cast_add]
+    simp only [Nat.cast_ofNat, ne_eq]
+    apply Not.intro
+    intro a
+    linarith
+  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
+    rw [h]
+    ring
+  simp_all
+
+lemma linesInPlane_eq_sq {S : (PureU1 (n.succ.succ.succ.succ.succ)).LinSols}
+    (hS : lineInPlaneCond S) : ∀ (i j : Fin n.succ.succ.succ.succ.succ) (_ : i ≠ j),
+    constAbsProp (S.val i, S.val j) := by
+  have hneq : ((Fin.last n.succ.succ.succ).castSucc) ≠ ((Fin.last n.succ.succ.succ).succ) := by
+    simp [Fin.ext_iff]
+  refine Prop_two constAbsProp hneq ?_
+  intro M
+  exact lineInPlaneCond_eq_last (lineInPlaneCond_perm hS M)
+
+theorem linesInPlane_constAbs {S : (PureU1 (n.succ.succ.succ.succ.succ)).LinSols}
+    (hS : lineInPlaneCond S) : constAbs S.val := by
+  intro i j
+  by_cases hij : i ≠ j
+  exact linesInPlane_eq_sq hS i j hij
+  simp at hij
+  rw [hij]
+
+lemma linesInPlane_four (S : (PureU1 4).Sols) (hS : lineInPlaneCond S.1.1) :
+    constAbsProp (S.val (0 : Fin 4), S.val (1 : Fin 4))  := by
+  simp [constAbsProp]
+  by_contra hn
+  have hLin := pureU1_linear S.1.1
+  have hcube := pureU1_cube S
+  simp 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
+  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)
+  simp_all [lineInPlaneProp]
+  have h1 : S.val (2 : Fin 4) = S.val (3 : Fin 4)  := by
+    linear_combination l012 / 2 + -1 * l013 / 2
+  by_cases h2 : S.val (0 : Fin 4) = S.val (2 : Fin 4)
+  simp_all
+  have h3 : S.val (1 : Fin 4) = - 3 * S.val (2 : Fin 4) := by
+    linear_combination l012 + 3 * h1
+  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
+  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
+    linear_combination l012 + h1
+  simp_all
+  simp_all
+  have h4 : S.val (0 : Fin 4) = - 3 * S.val (3 : Fin 4) := by
+    linear_combination l023
+  have h5 : S.val (1 : Fin 4) = S.val (3 : Fin 4) := by
+    linear_combination l013 - 1 * h4
+  rw [h4, h5] at hcube
+  have h6 : S.val (3 : Fin 4) ^ 3 = 0 := by
+    linear_combination -1 * hcube / 24
+  simp at h6
+  simp_all
+
+
+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) ?_
+  intro M
+  let S' := (FamilyPermutations 4).solAction.toFun S M
+  have hS' :  lineInPlaneCond S'.1.1 :=
+    (lineInPlaneCond_perm hS M)
+  exact linesInPlane_four S' hS'
+
+
+lemma linesInPlane_constAbs_four (S : (PureU1 4).Sols)
+    (hS : lineInPlaneCond S.1.1) : constAbs S.val := by
+  intro i j
+  by_cases hij : i ≠ j
+  exact linesInPlane_eq_sq_four hS i j hij
+  simp at hij
+  rw [hij]
+
+theorem linesInPlane_constAbs_AF (S : (PureU1 (n.succ.succ.succ.succ)).Sols)
+    (hS : lineInPlaneCond S.1.1) : constAbs S.val := by
+  induction n
+  exact linesInPlane_constAbs_four S hS
+  exact linesInPlane_constAbs hS
+
+
+end PureU1

HepLean/AnomalyCancellation/PureU1/LowDim/One.lean

@@ -0,0 +1,35 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.AnomalyCancellation.PureU1.Permutations
+/-!
+# The Pure U(1) case with 1 fermion
+
+We show that in this case the charge must be zero.
+-/
+
+universe v u
+
+open Nat
+open  Finset
+
+namespace PureU1
+
+variable {n : ℕ}
+
+namespace One
+
+theorem solEqZero (S : (PureU1 1).LinSols) : S = 0 := by
+  apply ACCSystemLinear.LinSols.ext
+  have hLin := pureU1_linear S
+  simp at hLin
+  funext i
+  simp at i
+  rw [show i = (0 : Fin 1) by omega]
+  exact hLin
+
+end One
+
+end PureU1

HepLean/AnomalyCancellation/PureU1/LowDim/Three.lean

@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.AnomalyCancellation.PureU1.Permutations
+/-!
+# The Pure U(1) case with 3 fermion
+
+We show that S is a solution only if one of its charges is zero.
+We define a surjective map from `LinSols` with a charge equal to zero to `Sols`.
+-/
+
+universe v u
+
+open Nat
+open  Finset
+
+namespace PureU1
+
+variable {n : ℕ}
+namespace Three
+
+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
+  rw [Fin.sum_univ_three] at hL
+  change _ ↔ accCube _ _ = _
+  rw [accCube_explicit, Fin.sum_univ_three]
+  rw [show S.val (0 : Fin 3) = - (S.val (1 : Fin 3) + S.val (2 : Fin 3)) by
+      linear_combination hL]
+  ring_nf
+
+lemma cube_for_linSol (S : (PureU1 3).LinSols) :
+    (S.val (0 : Fin 3) = 0 ∨ S.val (1 : Fin 3) = 0 ∨ S.val (2 : Fin 3) = 0) ↔
+    (PureU1 3).cubicACC S.val = 0 := by
+  rw [← cube_for_linSol']
+  simp only [Fin.isValue, _root_.mul_eq_zero, OfNat.ofNat_ne_zero, false_or]
+  rw [@or_assoc]
+
+lemma three_sol_zero (S : (PureU1 3).Sols) : S.val (0 : Fin 3) = 0 ∨ S.val (1 : Fin 3) = 0
+    ∨ S.val (2 : Fin 3) = 0 := (cube_for_linSol S.1.1).mpr S.cubicSol
+
+/-- Given a `LinSol` with a charge equal to zero a `Sol`.-/
+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⟩,
+    (cube_for_linSol S).mp hS⟩
+
+
+theorem solOfLinear_surjects (S : (PureU1 3).Sols) :
+    ∃ (T : (PureU1 3).LinSols) (hT : T.val (0 : Fin 3) = 0 ∨ T.val (1 : Fin 3) = 0
+    ∨ T.val (2 : Fin 3) = 0), solOfLinear T hT = S := by
+  use S.1.1
+  use (three_sol_zero S)
+  rfl
+
+end Three
+
+end PureU1

HepLean/AnomalyCancellation/PureU1/LowDim/Two.lean

@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.AnomalyCancellation.PureU1.Permutations
+/-!
+# The Pure U(1) case with 2 fermions
+
+We define an equivalence between `LinSols` and `Sols`.
+-/
+
+universe v u
+
+open Nat
+open  Finset
+
+namespace PureU1
+
+variable {n : ℕ}
+
+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
+    have hLin := pureU1_linear S
+    simp 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) by linear_combination hLin]
+    ring⟩
+  invFun S := S.1.1
+  left_inv S := rfl
+  right_inv S := rfl
+
+end Two
+
+end PureU1

HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean

@@ -0,0 +1,713 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.AnomalyCancellation.PureU1.Sort
+import HepLean.AnomalyCancellation.PureU1.BasisLinear
+import HepLean.AnomalyCancellation.PureU1.VectorLike
+import Mathlib.Logic.Equiv.Fin
+/-!
+# Basis of `LinSols` in the odd case
+
+We give a basis of `LinSols` in the odd case. This basis has the special propoerty
+that splits into two planes on which every point is a solution to the ACCs.
+-/
+universe v u
+
+open Nat
+open  Finset
+open BigOperators
+
+namespace PureU1
+
+variable {n : ℕ}
+
+
+namespace VectorLikeOddPlane
+
+lemma split_odd! (n : ℕ) : (1 + n) + n = 2 * n +1 := by
+  omega
+
+lemma split_adda (n : ℕ) : ((1+n)+1) + n.succ = 2 * n.succ + 1 := by
+  omega
+
+section theDeltas
+
+/-- A helper function for what follows. -/
+def δ₁ (j : Fin n) : Fin (2 * n + 1) :=
+  Fin.cast (split_odd n) (Fin.castAdd n (Fin.castAdd 1 j))
+
+/-- A helper function for what follows. -/
+def δ₂ (j : Fin n) : Fin (2 * n + 1) :=
+  Fin.cast (split_odd n) (Fin.natAdd (n+1) j)
+
+/-- A helper function for what follows. -/
+def δ₃ : Fin (2 * n + 1) :=
+  Fin.cast (split_odd n) (Fin.castAdd n (Fin.natAdd n 1))
+
+/-- A helper function for what follows. -/
+def δ!₁ (j : Fin n) : Fin (2 * n + 1) :=
+  Fin.cast (split_odd! n) (Fin.castAdd n (Fin.natAdd 1 j))
+
+/-- A helper function for what follows. -/
+def δ!₂ (j : Fin n) : Fin (2 * n + 1) :=
+  Fin.cast (split_odd! n) (Fin.natAdd (1 + n) j)
+
+/-- A helper function for what follows. -/
+def δ!₃ : Fin (2 * n + 1) :=
+  Fin.cast (split_odd! n) (Fin.castAdd n (Fin.castAdd n 1))
+
+/-- A helper function for what follows. -/
+def δa₁ : Fin (2 * n.succ + 1) :=
+  Fin.cast (split_adda n) (Fin.castAdd n.succ (Fin.castAdd 1 (Fin.castAdd n 1)))
+
+/-- A helper function for what follows. -/
+def δa₂ (j : Fin n) : Fin (2 * n.succ + 1) :=
+  Fin.cast (split_adda n) (Fin.castAdd n.succ (Fin.castAdd 1 (Fin.natAdd 1 j)))
+
+/-- A helper function for what follows. -/
+def δa₃ : Fin (2 * n.succ + 1) :=
+  Fin.cast (split_adda n) (Fin.castAdd n.succ (Fin.natAdd (1+n) 1))
+
+/-- A helper function for what follows. -/
+def δa₄ (j : Fin n.succ) : Fin (2 * n.succ + 1) :=
+  Fin.cast (split_adda n) (Fin.natAdd ((1+n)+1) j)
+
+lemma δa₁_δ₁ : @δa₁ n = δ₁ 0 := by
+  rfl
+
+lemma δa₁_δ!₃ : @δa₁ n = δ!₃ := by
+  rfl
+
+lemma δa₂_δ₁ (j : Fin n) : δa₂ j = δ₁ j.succ := by
+  rw [Fin.ext_iff]
+  simp [δa₂, δ₁]
+  omega
+
+lemma δa₂_δ!₁ (j : Fin n) : δa₂ j = δ!₁ j.castSucc := by
+  rw [Fin.ext_iff]
+  simp [δa₂, δ!₁]
+
+lemma δa₃_δ₃ : @δa₃ n = δ₃ := by
+  rw [Fin.ext_iff]
+  simp [δa₃, δ₃]
+  omega
+
+lemma δa₃_δ!₁ : δa₃ = δ!₁ (Fin.last n) := by
+  rfl
+
+lemma δa₄_δ₂ (j : Fin n.succ) : δa₄ j = δ₂ j := by
+  rw [Fin.ext_iff]
+  simp [δa₄, δ₂]
+  omega
+
+lemma δa₄_δ!₂ (j : Fin n.succ) : δa₄ j = δ!₂ j := by
+  rw [Fin.ext_iff]
+  simp [δa₄, δ!₂]
+  omega
+
+lemma δ₂_δ!₂ (j : Fin n) : δ₂ j = δ!₂ j := by
+  rw [Fin.ext_iff]
+  simp [δ₂, δ!₂]
+  omega
+
+lemma sum_δ  (S : Fin (2 * n + 1) → ℚ) :
+    ∑ i, S i = S δ₃ + ∑ i : Fin n, ((S ∘ δ₁) i + (S ∘ δ₂) i) := by
+  have h1 : ∑ i, S i = ∑ i : Fin (n + 1 + n), S (Fin.cast (split_odd n) i) := by
+    rw [Finset.sum_equiv (Fin.castIso (split_odd n)).symm.toEquiv]
+    intro i
+    simp only [mem_univ, Fin.symm_castIso, RelIso.coe_fn_toEquiv, Fin.castIso_apply]
+    intro i
+    simp
+  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]
+  nth_rewrite 2 [add_comm]
+  rw [add_assoc]
+  rw [Finset.sum_add_distrib]
+  rfl
+
+lemma sum_δ!  (S : Fin (2 * n + 1) → ℚ) :
+    ∑ i, S i = S δ!₃ + ∑ i : Fin n, ((S ∘ δ!₁) i + (S ∘ δ!₂) i) := by
+  have h1 : ∑ i, S i = ∑ i : Fin ((1+n)+n), S (Fin.cast (split_odd! n) i) := by
+    rw [Finset.sum_equiv (Fin.castIso (split_odd! n)).symm.toEquiv]
+    intro i
+    simp only [mem_univ, Fin.symm_castIso, RelIso.coe_fn_toEquiv, Fin.castIso_apply]
+    intro i
+    simp
+  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]
+  rw [add_assoc]
+  rw [Finset.sum_add_distrib]
+  rfl
+
+end theDeltas
+
+section theBasisVectors
+
+/-- The first part of the basis as charge assignments. -/
+def basisAsCharges (j : Fin n) : (PureU1 (2 * n + 1)).charges :=
+  fun i =>
+  if i = δ₁ j then
+    1
+  else
+    if i = δ₂ j then
+      - 1
+    else
+      0
+
+/-- The second part of the basis as charge assignments. -/
+def basis!AsCharges (j : Fin n) : (PureU1 (2 * n + 1)).charges :=
+  fun i =>
+  if i = δ!₁ j then
+    1
+  else
+    if i = δ!₂ j then
+      - 1
+    else
+      0
+
+lemma basis_on_δ₁_self (j : Fin n) : basisAsCharges j (δ₁ j) = 1 := by
+  simp [basisAsCharges]
+
+lemma basis!_on_δ!₁_self (j : Fin n) : basis!AsCharges j (δ!₁ j) = 1 := by
+  simp [basis!AsCharges]
+
+lemma basis_on_δ₁_other {k j : Fin n} (h : k ≠ j) :
+    basisAsCharges k (δ₁ j) = 0 := by
+  simp [basisAsCharges]
+  simp [δ₁, δ₂]
+  split
+  rename_i h1
+  rw [Fin.ext_iff] at h1
+  simp_all
+  rw [Fin.ext_iff] at h
+  simp_all
+  split
+  rename_i h1 h2
+  simp_all
+  rw [Fin.ext_iff] at h2
+  simp at h2
+  omega
+  rfl
+
+lemma basis!_on_δ!₁_other {k j : Fin n} (h : k ≠ j) :
+    basis!AsCharges k (δ!₁ j) = 0 := by
+  simp [basis!AsCharges]
+  simp [δ!₁, δ!₂]
+  split
+  rename_i h1
+  rw [Fin.ext_iff] at h1
+  simp_all
+  rw [Fin.ext_iff] at h
+  simp_all
+  split
+  rename_i h1 h2
+  simp_all
+  rw [Fin.ext_iff] at h2
+  simp at h2
+  omega
+  rfl
+
+lemma basis_on_other {k : Fin n} {j : Fin (2 * n + 1)} (h1 : j ≠ δ₁ k)  (h2 : j ≠ δ₂ k) :
+    basisAsCharges k j = 0 := by
+  simp [basisAsCharges]
+  simp_all only [ne_eq, ↓reduceIte]
+
+lemma basis!_on_other {k : Fin n} {j : Fin (2 * n + 1)} (h1 : j ≠ δ!₁ k)  (h2 : j ≠ δ!₂ k) :
+    basis!AsCharges k j = 0 := by
+  simp [basis!AsCharges]
+  simp_all only [ne_eq, ↓reduceIte]
+
+lemma basis_δ₂_eq_minus_δ₁ (j i : Fin n) :
+    basisAsCharges j (δ₂ i) = - basisAsCharges j (δ₁ i) := by
+  simp [basisAsCharges, δ₂, δ₁]
+  split <;> split
+  any_goals split
+  any_goals split
+  any_goals rfl
+  all_goals rename_i h1 h2
+  all_goals rw [Fin.ext_iff] at h1 h2
+  all_goals simp_all
+  all_goals rename_i h3
+  all_goals rw [Fin.ext_iff] at h3
+  all_goals simp_all
+  all_goals omega
+
+lemma basis!_δ!₂_eq_minus_δ!₁ (j i : Fin n) :
+    basis!AsCharges j (δ!₂ i) = - basis!AsCharges j (δ!₁ i) := by
+  simp [basis!AsCharges, δ!₂, δ!₁]
+  split <;> split
+  any_goals split
+  any_goals split
+  any_goals rfl
+  all_goals rename_i h1 h2
+  all_goals rw [Fin.ext_iff] at h1 h2
+  all_goals simp_all
+  subst h1
+  exact Fin.elim0 i
+  all_goals rename_i h3
+  all_goals rw [Fin.ext_iff] at h3
+  all_goals simp_all
+  all_goals omega
+
+lemma basis_on_δ₂_self (j : Fin n) : basisAsCharges j (δ₂ j) = - 1 := by
+  rw [basis_δ₂_eq_minus_δ₁, basis_on_δ₁_self]
+
+lemma basis!_on_δ!₂_self (j : Fin n) : basis!AsCharges j (δ!₂ j) = - 1 := by
+  rw [basis!_δ!₂_eq_minus_δ!₁, basis!_on_δ!₁_self]
+
+lemma basis_on_δ₂_other {k j : Fin n} (h : k ≠ j) : basisAsCharges k (δ₂ j) = 0 := by
+  rw [basis_δ₂_eq_minus_δ₁, basis_on_δ₁_other h]
+  rfl
+
+lemma basis!_on_δ!₂_other {k j : Fin n} (h : k ≠ j) : basis!AsCharges k (δ!₂ j) = 0 := by
+  rw [basis!_δ!₂_eq_minus_δ!₁, basis!_on_δ!₁_other h]
+  rfl
+
+lemma basis_on_δ₃ (j : Fin n) : basisAsCharges j δ₃ = 0 := by
+  simp [basisAsCharges]
+  split <;> rename_i h
+  rw [Fin.ext_iff] at h
+  simp [δ₃, δ₁] at h
+  omega
+  split <;> rename_i h2
+  rw [Fin.ext_iff] at h2
+  simp [δ₃, δ₂] at h2
+  omega
+  rfl
+
+lemma basis!_on_δ!₃ (j : Fin n) : basis!AsCharges j δ!₃ = 0 := by
+  simp [basis!AsCharges]
+  split <;> rename_i h
+  rw [Fin.ext_iff] at h
+  simp [δ!₃, δ!₁] at h
+  omega
+  split <;> rename_i h2
+  rw [Fin.ext_iff] at h2
+  simp [δ!₃, δ!₂] at h2
+  omega
+  rfl
+
+lemma basis_linearACC (j : Fin n) : (accGrav (2 * n + 1)) (basisAsCharges j) = 0 := by
+  rw [accGrav]
+  simp only [LinearMap.coe_mk, AddHom.coe_mk]
+  erw [sum_δ]
+  simp [basis_δ₂_eq_minus_δ₁, basis_on_δ₃]
+
+lemma basis!_linearACC (j : Fin n) : (accGrav (2 * n + 1)) (basis!AsCharges j) = 0 := by
+  rw [accGrav]
+  simp only [LinearMap.coe_mk, AddHom.coe_mk]
+  rw [sum_δ!, basis!_on_δ!₃]
+  simp [basis!_δ!₂_eq_minus_δ!₁]
+
+/-- The first part of the basis as `LinSols`. -/
+@[simps!]
+def basis (j : Fin n) : (PureU1 (2 * n + 1)).LinSols :=
+  ⟨basisAsCharges j, by
+    intro i
+    simp at i
+    match i with
+    | 0 =>
+    exact basis_linearACC j⟩
+
+/-- The second part of the basis as `LinSols`. -/
+@[simps!]
+def basis! (j : Fin n) : (PureU1 (2 * n + 1)).LinSols :=
+  ⟨basis!AsCharges j, by
+    intro i
+    simp at i
+    match i with
+    | 0 =>
+    exact basis!_linearACC j⟩
+
+/-- The whole basis as `LinSols`. -/
+def basisa : Fin n ⊕ Fin n → (PureU1 (2 * n + 1)).LinSols := fun i =>
+  match i with
+  | .inl i => basis i
+  | .inr i => basis! i
+
+end theBasisVectors
+
+/-- Swapping the elements δ!₁ j and δ!₂ j is equivalent to adding a vector basis!AsCharges j. -/
+lemma swap!_as_add {S S' : (PureU1 (2 * n + 1)).LinSols} (j : Fin n)
+    (hS : ((FamilyPermutations (2 * n + 1)).linSolRep
+    (pairSwap (δ!₁ j)  (δ!₂ j))) S = S') :
+    S'.val = S.val + (S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j := by
+  funext i
+  rw [← hS, FamilyPermutations_anomalyFreeLinear_apply]
+  by_cases  hi : i = δ!₁ j
+  subst hi
+  simp [HSMul.hSMul, basis!_on_δ!₁_self, pairSwap_inv_fst]
+  by_cases hi2 : i = δ!₂ j
+  subst hi2
+  simp [HSMul.hSMul,basis!_on_δ!₂_self, pairSwap_inv_snd]
+  simp [HSMul.hSMul]
+  rw [basis!_on_other hi hi2]
+  change  S.val ((pairSwap (δ!₁ j) (δ!₂ j)).invFun i) =_
+  erw [pairSwap_inv_other (Ne.symm hi) (Ne.symm hi2)]
+  simp
+
+/-- A point in the span of the first part of the basis as a charge. -/
+def P (f : Fin n → ℚ) : (PureU1 (2 * n + 1)).charges := ∑ i, f i • basisAsCharges i
+
+/-- A point in the span of the second part of the basis as a charge. -/
+def P! (f : Fin n → ℚ) : (PureU1 (2 * n + 1)).charges := ∑ i, f i • basis!AsCharges i
+
+/-- A point in the span of the basis as a charge. -/
+def Pa (f : Fin n → ℚ) (g : Fin n → ℚ) : (PureU1 (2 * n + 1)).charges := P f + P! g
+
+lemma P_δ₁ (f : Fin n → ℚ) (j : Fin n) : P f (δ₁ j) = f j := by
+  rw [P, sum_of_charges]
+  simp [HSMul.hSMul, SMul.smul]
+  rw [Finset.sum_eq_single j]
+  rw [basis_on_δ₁_self]
+  simp only [mul_one]
+  intro k _ hkj
+  rw [basis_on_δ₁_other hkj]
+  simp only [mul_zero]
+  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
+  rw [P!, sum_of_charges]
+  simp [HSMul.hSMul, SMul.smul]
+  rw [Finset.sum_eq_single j]
+  rw [basis!_on_δ!₁_self]
+  simp only [mul_one]
+  intro k _ hkj
+  rw [basis!_on_δ!₁_other hkj]
+  simp only [mul_zero]
+  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
+  rw [P, sum_of_charges]
+  simp [HSMul.hSMul, SMul.smul]
+  rw [Finset.sum_eq_single j]
+  rw [basis_on_δ₂_self]
+  simp only [mul_neg, mul_one]
+  intro k _ hkj
+  rw [basis_on_δ₂_other hkj]
+  simp only [mul_zero]
+  simp
+
+lemma P!_δ!₂ (f : Fin n → ℚ) (j : Fin n) : P! f (δ!₂ j) = - f j := by
+  rw [P!, sum_of_charges]
+  simp [HSMul.hSMul, SMul.smul]
+  rw [Finset.sum_eq_single j]
+  rw [basis!_on_δ!₂_self]
+  simp only [mul_neg, mul_one]
+  intro k _ hkj
+  rw [basis!_on_δ!₂_other hkj]
+  simp only [mul_zero]
+  simp
+
+lemma P_δ₃ (f : Fin n → ℚ) : P f (δ₃) = 0 := by
+  rw [P, sum_of_charges]
+  simp [HSMul.hSMul, SMul.smul, basis_on_δ₃]
+
+lemma P!_δ!₃ (f : Fin n → ℚ) : P! f (δ!₃) = 0 := by
+  rw [P!, sum_of_charges]
+  simp [HSMul.hSMul, SMul.smul, basis!_on_δ!₃]
+
+lemma Pa_δa₁ (f g : Fin n.succ → ℚ) : Pa f g δa₁ = f 0 := by
+  rw [Pa]
+  simp only [ACCSystemCharges.chargesAddCommMonoid_add]
+  nth_rewrite 1 [δa₁_δ₁]
+  rw [δa₁_δ!₃]
+  rw [P_δ₁, P!_δ!₃]
+  simp
+
+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]
+  simp only [ACCSystemCharges.chargesAddCommMonoid_add]
+  nth_rewrite 1 [δa₂_δ₁]
+  rw [δa₂_δ!₁]
+  rw [P_δ₁, P!_δ!₁]
+
+lemma Pa_δa₃ (f g : Fin n.succ → ℚ)  : Pa f g (δa₃) = g (Fin.last n) := by
+  rw [Pa]
+  simp only [ACCSystemCharges.chargesAddCommMonoid_add]
+  nth_rewrite 1 [δa₃_δ₃]
+  rw [δa₃_δ!₁]
+  rw [P_δ₃, P!_δ!₁]
+  simp
+
+lemma Pa_δa₄ (f g : Fin n.succ → ℚ) (j : Fin n.succ) : Pa f g (δa₄ j) = - f j - g j := by
+  rw [Pa]
+  simp only [ACCSystemCharges.chargesAddCommMonoid_add]
+  nth_rewrite 1 [δa₄_δ₂]
+  rw [δa₄_δ!₂]
+  rw [P_δ₂, P!_δ!₂]
+  ring
+
+lemma P_linearACC (f : Fin n → ℚ) : (accGrav (2 * n + 1)) (P f) = 0 := by
+  rw [accGrav]
+  simp only [LinearMap.coe_mk, AddHom.coe_mk]
+  rw [sum_δ]
+  simp [P_δ₂, P_δ₁, P_δ₃]
+
+lemma P!_linearACC (f : Fin n → ℚ) : (accGrav (2 * n + 1)) (P! f) = 0 := by
+  rw [accGrav]
+  simp only [LinearMap.coe_mk, AddHom.coe_mk]
+  rw [sum_δ!]
+  simp [P!_δ!₂, P!_δ!₁, P!_δ!₃]
+
+lemma P_accCube (f : Fin n → ℚ) : accCube (2 * n +1) (P f) = 0 := by
+  rw [accCube_explicit, sum_δ, P_δ₃]
+  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_δ₂]
+  ring
+
+lemma P!_accCube (f : Fin n → ℚ) : accCube (2 * n +1) (P! f) = 0 := by
+  rw [accCube_explicit, sum_δ!, P!_δ!₃]
+  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!_δ!₂]
+  ring
+
+lemma P_P_P!_accCube (g : Fin n → ℚ) (j : Fin n) :
+    accCubeTriLinSymm.toFun (P g, P g, basis!AsCharges j)
+    = (P g (δ!₁ j))^2 - (g j)^2 := by
+  simp [accCubeTriLinSymm]
+  rw [sum_δ!, basis!_on_δ!₃]
+  simp only [mul_zero, Function.comp_apply, zero_add]
+  rw [Finset.sum_eq_single j, basis!_on_δ!₁_self, basis!_on_δ!₂_self]
+  rw [← δ₂_δ!₂, P_δ₂]
+  ring
+  intro k _ hkj
+  erw [basis!_on_δ!₁_other hkj.symm, basis!_on_δ!₂_other hkj.symm]
+  simp only [mul_zero, add_zero]
+  simp
+
+
+lemma P_zero (f : Fin n → ℚ) (h : P f = 0) : ∀ i, f i = 0 := by
+  intro i
+  erw [← P_δ₁ f]
+  rw [h]
+  rfl
+
+lemma P!_zero (f : Fin n → ℚ) (h : P! f = 0) : ∀ i, f i = 0 := by
+  intro i
+  rw [← P!_δ!₁ f]
+  rw [h]
+  rfl
+
+lemma Pa_zero (f g : Fin n.succ → ℚ)  (h : Pa f g = 0) :
+    ∀ i, f i = 0 := by
+  have h₃ := Pa_δa₁ f g
+  rw [h] at h₃
+  change 0 = _ at h₃
+  simp at h₃
+  intro i
+  have hinduc (iv : ℕ) (hiv : iv < n.succ) : f ⟨iv, hiv⟩ = 0 := by
+    induction iv
+    exact h₃.symm
+    rename_i iv hi
+    have hivi : iv < n.succ := by omega
+    have hi2 := hi hivi
+    have h1 := Pa_δa₄ f g ⟨iv, hivi⟩
+    rw [h, hi2] at h1
+    change 0 = _ at h1
+    simp at h1
+    have h2 := Pa_δa₂ f g ⟨iv, by omega⟩
+    simp [h, h1] at h2
+    exact h2.symm
+  exact hinduc i.val i.prop
+
+lemma Pa_zero! (f g : Fin n.succ → ℚ) (h : Pa f g = 0) :
+    ∀ i, g i = 0 := by
+  have hf := Pa_zero f g h
+  rw [Pa, P] at h
+  simp [hf] at h
+  exact P!_zero g h
+
+/-- A point in the span of the first part of the basis. -/
+def P' (f : Fin n → ℚ) : (PureU1 (2 * n + 1)).LinSols := ∑ i, f i • basis i
+
+/-- A point in the span of the second part of the basis. -/
+def P!' (f : Fin n → ℚ) : (PureU1 (2 * n + 1)).LinSols := ∑ i, f i • basis! i
+
+/-- A point in the span of the whole basis. -/
+def Pa' (f : (Fin n) ⊕ (Fin n) → ℚ) : (PureU1 (2 * n + 1)).LinSols :=
+    ∑ i, f i • basisa i
+
+lemma Pa'_P'_P!' (f : (Fin n) ⊕ (Fin n) → ℚ) :
+    Pa' f = P' (f ∘ Sum.inl) + P!' (f ∘ Sum.inr):= by
+  exact Fintype.sum_sum_type _
+
+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]
+
+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]
+
+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
+  rw [P'_val] at h1
+  exact P_zero f h1
+
+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
+  rw [P!'_val] at h1
+  exact P!_zero f h1
+
+
+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
+  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
+  change Pa (f ∘ Sum.inl) (f ∘ Sum.inr) = 0 at h1
+  have hf := Pa_zero (f ∘ Sum.inl) (f ∘ Sum.inr) h1
+  have hg := Pa_zero! (f ∘ Sum.inl) (f ∘ Sum.inr) h1
+  intro i
+  simp_all
+  cases i
+  simp_all
+  simp_all
+
+lemma Pa'_eq (f f' : (Fin n.succ) ⊕ (Fin n.succ) → ℚ)  : Pa' f = Pa' f' ↔ f = f' := by
+  apply Iff.intro
+  intro h
+  funext i
+  rw [Pa', Pa'] at h
+  have h1 : ∑ i : Fin n.succ ⊕ Fin n.succ, (f i + (- f' i)) • basisa i = 0 := by
+    simp only [add_smul, neg_smul]
+    rw [Finset.sum_add_distrib]
+    rw [h]
+    rw [← Finset.sum_add_distrib]
+    simp
+  have h2 : ∀ i, (f i + (- f' i)) = 0 := by
+    exact Fintype.linearIndependent_iff.mp (@basisa_linear_independent (n))
+     (fun i => f i + -f' i) h1
+  have h2i := h2 i
+  linarith
+  intro h
+  rw [h]
+
+/-- A helper function for what follows. TODO: replace this with mathlib functions. -/
+def join (g f : Fin n → ℚ) :  Fin n ⊕ Fin n → ℚ := fun i =>
+  match i with
+  | .inl i => g i
+  | .inr i => f i
+
+lemma join_ext (g g' : Fin n → ℚ) (f f' : Fin n → ℚ) :
+    join g f = join g' f' ↔ g = g' ∧ f = f' := by
+  apply Iff.intro
+  intro h
+  apply And.intro
+  funext i
+  exact congr_fun h (Sum.inl i)
+  funext i
+  exact congr_fun h (Sum.inr i)
+  intro h
+  rw [h.left, h.right]
+
+lemma join_Pa (g g' : Fin n.succ → ℚ) (f f' : Fin n.succ → ℚ) :
+    Pa' (join g f) = Pa' (join g' f') ↔ Pa g f = Pa g' f' := by
+  apply Iff.intro
+  intro h
+  rw [Pa'_eq] at h
+  rw [join_ext] at h
+  rw [h.left, h.right]
+  intro h
+  apply ACCSystemLinear.LinSols.ext
+  rw [Pa'_P'_P!', Pa'_P'_P!']
+  simp [P'_val, P!'_val]
+  exact h
+
+lemma Pa_eq (g g' : Fin n.succ → ℚ) (f f' : Fin n.succ → ℚ) :
+    Pa g f = Pa g' f' ↔ g = g' ∧ f = f' := by
+  rw [← join_Pa]
+  rw [← join_ext]
+  exact Pa'_eq _ _
+
+
+
+lemma basisa_card :  Fintype.card ((Fin n.succ) ⊕ (Fin n.succ)) =
+    FiniteDimensional.finrank ℚ (PureU1 (2 * n.succ + 1)).LinSols := by
+  erw [BasisLinear.finrank_AnomalyFreeLinear]
+  simp only [Fintype.card_sum, Fintype.card_fin]
+  omega
+
+/-- The basis formed out of our basisa vectors. -/
+noncomputable def basisaAsBasis :
+    Basis (Fin n.succ ⊕ Fin n.succ) ℚ (PureU1 (2 * n.succ + 1)).LinSols :=
+  basisOfLinearIndependentOfCardEqFinrank (@basisa_linear_independent n) basisa_card
+
+lemma span_basis (S : (PureU1 (2 * n.succ + 1)).LinSols) :
+    ∃ (g f : Fin n.succ → ℚ) , S.val = P g + P! f  := by
+  have h := (mem_span_range_iff_exists_fun ℚ).mp (Basis.mem_span basisaAsBasis S)
+  obtain ⟨f, hf⟩ := h
+  simp [basisaAsBasis] at hf
+  change P' _ + P!' _ = S at hf
+  use f ∘ Sum.inl
+  use f ∘ Sum.inr
+  rw [← hf]
+  simp [P'_val, P!'_val]
+  rfl
+
+lemma span_basis_swap! {S : (PureU1 (2 * n.succ + 1)).LinSols} (j : Fin n.succ)
+    (hS : ((FamilyPermutations (2 * n.succ + 1)).linSolRep
+    (pairSwap (δ!₁ j) (δ!₂ j))) S = S') (g f : Fin n.succ → ℚ) (hS1 : S.val = P g + P! f):
+    ∃ (g' f' : Fin n.succ → ℚ),
+     S'.val = P g' + P! f' ∧ P! f' = P! f +
+    (S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j ∧ g' = g := by
+  let X := P! f + (S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j
+  have hf : P! f ∈ Submodule.span ℚ (Set.range basis!AsCharges) := by
+     rw [(mem_span_range_iff_exists_fun ℚ)]
+     use f
+     rfl
+  have hP : (S.val (δ!₂ j) - S.val (δ!₁ j)) • basis!AsCharges j ∈
+      Submodule.span ℚ (Set.range basis!AsCharges) := by
+    apply Submodule.smul_mem
+    apply SetLike.mem_of_subset
+    apply Submodule.subset_span
+    simp_all only [Set.mem_range, exists_apply_eq_apply]
+  have hX : X ∈  Submodule.span ℚ (Set.range (basis!AsCharges)) := by
+    apply Submodule.add_mem
+    exact hf
+    exact hP
+  have hXsum := (mem_span_range_iff_exists_fun ℚ).mp hX
+  obtain ⟨f', hf'⟩ := hXsum
+  use g
+  use f'
+  change P! f' = _ at hf'
+  erw [hf']
+  simp only [and_self, and_true]
+  change S'.val = P g + (P! f + _)
+  rw [← add_assoc, ← hS1]
+  apply swap!_as_add at hS
+  exact hS
+
+
+end VectorLikeOddPlane
+
+
+end PureU1

HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean

@@ -0,0 +1,173 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.AnomalyCancellation.PureU1.Basic
+import HepLean.AnomalyCancellation.PureU1.Permutations
+import HepLean.AnomalyCancellation.PureU1.VectorLike
+import HepLean.AnomalyCancellation.PureU1.ConstAbs
+import HepLean.AnomalyCancellation.PureU1.LineInPlaneCond
+import HepLean.AnomalyCancellation.PureU1.Odd.BasisLinear
+import Mathlib.Tactic.Polyrith
+import Mathlib.RepresentationTheory.Basic
+/-!
+
+# Line In Cubic Odd case
+
+We say that a linear solution satisfies the `lineInCubic` property
+if the line through that point and through the two different planes formed by the baisis of
+`LinSols` lies in the cubic.
+
+We show that for a solution all its permutations satsfiy this property,
+then the charge must be zero.
+
+The main reference for this file is:
+
+- https://arxiv.org/pdf/1912.04804.pdf
+-/
+namespace PureU1
+namespace Odd
+
+open BigOperators
+
+variable {n : ℕ}
+open VectorLikeOddPlane
+
+/-- A  property on `LinSols`, statified if every point on the line between the two planes
+in the basis through that point is in the cubic. -/
+def lineInCubic (S : (PureU1 (2 * n + 1)).LinSols) : Prop :=
+  ∀ (g f : Fin n → ℚ)  (_ : S.val = Pa g f) (a b : ℚ) ,
+  accCube (2 * n + 1) (a • P g + b • P! f) = 0
+
+lemma lineInCubic_expand {S : (PureU1 (2 * n + 1)).LinSols} (h : lineInCubic S) :
+    ∀ (g : Fin n → ℚ) (f : Fin n → ℚ) (_ : S.val = P g + P! f) (a b : ℚ) ,
+    3 * a * b * (a * accCubeTriLinSymm (P g, P g, P! f)
+    + b * accCubeTriLinSymm (P! f, P! f, P g)) = 0 := by
+  intro g f hS a b
+  have h1 := h g f hS a b
+  change accCubeTriLinSymm.toCubic (a • P g + b • P! f) = 0 at h1
+  simp only [TriLinearSymm.toCubic_add] at h1
+  simp only [HomogeneousCubic.map_smul,
+   accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂, accCubeTriLinSymm.map_smul₃] at h1
+  erw [P_accCube, P!_accCube] at h1
+  rw [← h1]
+  ring
+
+
+lemma line_in_cubic_P_P_P! {S : (PureU1 (2 * n + 1)).LinSols} (h : lineInCubic S) :
+    ∀ (g : Fin n → ℚ) (f : Fin n → ℚ) (_ : S.val =  P g + P! f),
+    accCubeTriLinSymm (P g, P g, P! f) = 0 := by
+  intro g f hS
+  linear_combination 2 / 3 * (lineInCubic_expand h g f hS 1 1 ) -
+     (lineInCubic_expand h g f hS 1 2 ) / 6
+
+
+
+/-- We say a `LinSol` satifies  `lineInCubicPerm` if all its permutations satsify `lineInCubic`. -/
+def lineInCubicPerm (S : (PureU1 (2 * n + 1)).LinSols) : Prop :=
+  ∀ (M : (FamilyPermutations (2 * n + 1)).group ),
+    lineInCubic ((FamilyPermutations (2 * n + 1)).linSolRep M S)
+
+/-- If `lineInCubicPerm S` then `lineInCubic S`.  -/
+lemma lineInCubicPerm_self {S : (PureU1 (2 * n + 1)).LinSols} (hS : lineInCubicPerm S) :
+    lineInCubic S := hS 1
+
+/-- 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')
+
+
+lemma lineInCubicPerm_swap {S : (PureU1 (2 * n.succ + 1)).LinSols}
+    (LIC : lineInCubicPerm S) :
+    ∀ (j : Fin n.succ) (g f : Fin n.succ → ℚ) (_ : S.val = Pa g f) ,
+      (S.val (δ!₂ j) - S.val (δ!₁ j))
+      * accCubeTriLinSymm.toFun (P g, P g, basis!AsCharges j) = 0 := by
+  intro j g f h
+  let S' :=  (FamilyPermutations (2 * n.succ + 1)).linSolRep
+    (pairSwap (δ!₁ j) (δ!₂ j)) S
+  have hSS' : ((FamilyPermutations (2 * n.succ + 1)).linSolRep
+    (pairSwap (δ!₁ j) (δ!₂ 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
+  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 + 1)).LinSols}
+    (f g : Fin n.succ.succ → ℚ) (hS : S.val = Pa f g) :
+    accCubeTriLinSymm.toFun (P f, P f, basis!AsCharges 0) =
+    (S.val (δ!₁ 0) + S.val (δ!₂ 0)) * (2 * S.val δ!₃ + S.val (δ!₁ 0) + S.val (δ!₂ 0)) := by
+  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
+  nth_rewrite 1 [ht]
+  rw [P_δ₁]
+  have h1 := Pa_δa₁ f g
+  have h4 := Pa_δa₄ f g 0
+  have h2 := Pa_δa₂ f g 0
+  rw [← hS] at h1 h2 h4
+  simp 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]
+  rw [δa₄_δ!₂]
+  have h0 : (δa₂ (0 : Fin n.succ)) = δ!₁ 0 := by
+    rw [δa₂_δ!₁]
+    simp
+  rw [h0, δa₁_δ!₃]
+  ring
+
+lemma lineInCubicPerm_last_cond {S : (PureU1 (2 * n.succ.succ+1)).LinSols}
+    (LIC : lineInCubicPerm S) :
+    lineInPlaneProp ((S.val (δ!₂ 0)), ((S.val (δ!₁ 0)), (S.val δ!₃))) := by
+  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
+  cases h1 <;> rename_i h1
+  apply Or.inl
+  linear_combination h1
+  cases h1 <;> rename_i h1
+  apply Or.inr
+  apply Or.inl
+  linear_combination h1
+  apply Or.inr
+  apply Or.inr
+  linear_combination h1
+
+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, δ!₁, δ!₃]
+  intro M
+  exact lineInCubicPerm_last_cond (lineInCubicPerm_permute LIC M)
+
+lemma lineInCubicPerm_constAbs  {S : (PureU1 (2 * n.succ.succ + 1)).LinSols}
+    (LIC : lineInCubicPerm S) : constAbs S.val :=
+  linesInPlane_constAbs (lineInCubicPerm_last_perm LIC)
+
+theorem  lineInCubicPerm_zero {S : (PureU1 (2 * n.succ.succ + 1)).LinSols}
+    (LIC : lineInCubicPerm S) : S = 0 :=
+  ConstAbs.boundary_value_odd S (lineInCubicPerm_constAbs LIC)
+
+end Odd
+end PureU1

HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean

@@ -0,0 +1,171 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.AnomalyCancellation.PureU1.Basic
+import HepLean.AnomalyCancellation.PureU1.Permutations
+import HepLean.AnomalyCancellation.PureU1.VectorLike
+import HepLean.AnomalyCancellation.PureU1.ConstAbs
+import HepLean.AnomalyCancellation.PureU1.LineInPlaneCond
+import HepLean.AnomalyCancellation.PureU1.Odd.LineInCubic
+import Mathlib.Tactic.Polyrith
+import Mathlib.RepresentationTheory.Basic
+/-!
+# Parameterization in odd case
+
+Given maps `g : Fin n → ℚ`,  `f : Fin n → ℚ` and `a : ℚ` we form a solution to the anomaly
+equations. We show that every solution can be got in this way, up to permutation, unless it is zero.
+
+The main reference is:
+
+- https://arxiv.org/pdf/1912.04804.pdf
+
+-/
+namespace PureU1
+namespace Odd
+open BigOperators
+
+variable {n : ℕ}
+open VectorLikeOddPlane
+
+/-- Given a `g f : Fin n → ℚ` and a `a : ℚ` we form a linear solution. We will later
+show that this can be extended to a complete solution. -/
+def parameterizationAsLinear (g f : Fin n → ℚ)  (a : ℚ) :
+    (PureU1 (2 * n + 1)).LinSols :=
+  a • ((accCubeTriLinSymm (P! f, P! f, P g)) • P' g +
+  (- accCubeTriLinSymm (P g, P g, P! f)) • P!' f)
+
+lemma parameterizationAsLinear_val (g f : Fin n → ℚ) (a : ℚ) :
+    (parameterizationAsLinear g f a).val =
+    a • ((accCubeTriLinSymm (P! f, P! f, P g)) • P g +
+    (- accCubeTriLinSymm (P g, P g, P! f)) • P! f) := by
+  rw [parameterizationAsLinear]
+  change a • (_ • (P' g).val + _ • (P!' f).val) = _
+  rw [P'_val, P!'_val]
+
+lemma parameterizationCharge_cube (g f : Fin n → ℚ)  (a : ℚ):
+    (accCube (2 * n + 1)) (parameterizationAsLinear g f a).val = 0 := by
+  change accCubeTriLinSymm.toCubic _ = 0
+  rw [parameterizationAsLinear_val]
+  rw [HomogeneousCubic.map_smul]
+  rw [TriLinearSymm.toCubic_add]
+  rw [HomogeneousCubic.map_smul, HomogeneousCubic.map_smul]
+  erw [P_accCube g, P!_accCube f]
+  rw [accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂,
+   accCubeTriLinSymm.map_smul₃, accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂,
+   accCubeTriLinSymm.map_smul₃]
+  ring
+
+/-- Given a `g f : Fin n → ℚ` and a `a : ℚ` we form a solution. -/
+def parameterization (g f : Fin n → ℚ) (a : ℚ) :
+    (PureU1 (2 * n + 1)).Sols :=
+  ⟨⟨parameterizationAsLinear g f a, by intro i; simp at i; exact Fin.elim0 i⟩,
+  parameterizationCharge_cube g f a⟩
+
+lemma anomalyFree_param {S : (PureU1 (2 * n + 1)).Sols}
+    (g f : Fin n → ℚ)  (hS : S.val = P g + P! f) :
+    accCubeTriLinSymm (P g, P g, P! f) =
+    - accCubeTriLinSymm (P! f, P! f, P g) := by
+  have hC := S.cubicSol
+  rw [hS] at hC
+  change (accCube (2 * n + 1)) (P g + P! f) = 0 at hC
+  erw [TriLinearSymm.toCubic_add] at hC
+  erw [P_accCube] at hC
+  erw [P!_accCube] at hC
+  linear_combination hC / 3
+
+/-- A proposition on a solution which is true if `accCubeTriLinSymm (P g, P g, P! f) ≠  0`.
+In this case our parameterization above will be able to recover this point. -/
+def genericCase (S : (PureU1 (2 * n.succ + 1)).Sols) : Prop :=
+  ∀ (g f : Fin n.succ → ℚ)  (_ : S.val = P g + P! f) ,
+  accCubeTriLinSymm (P g, P g, P! f) ≠  0
+
+lemma genericCase_exists (S : (PureU1 (2 * n.succ + 1)).Sols)
+    (hs : ∃ (g f : Fin n.succ → ℚ), S.val = P g + P! f ∧
+    accCubeTriLinSymm (P g, P g, P! f) ≠  0) : genericCase S := by
+  intro g f hS hC
+  obtain ⟨g', f', hS', hC'⟩ := hs
+  rw [hS] at hS'
+  erw [Pa_eq] at hS'
+  rw [hS'.1, hS'.2] at hC
+  exact hC' hC
+
+/-- A proposition on a solution which is true if `accCubeTriLinSymm (P g, P g, P! f) ≠  0`.
+In this case we will show that S is zero if it is true for all permutations. -/
+def specialCase  (S : (PureU1 (2 * n.succ + 1)).Sols) : Prop :=
+  ∀ (g f : Fin n.succ → ℚ) (_ : S.val = P g + P! f) ,
+  accCubeTriLinSymm (P g, P g, P! f) = 0
+
+lemma specialCase_exists (S : (PureU1 (2 * n.succ + 1)).Sols)
+    (hs : ∃ (g f : Fin n.succ → ℚ), S.val = P g + P! f ∧
+    accCubeTriLinSymm (P g, P g, P! f) =  0) : specialCase S := by
+  intro g f hS
+  obtain ⟨g', f', hS', hC'⟩ := hs
+  rw [hS] at hS'
+  erw [Pa_eq] at hS'
+  rw [hS'.1, hS'.2]
+  exact hC'
+
+lemma generic_or_special (S : (PureU1 (2 * n.succ + 1)).Sols) :
+    genericCase S ∨ specialCase S := by
+  obtain ⟨g, f, h⟩ := span_basis S.1.1
+  have h1 :  accCubeTriLinSymm (P g, P g, P! f) ≠  0 ∨
+     accCubeTriLinSymm (P g, P g, P! f) = 0 := by
+    exact ne_or_eq _ _
+  cases h1 <;> rename_i h1
+  exact Or.inl (genericCase_exists S ⟨g, f, h, h1⟩)
+  exact Or.inr (specialCase_exists S ⟨g, f, h, h1⟩)
+
+theorem generic_case {S : (PureU1 (2 * n.succ + 1)).Sols} (h : genericCase S) :
+    ∃ g f a,  S = parameterization g f a := by
+  obtain ⟨g, f, hS⟩ := span_basis S.1.1
+  use g, f, (accCubeTriLinSymm (P! f, P! f, P g))⁻¹
+  rw [parameterization]
+  apply ACCSystem.Sols.ext
+  rw [parameterizationAsLinear_val]
+  change S.val = _ • ( _ • P g + _• P! f)
+  rw [anomalyFree_param _ _ hS]
+  rw [neg_neg, ← smul_add, smul_smul, inv_mul_cancel, one_smul]
+  exact hS
+  have h := h g f hS
+  rw [anomalyFree_param _ _ hS] at h
+  simp at h
+  exact h
+
+
+lemma special_case_lineInCubic {S : (PureU1 (2 * n.succ + 1)).Sols}
+    (h : specialCase S) :
+      lineInCubic S.1.1 := by
+  intro g f hS a b
+  erw [TriLinearSymm.toCubic_add]
+  rw [HomogeneousCubic.map_smul, HomogeneousCubic.map_smul]
+  erw [P_accCube]
+  erw [P!_accCube]
+  have h := h g f hS
+  rw [accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂,
+   accCubeTriLinSymm.map_smul₃, accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂,
+   accCubeTriLinSymm.map_smul₃]
+  rw [h]
+  rw [anomalyFree_param _ _ hS] at h
+  simp at h
+  change accCubeTriLinSymm (P! f, P! f, P g) = 0 at h
+  erw [h]
+  simp
+
+lemma special_case_lineInCubic_perm {S : (PureU1 (2 * n.succ + 1)).Sols}
+    (h : ∀ (M : (FamilyPermutations (2 * n.succ + 1)).group),
+    specialCase ((FamilyPermutations (2 * n.succ + 1)).solAction.toFun S M)) :
+    lineInCubicPerm S.1.1 := by
+  intro M
+  have hM := special_case_lineInCubic (h M)
+  exact hM
+
+theorem special_case {S : (PureU1 (2 * n.succ.succ + 1)).Sols}
+    (h : ∀ (M : (FamilyPermutations (2 * n.succ.succ + 1)).group),
+    specialCase ((FamilyPermutations (2 * n.succ.succ + 1)).solAction.toFun S M)) :
+    S.1.1 = 0 := by
+  have ht :=  special_case_lineInCubic_perm h
+  exact lineInCubicPerm_zero ht
+end Odd
+end PureU1

HepLean/AnomalyCancellation/PureU1/Permutations.lean

@@ -0,0 +1,343 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.AnomalyCancellation.PureU1.Basic
+import HepLean.AnomalyCancellation.GroupActions
+import Mathlib.Tactic.Polyrith
+import Mathlib.RepresentationTheory.Basic
+import Mathlib.Data.Fin.Tuple.Sort
+/-!
+# Permutations of Pure U(1) ACC
+
+We define the permutation group action on the charges of the Pure U(1) ACC system.
+We further define the action on the ACC System.
+
+-/
+
+universe v u
+
+open Nat
+open  Finset
+
+namespace PureU1
+
+/-- The permutation group of the n-fermions. -/
+@[simp]
+def permGroup (n  : ℕ) := Equiv.Perm (Fin n)
+
+instance {n : ℕ} : Group (permGroup n) := by
+  simp [permGroup]
+  infer_instance
+
+section Charges
+
+/-- The image of an element of `permGroup` under the representation on charges. -/
+@[simps!]
+def chargeMap {n : ℕ} (f : permGroup n) :
+    (PureU1 n).charges  →ₗ[ℚ] (PureU1 n).charges where
+  toFun S := S ∘ f.toFun
+  map_add' S T := by
+    funext i
+    simp
+  map_smul' a S := by
+    funext i
+    simp [HSMul.hSMul]
+    -- rw [show Rat.cast a = a from rfl]
+
+open PureU1Charges in
+
+/-- The representation of `permGroup` acting on the vector space of charges. -/
+@[simp]
+def permCharges {n : ℕ} : Representation ℚ (permGroup n) (PureU1 n).charges where
+  toFun f := chargeMap f⁻¹
+  map_mul' f g :=by
+    simp only [permGroup, mul_inv_rev]
+    apply LinearMap.ext
+    intro S
+    funext i
+    rfl
+  map_one' := by
+    apply LinearMap.ext
+    intro S
+    funext i
+    rfl
+
+lemma accGrav_invariant {n : ℕ} (f : (permGroup n)) (S : (PureU1 n).charges) :
+    PureU1.accGrav n (permCharges f S) = accGrav n S := by
+  simp [accGrav, permCharges]
+  apply (Equiv.Perm.sum_comp _ _ _ ?_)
+  simp
+
+open BigOperators
+lemma accCube_invariant {n : ℕ} (f : (permGroup n)) (S : (PureU1 n).charges) :
+    accCube n (permCharges f S) = accCube n S := by
+  rw [accCube_explicit, accCube_explicit]
+  change  ∑ i : Fin n, ((((fun a => a^3) ∘ S) (f.symm i))) = _
+  apply (Equiv.Perm.sum_comp _ _ _ ?_)
+  simp
+
+end Charges
+
+/-- The permutations acting on the ACC system. -/
+@[simp]
+def FamilyPermutations (n : ℕ) : ACCSystemGroupAction (PureU1 n) where
+  group := permGroup n
+  groupInst := inferInstance
+  rep := permCharges
+  linearInvariant := by
+    intro i
+    simp at i
+    match i with
+    | 0 => exact accGrav_invariant
+  quadInvariant := by
+    intro i
+    simp at i
+    exact Fin.elim0 i
+  cubicInvariant := accCube_invariant
+
+
+lemma FamilyPermutations_charges_apply (S : (PureU1 n).charges)
+    (i : Fin n) (f : (FamilyPermutations n).group) :
+    ((FamilyPermutations n).rep f S) i = S (f.invFun i) := by
+  rfl
+
+lemma FamilyPermutations_anomalyFreeLinear_apply (S : (PureU1 n).LinSols)
+    (i : Fin n) (f : (FamilyPermutations n).group) :
+    ((FamilyPermutations n).linSolRep f S).val i = S.val (f.invFun i) := by
+  rfl
+
+
+/-- The permutation which swaps i and j. TODO: Replace with: `Equiv.swap`. -/
+def pairSwap {n : ℕ} (i j : Fin n) : (FamilyPermutations n).group where
+  toFun s :=
+    if s = i then
+        j
+    else
+      if s = j then
+        i
+      else
+        s
+  invFun s :=
+    if s = i then
+        j
+    else
+      if s = j then
+        i
+      else
+        s
+  left_inv s := by
+    aesop
+  right_inv s := by
+    aesop
+
+lemma pairSwap_self_inv {n : ℕ} (i j : Fin n) :  (pairSwap i j)⁻¹ =  (pairSwap i j) := by
+  rfl
+
+lemma pairSwap_fst {n : ℕ} (i j : Fin n) : (pairSwap i j).toFun i  = j := by
+  simp [pairSwap]
+
+lemma pairSwap_snd {n : ℕ} (i j : Fin n) : (pairSwap i j).toFun j  = i := by
+  simp [pairSwap]
+
+lemma pairSwap_inv_fst {n : ℕ} (i j : Fin n) : (pairSwap i j).invFun i  = j := by
+  simp [pairSwap]
+
+lemma pairSwap_inv_snd {n : ℕ} (i j : Fin n) : (pairSwap i j).invFun j  = i := by
+  simp [pairSwap]
+
+lemma pairSwap_other  {n : ℕ} (i j k : Fin n) (hik : i ≠ k)  (hjk : j ≠ k) :
+    (pairSwap i j).toFun k = k := by
+  simp [pairSwap]
+  split
+  simp_all
+  split
+  simp_all
+  rfl
+
+lemma pairSwap_inv_other  {n : ℕ} {i j k : Fin n} (hik : i ≠ k)  (hjk : j ≠ k) :
+    (pairSwap i j).invFun k = k := by
+  simp [pairSwap]
+  split
+  simp_all
+  split
+  simp_all
+  rfl
+
+/-- A permutation of fermions which takes one ordered subset into another. -/
+noncomputable def permOfInjection (f g : Fin m ↪  Fin n) : (FamilyPermutations n).group :=
+  Equiv.extendSubtype (g.toEquivRange.symm.trans f.toEquivRange)
+
+section permTwo
+
+variable {i j  i' j'  : Fin n} (hij : i ≠ j)  (hij' : i' ≠ j')
+
+/-- Given two distinct elements, an embedding of `Fin 2` into `Fin n`. -/
+def permTwoInj : Fin 2 ↪ Fin n where
+  toFun s := match s with
+    | 0 => i
+    | 1 => j
+  inj' s1 s2 := by
+    aesop
+
+lemma permTwoInj_fst : i ∈ Set.range ⇑(permTwoInj hij) := by
+  simp only [Set.mem_range]
+  use 0
+  rfl
+
+lemma permTwoInj_fst_apply :
+    (Function.Embedding.toEquivRange (permTwoInj hij)).symm ⟨i, permTwoInj_fst  hij⟩ = 0 := by
+  exact (Equiv.symm_apply_eq (Function.Embedding.toEquivRange (permTwoInj hij))).mpr rfl
+
+lemma permTwoInj_snd : j ∈ Set.range ⇑(permTwoInj hij) := by
+  simp only [Set.mem_range]
+  use 1
+  rfl
+
+lemma permTwoInj_snd_apply :
+    (Function.Embedding.toEquivRange (permTwoInj hij)).symm
+    ⟨j, permTwoInj_snd  hij⟩ = 1 := by
+  exact (Equiv.symm_apply_eq (Function.Embedding.toEquivRange (permTwoInj hij))).mpr rfl
+
+/-- A permutation which swaps `i` with `i'` and `j` with `j'`. -/
+noncomputable def permTwo : (FamilyPermutations n).group :=
+  permOfInjection (permTwoInj hij)  (permTwoInj hij')
+
+lemma permTwo_fst : (permTwo hij hij').toFun i' = i := by
+  rw [permTwo, permOfInjection]
+  have ht := Equiv.extendSubtype_apply_of_mem
+    ((permTwoInj hij').toEquivRange.symm.trans
+    (permTwoInj hij).toEquivRange) i' (permTwoInj_fst hij')
+  simp at ht
+  simp [ht, permTwoInj_fst_apply]
+  rfl
+
+lemma permTwo_snd : (permTwo hij hij').toFun j' = j := by
+  rw [permTwo, permOfInjection]
+  have ht := Equiv.extendSubtype_apply_of_mem
+    ((permTwoInj hij' ).toEquivRange.symm.trans
+    (permTwoInj hij).toEquivRange) j' (permTwoInj_snd hij')
+  simp at ht
+  simp [ht, permTwoInj_snd_apply]
+  rfl
+
+end permTwo
+
+section permThree
+
+variable {i j k i' j' k' : Fin n} (hij : i ≠ j) (hjk : j ≠ k) (hik : i ≠ k) (hij' : i' ≠ j')
+  (hjk' : j' ≠ k') (hik' : i' ≠ k')
+
+/-- Given three distinct elements an embedding of `Fin 3` into `Fin n`. -/
+def permThreeInj : Fin 3 ↪ Fin n where
+  toFun s := match s with
+    | 0 => i
+    | 1 => j
+    | 2 => k
+  inj' s1 s2 := by
+    aesop
+
+lemma permThreeInj_fst : i ∈ Set.range ⇑(permThreeInj hij hjk hik) := by
+  simp only [Set.mem_range]
+  use 0
+  rfl
+
+lemma permThreeInj_fst_apply :
+    (Function.Embedding.toEquivRange (permThreeInj hij hjk hik)).symm
+    ⟨i, permThreeInj_fst  hij hjk hik⟩ = 0 := by
+  exact (Equiv.symm_apply_eq (Function.Embedding.toEquivRange (permThreeInj hij hjk hik))).mpr rfl
+
+
+lemma permThreeInj_snd : j ∈ Set.range ⇑(permThreeInj hij hjk hik) := by
+  simp only [Set.mem_range]
+  use 1
+  rfl
+
+lemma permThreeInj_snd_apply :
+    (Function.Embedding.toEquivRange (permThreeInj hij hjk hik)).symm
+    ⟨j, permThreeInj_snd  hij hjk hik⟩ = 1 := by
+  exact (Equiv.symm_apply_eq (Function.Embedding.toEquivRange (permThreeInj hij hjk hik))).mpr rfl
+
+lemma permThreeInj_thd : k ∈ Set.range ⇑(permThreeInj hij hjk hik) := by
+  simp only [Set.mem_range]
+  use 2
+  rfl
+
+lemma permThreeInj_thd_apply :
+    (Function.Embedding.toEquivRange (permThreeInj hij hjk hik)).symm
+    ⟨k, permThreeInj_thd hij hjk hik⟩ = 2 := by
+  exact (Equiv.symm_apply_eq (Function.Embedding.toEquivRange (permThreeInj hij hjk hik))).mpr rfl
+
+/-- A permutation which swaps three distinct elements with another three. -/
+noncomputable def permThree : (FamilyPermutations n).group :=
+  permOfInjection (permThreeInj hij hjk hik)  (permThreeInj hij' hjk' hik')
+
+lemma permThree_fst : (permThree hij hjk hik hij' hjk' hik').toFun i' = i := by
+  rw [permThree, permOfInjection]
+  have ht := Equiv.extendSubtype_apply_of_mem
+    ((permThreeInj hij' hjk' hik').toEquivRange.symm.trans
+    (permThreeInj hij hjk hik).toEquivRange) i' (permThreeInj_fst hij' hjk' hik')
+  simp at ht
+  simp [ht, permThreeInj_fst_apply]
+  rfl
+
+lemma permThree_snd : (permThree hij hjk hik hij' hjk' hik').toFun j' = j := by
+  rw [permThree, permOfInjection]
+  have ht := Equiv.extendSubtype_apply_of_mem
+    ((permThreeInj hij' hjk' hik').toEquivRange.symm.trans
+    (permThreeInj hij hjk hik).toEquivRange) j' (permThreeInj_snd hij' hjk' hik')
+  simp at ht
+  simp [ht, permThreeInj_snd_apply]
+  rfl
+
+lemma permThree_thd : (permThree hij hjk hik hij' hjk' hik').toFun k' = k := by
+  rw [permThree, permOfInjection]
+  have ht := Equiv.extendSubtype_apply_of_mem
+    ((permThreeInj hij' hjk' hik').toEquivRange.symm.trans
+    (permThreeInj hij hjk hik).toEquivRange) k' (permThreeInj_thd hij' hjk' hik')
+  simp at ht
+  simp [ht, permThreeInj_thd_apply]
+  rfl
+
+end permThree
+
+lemma Prop_two (P : ℚ × ℚ → Prop) {S : (PureU1 n).LinSols}
+    {a b : Fin n} (hab : a ≠ b)
+    (h : ∀ (f : (FamilyPermutations n).group),
+    P ((((FamilyPermutations n).linSolRep f S).val a),
+      (((FamilyPermutations n).linSolRep f S).val b)
+    )) : ∀ (i j : Fin n) (_ : i ≠ j),
+    P (S.val i, S.val j) := by
+  intro i j hij
+  have h1 := h (permTwo hij hab ).symm
+  rw [FamilyPermutations_anomalyFreeLinear_apply, FamilyPermutations_anomalyFreeLinear_apply] at h1
+  simp at h1
+  change  P
+   (S.val ((permTwo hij hab ).toFun a),
+   S.val ((permTwo hij hab ).toFun b)) at h1
+  erw [permTwo_fst,permTwo_snd] at h1
+  exact h1
+
+lemma Prop_three (P : ℚ × ℚ × ℚ → Prop) {S : (PureU1 n).LinSols}
+    {a b c : Fin n} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c)
+    (h : ∀ (f : (FamilyPermutations n).group),
+    P ((((FamilyPermutations n).linSolRep f S).val a),(
+      (((FamilyPermutations n).linSolRep f S).val b),
+      (((FamilyPermutations n).linSolRep f S).val c)
+    ))) : ∀ (i j k : Fin n) (_ : i ≠ j) (_ : j ≠ k)  (_ : i ≠ k),
+    P (S.val i, (S.val j, S.val k)) := by
+  intro i j k hij hjk hik
+  have h1 := h (permThree hij hjk hik hab hbc hac).symm
+  rw [FamilyPermutations_anomalyFreeLinear_apply, FamilyPermutations_anomalyFreeLinear_apply,
+   FamilyPermutations_anomalyFreeLinear_apply] at h1
+  simp at h1
+  change  P
+   (S.val ((permThree hij hjk hik hab hbc hac).toFun a),
+   S.val ((permThree hij hjk hik hab hbc hac).toFun b),
+    S.val ((permThree hij hjk hik hab hbc hac).toFun c)) at h1
+  erw [permThree_fst,permThree_snd, permThree_thd] at h1
+  exact h1
+
+
+end PureU1

HepLean/AnomalyCancellation/PureU1/Sort.lean

@@ -0,0 +1,78 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.AnomalyCancellation.PureU1.Permutations
+/-!
+# Sort for Pure U(1) charges
+
+We define the sort function for Pure U(1) charges, and prove some basic properties.
+
+-/
+
+universe v u
+
+open Nat
+open  Finset
+
+namespace PureU1
+
+variable {n : ℕ}
+
+/-- We say a charge is shorted if for all `i ≤ j`, then `S i ≤ S j`. -/
+@[simp]
+def sorted {n : ℕ}  (S : (PureU1 n).charges) : Prop :=
+   ∀ i j (_ : i ≤ j),  S i ≤ S j
+
+/-- Given a charge assignment `S`, the corresponding sorted charge assignment. -/
+@[simp]
+def sort {n : ℕ} (S : (PureU1 n).charges) : (PureU1 n).charges :=
+  ((FamilyPermutations n).rep (Tuple.sort S).symm S)
+
+lemma sort_sorted {n : ℕ} (S : (PureU1 n).charges) :  sorted (sort S) := by
+  simp only [sorted, PureU1_numberCharges, sort, FamilyPermutations, permGroup, permCharges,
+    MonoidHom.coe_mk, OneHom.coe_mk, chargeMap_apply]
+  intro i j hij
+  exact Tuple.monotone_sort S hij
+
+lemma sort_perm {n : ℕ} (S : (PureU1 n).charges) (M :(FamilyPermutations n).group) :
+    sort ((FamilyPermutations n).rep M S) = sort S :=
+  @Tuple.comp_perm_comp_sort_eq_comp_sort n ℚ _ S M⁻¹
+
+lemma sort_apply {n : ℕ} (S : (PureU1 n).charges) (j : Fin n) :
+    sort S j = S ((Tuple.sort S) j) := by
+  rfl
+
+lemma sort_zero {n : ℕ} (S : (PureU1 n).charges)  (hS : sort S = 0) : S = 0 := by
+  funext i
+  have hj : ∀ j, sort S j = 0 := by
+    rw [hS]
+    intro j
+    rfl
+  have hi := hj ((Tuple.sort S).invFun i)
+  rw [sort_apply] at hi
+  simp at hi
+  rw [hi]
+  rfl
+
+lemma sort_projection {n : ℕ} (S : (PureU1 n).charges) : sort (sort S) = sort S :=
+  sort_perm S (Tuple.sort S).symm
+
+/-- The sort function acting on `LinSols`. -/
+def sortAFL  {n : ℕ} (S : (PureU1 n).LinSols) : (PureU1 n).LinSols :=
+  ((FamilyPermutations n).linSolRep (Tuple.sort S.val).symm S)
+
+lemma sortAFL_val {n : ℕ} (S : (PureU1 n).LinSols) :  (sortAFL S).val = sort S.val := by
+  rfl
+
+
+lemma sortAFL_zero {n : ℕ} (S : (PureU1 n).LinSols)  (hS : sortAFL S = 0) : S = 0 := by
+  apply ACCSystemLinear.LinSols.ext
+  have h1 : sort S.val = 0 := by
+    rw [← sortAFL_val]
+    rw [hS]
+    rfl
+  exact sort_zero S.val h1
+
+end PureU1

HepLean/AnomalyCancellation/PureU1/VectorLike.lean

@@ -0,0 +1,44 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.AnomalyCancellation.PureU1.Sort
+import Mathlib.Logic.Equiv.Fin
+/-!
+# Vector like charges
+
+For the `n`-even case we define the property of a charge assignment being vector like.
+
+## TODO
+
+The `n`-odd case.
+
+-/
+universe v u
+
+open Nat
+open  Finset
+open BigOperators
+
+namespace PureU1
+
+variable {n : ℕ}
+
+/--
+  Given a natural number `n`, this lemma proves that `n + n` is equal to `2 * n`.
+-/
+lemma split_equal (n : ℕ) : n + n = 2 * n := (Nat.two_mul n).symm
+
+
+lemma split_odd (n : ℕ) : n + 1 + n = 2 * n + 1 := by omega
+
+/-- A charge configuration for n even is vector like if when sorted the `i`th element
+is equal to the negative of the `n + i`th element.  -/
+@[simp]
+def vectorLikeEven  (S : (PureU1 (2 * n)).charges) : Prop :=
+  ∀ (i : Fin n), (sort S) (Fin.cast (split_equal n)  (Fin.castAdd n i))
+  = - (sort S) (Fin.cast (split_equal n)  (Fin.natAdd n i))
+
+
+end PureU1