diff --git a/HepLean.lean b/HepLean.lean
index 9b65669..5e92471 100644
--- a/HepLean.lean
+++ b/HepLean.lean
@@ -36,11 +36,14 @@ import HepLean.AnomalyCancellation.SMNu.Basic
 import HepLean.AnomalyCancellation.SMNu.FamilyMaps
 import HepLean.AnomalyCancellation.SMNu.NoGrav.Basic
 import HepLean.AnomalyCancellation.SMNu.Ordinary.Basic
+import HepLean.AnomalyCancellation.SMNu.Ordinary.DimSevenPlane
 import HepLean.AnomalyCancellation.SMNu.Ordinary.FamilyMaps
 import HepLean.AnomalyCancellation.SMNu.Permutations
 import HepLean.AnomalyCancellation.SMNu.PlusU1.BMinusL
 import HepLean.AnomalyCancellation.SMNu.PlusU1.Basic
+import HepLean.AnomalyCancellation.SMNu.PlusU1.BoundPlaneDim
 import HepLean.AnomalyCancellation.SMNu.PlusU1.FamilyMaps
 import HepLean.AnomalyCancellation.SMNu.PlusU1.HyperCharge
+import HepLean.AnomalyCancellation.SMNu.PlusU1.PlaneNonSols
 import HepLean.AnomalyCancellation.SMNu.PlusU1.QuadSol
 import HepLean.AnomalyCancellation.SMNu.PlusU1.QuadSolToSol
diff --git a/HepLean/AnomalyCancellation/Basic.lean b/HepLean/AnomalyCancellation/Basic.lean
index 85932c3..382bcb7 100644
--- a/HepLean/AnomalyCancellation/Basic.lean
+++ b/HepLean/AnomalyCancellation/Basic.lean
@@ -4,6 +4,8 @@ Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.AnomalyCancellation.LinearMaps
+import Mathlib.Algebra.Module.Basic
+import Mathlib.LinearAlgebra.FiniteDimensional
 /-!
 # Basic set up for anomaly cancellation conditions
 
@@ -57,6 +59,9 @@ instance chargesModule (χ : ACCSystemCharges) : Module ℚ χ.charges :=
 instance ChargesAddCommGroup (χ : ACCSystemCharges) : AddCommGroup χ.charges :=
   Module.addCommMonoidToAddCommGroup ℚ
 
+instance (χ : ACCSystemCharges) : Module.Finite ℚ χ.charges :=
+  FiniteDimensional.finiteDimensional_pi ℚ
+
 end ACCSystemCharges
 
 /-- The type of charges plus the linear ACCs. -/
@@ -230,6 +235,10 @@ lemma Sols.ext {χ : ACCSystem} {S T : χ.Sols} (h : S.val = T.val) :
   cases' S
   simp_all only
 
+/-- We say a charge S is a solution if it extends to a solution. -/
+def isSolution (χ : ACCSystem) (S : χ.charges) : Prop :=
+ ∃ (sol : χ.Sols), sol.val = S
+
 /-- An instance giving the properties and structures to define an action of `ℚ` on `Sols`. -/
 instance solsMulAction (χ : ACCSystem) : MulAction ℚ χ.Sols where
   smul a S :=  ⟨a • S.toQuadSols , by
diff --git a/HepLean/AnomalyCancellation/LinearMaps.lean b/HepLean/AnomalyCancellation/LinearMaps.lean
index b080d60..2147ac2 100644
--- a/HepLean/AnomalyCancellation/LinearMaps.lean
+++ b/HepLean/AnomalyCancellation/LinearMaps.lean
@@ -5,6 +5,7 @@ Authors: Joseph Tooby-Smith
 -/
 import Mathlib.Tactic.Polyrith
 import Mathlib.Algebra.Module.LinearMap.Basic
+import Mathlib.Algebra.BigOperators.Fin
 /-!
 # Linear maps
 
@@ -107,6 +108,7 @@ class IsSymmetric {V : Type} [AddCommMonoid V] [Module ℚ V] (f : V →ₗ[ℚ]
   swap : ∀ S T, f S T = f T S
 
 namespace BiLinearSymm
+open BigOperators
 
 variable {V : Type} [AddCommMonoid V] [Module ℚ V]
 
@@ -147,6 +149,30 @@ lemma map_add₂ (f : BiLinearSymm V) (S : V) (T1 T2 : V) :
     f (S, T1 + T2) = f (S, T1) + f (S, T2) := by
   rw [f.swap, f.map_add₁, f.swap T1 S, f.swap T2 S]
 
+/-- Fixing the second input vectors, the resulting linear map. -/
+def toLinear₁  (f : BiLinearSymm V) (T : V) : V →ₗ[ℚ] ℚ where
+  toFun S := f (S, T)
+  map_add' S1 S2 := by
+    simp only [f.map_add₁]
+  map_smul' a S := by
+    simp only [f.map_smul₁]
+    rfl
+
+lemma toLinear₁_apply (f : BiLinearSymm V) (S T : V) : f (S, T) = f.toLinear₁ T S := rfl
+
+lemma map_sum₁ {n : ℕ} (f : BiLinearSymm V) (S : Fin n → V) (T : V)  :
+    f (∑ i, S i, T) = ∑ i, f (S i, T) := by
+  rw [f.toLinear₁_apply]
+  rw [map_sum]
+  rfl
+
+lemma map_sum₂ {n : ℕ} (f : BiLinearSymm V) (S : Fin n → V) (T : V) :
+    f ( T, ∑ i, S i) = ∑ i, f (T, S i) := by
+  rw [swap, map_sum₁]
+  apply Fintype.sum_congr
+  intro i
+  rw [swap]
+
 
 /-- The homogenous quadratic equation obtainable from a bilinear function. -/
 @[simps!]
@@ -214,6 +240,11 @@ instance instFun : FunLike (TriLinear V) (V × V × V) ℚ where
     simp_all
 
 end TriLinear
+/-- The structure of a symmetric trilinear function. -/
+structure TriLinearSymm' (V : Type) [AddCommMonoid V] [Module ℚ V] extends
+    V →ₗ[ℚ] V →ₗ[ℚ] V →ₗ[ℚ] ℚ where
+  swap₁' : ∀ S T L, toFun S T L = toFun T S L
+  swap₂' : ∀ S T L, toFun S T L = toFun S L T
 
 /-- The structure of a symmetric trilinear function. -/
 structure TriLinearSymm (V : Type) [AddCommMonoid V] [Module ℚ V] where
@@ -225,7 +256,7 @@ structure TriLinearSymm (V : Type) [AddCommMonoid V] [Module ℚ V] where
   swap₂' : ∀ S T L, toFun (S, T, L) = toFun (S, L, T)
 
 namespace TriLinearSymm
-
+open BigOperators
 variable {V : Type} [AddCommMonoid V] [Module ℚ V]
 
 instance instFun : FunLike (TriLinearSymm V) (V × V × V) ℚ where
@@ -235,7 +266,6 @@ instance instFun : FunLike (TriLinearSymm V) (V × V × V) ℚ where
     cases g
     simp_all
 
-
 lemma toFun_eq_coe (f : TriLinearSymm V) : f.toFun = f := rfl
 
 lemma swap₁ (f : TriLinearSymm V) (S T L : V) : f (S, T, L) = f (T, S, L) :=
@@ -271,6 +301,49 @@ lemma map_add₃ (f : TriLinearSymm V) (S T L1 L2 : V) :
     f (S, T, L1 + L2) = f (S, T, L1) + f (S, T, L2) := by
   rw [f.swap₃, f.map_add₁, f.swap₃, f.swap₃ L2 T S]
 
+/-- Fixing the second and third input vectors, the resulting linear map. -/
+def toLinear₁  (f : TriLinearSymm V) (T L : V) : V →ₗ[ℚ] ℚ where
+  toFun S := f (S, T, L)
+  map_add' S1 S2 := by
+    simp only [f.map_add₁]
+  map_smul' a S := by
+    simp only [f.map_smul₁]
+    rfl
+
+lemma toLinear₁_apply (f : TriLinearSymm V) (S T L : V) : f (S, T, L) = f.toLinear₁ T L S := rfl
+
+lemma map_sum₁ {n : ℕ} (f : TriLinearSymm V) (S : Fin n → V) (T : V) (L : V) :
+    f (∑ i, S i, T, L) = ∑ i, f (S i, T, L) := by
+  rw [f.toLinear₁_apply]
+  rw [map_sum]
+  rfl
+
+lemma map_sum₂ {n : ℕ} (f : TriLinearSymm V) (S : Fin n → V) (T : V) (L : V) :
+    f ( T, ∑ i, S i, L) = ∑ i, f (T, S i, L) := by
+  rw [swap₁, map_sum₁]
+  apply Fintype.sum_congr
+  intro i
+  rw [swap₁]
+
+lemma map_sum₃ {n : ℕ} (f : TriLinearSymm V) (S : Fin n → V) (T : V) (L : V) :
+    f ( T, L, ∑ i, S i) = ∑ i, f (T, L, S i) := by
+  rw [swap₃, map_sum₁]
+  apply Fintype.sum_congr
+  intro i
+  rw [swap₃]
+
+lemma map_sum₁₂₃ {n1 n2 n3 : ℕ} (f : TriLinearSymm V) (S : Fin n1 → V)
+    (T : Fin n2 → V) (L : Fin n3 → V) :
+    f (∑ i, S i, ∑ i, T i, ∑ i, L i) = ∑ i, ∑ k, ∑ l, f (S i,  T k,  L l) := by
+  rw [map_sum₁]
+  apply Fintype.sum_congr
+  intro i
+  rw [map_sum₂]
+  apply Fintype.sum_congr
+  intro i
+  rw [map_sum₃]
+
+
 /-- The homogenous cubic equation obtainable from a symmetric trilinear function. -/
 @[simps!]
 def toCubic {charges : Type} [AddCommMonoid charges] [Module ℚ charges]
diff --git a/HepLean/AnomalyCancellation/SMNu/Ordinary/DimSevenPlane.lean b/HepLean/AnomalyCancellation/SMNu/Ordinary/DimSevenPlane.lean
new file mode 100644
index 0000000..d2806a7
--- /dev/null
+++ b/HepLean/AnomalyCancellation/SMNu/Ordinary/DimSevenPlane.lean
@@ -0,0 +1,349 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.AnomalyCancellation.SMNu.Ordinary.Basic
+/-!
+# Dimension 7 plane
+
+We work here in the three family case.
+We give an example of a 7 dimensional plane on which every point satisfies the ACCs.
+
+The main result of this file is `seven_dim_plane_exists` which states that there exists a
+7 dimensional plane of charges on which every point satisfies the ACCs.
+
+-/
+
+namespace SMRHN
+namespace SM
+open SMνCharges
+open SMνACCs
+open BigOperators
+
+namespace PlaneSeven
+
+/-- A charge assignment forming one of the basis elements of the plane. -/
+def B₀ : (SM 3).charges := toSpeciesEquiv.invFun ( fun s => fun i =>
+  match s, i with
+  | 0, 0 => 1
+  | 0, 1 => - 1
+  | _, _ => 0
+  )
+
+lemma B₀_cubic (S T : (SM 3).charges) : cubeTriLin (B₀, S, T) =
+    6 * (S (0 : Fin 18) * T  (0 : Fin 18) - S  (1 : Fin 18) * T  (1 : Fin 18)) := by
+  simp [Fin.sum_univ_three, B₀, Fin.divNat, Fin.modNat, finProdFinEquiv]
+  ring
+
+/-- A charge assignment forming one of the basis elements of the plane. -/
+def B₁ : (SM 3).charges := toSpeciesEquiv.invFun ( fun s => fun i =>
+  match s, i with
+  | 1, 0 => 1
+  | 1, 1 => - 1
+  | _, _ => 0
+  )
+
+lemma B₁_cubic (S T : (SM 3).charges) : cubeTriLin (B₁, S, T) =
+    3 * (S (3 : Fin 18) * T  (3 : Fin 18) - S  (4 : Fin 18) * T  (4 : Fin 18)) := by
+  simp [Fin.sum_univ_three, B₁, Fin.divNat, Fin.modNat, finProdFinEquiv]
+  ring
+
+/-- A charge assignment forming one of the basis elements of the plane. -/
+def B₂ : (SM 3).charges := toSpeciesEquiv.invFun ( fun s => fun i =>
+  match s, i with
+  | 2, 0 => 1
+  | 2, 1 => - 1
+  | _, _ => 0
+  )
+
+lemma B₂_cubic (S T : (SM 3).charges) : cubeTriLin (B₂, S, T) =
+    3 * (S (6 : Fin 18) * T  (6 : Fin 18) - S  (7 : Fin 18) * T  (7 : Fin 18)) := by
+  simp [Fin.sum_univ_three, B₂, Fin.divNat, Fin.modNat, finProdFinEquiv]
+  ring
+
+/-- A charge assignment forming one of the basis elements of the plane. -/
+def B₃ : (SM 3).charges := toSpeciesEquiv.invFun ( fun s => fun i =>
+  match s, i with
+  | 3, 0 => 1
+  | 3, 1 => - 1
+  | _, _ => 0
+  )
+
+lemma B₃_cubic (S T : (SM 3).charges) : cubeTriLin (B₃, S, T) =
+    2 * (S (9 : Fin 18) * T  (9 : Fin 18) - S  (10 : Fin 18) * T  (10 : Fin 18)) := by
+  simp [Fin.sum_univ_three, B₃, Fin.divNat, Fin.modNat, finProdFinEquiv]
+  ring_nf
+  rfl
+
+/-- A charge assignment forming one of the basis elements of the plane. -/
+def B₄ : (SM 3).charges := toSpeciesEquiv.invFun ( fun s => fun i =>
+  match s, i with
+  | 4, 0 => 1
+  | 4, 1 => - 1
+  | _, _ => 0
+  )
+
+lemma B₄_cubic (S T : (SM 3).charges) : cubeTriLin (B₄, S, T) =
+    (S (12 : Fin 18) * T  (12 : Fin 18) - S  (13 : Fin 18) * T  (13 : Fin 18)) := by
+  simp [Fin.sum_univ_three, B₄, Fin.divNat, Fin.modNat, finProdFinEquiv]
+  ring_nf
+  rfl
+
+/-- A charge assignment forming one of the basis elements of the plane. -/
+def B₅ : (SM 3).charges := toSpeciesEquiv.invFun ( fun s => fun i =>
+  match s, i with
+  | 5, 0 => 1
+  | 5, 1 => - 1
+  | _, _ => 0
+  )
+
+lemma B₅_cubic (S T : (SM 3).charges) : cubeTriLin (B₅, S, T) =
+    (S (15 : Fin 18) * T  (15 : Fin 18) - S  (16 : Fin 18) * T  (16 : Fin 18)) := by
+  simp [Fin.sum_univ_three, B₅, Fin.divNat, Fin.modNat, finProdFinEquiv]
+  ring_nf
+  rfl
+
+/-- A charge assignment forming one of the basis elements of the plane. -/
+def B₆ : (SM 3).charges := toSpeciesEquiv.invFun ( fun s => fun i =>
+  match s, i with
+  | 1, 2 => 1
+  | 2, 2 => -1
+  | _, _ => 0
+  )
+
+lemma B₆_cubic (S T : (SM 3).charges) : cubeTriLin (B₆, S, T) =
+    3* (S (5 : Fin 18) * T  (5 : Fin 18) - S  (8 : Fin 18) * T  (8 : Fin 18)) := by
+  simp [Fin.sum_univ_three, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
+  ring_nf
+
+/-- The charge assignments forming a basis of the plane. -/
+@[simp]
+def B : Fin 7 → (SM 3).charges := fun i =>
+  match i with
+  | 0 => B₀
+  | 1 => B₁
+  | 2 => B₂
+  | 3 => B₃
+  | 4 => B₄
+  | 5 => B₅
+  | 6 => B₆
+
+lemma B₀_Bi_cubic {i : Fin 7} (hi : 0 ≠ i) (S : (SM 3).charges) :
+    cubeTriLin (B 0, B i, S) = 0 := by
+  change cubeTriLin (B₀, B i, S) = 0
+  rw [B₀_cubic]
+  fin_cases i <;>
+    simp at hi <;>
+    simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
+
+
+lemma B₁_Bi_cubic {i : Fin 7} (hi : 1 ≠ i) (S : (SM 3).charges) :
+    cubeTriLin (B 1, B i, S) = 0 := by
+  change cubeTriLin (B₁, B i, S) = 0
+  rw [B₁_cubic]
+  fin_cases i <;>
+    simp at hi <;>
+    simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
+
+lemma B₂_Bi_cubic {i : Fin 7} (hi : 2 ≠ i) (S : (SM 3).charges) :
+    cubeTriLin (B 2, B i, S) = 0 := by
+  change cubeTriLin (B₂, B i, S) = 0
+  rw [B₂_cubic]
+  fin_cases i <;>
+    simp at hi <;>
+    simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
+
+lemma B₃_Bi_cubic {i : Fin 7} (hi : 3 ≠ i) (S : (SM 3).charges) :
+    cubeTriLin (B 3, B i, S) = 0 := by
+  change cubeTriLin (B₃, B i, S) = 0
+  rw [B₃_cubic]
+  fin_cases i <;>
+    simp at hi <;>
+    simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
+
+lemma B₄_Bi_cubic {i : Fin 7} (hi : 4 ≠ i) (S : (SM 3).charges) :
+    cubeTriLin (B 4, B i, S) = 0 := by
+  change cubeTriLin (B₄, B i, S) = 0
+  rw [B₄_cubic]
+  fin_cases i <;>
+    simp at hi <;>
+    simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
+
+lemma B₅_Bi_cubic {i : Fin 7} (hi : 5 ≠ i) (S : (SM 3).charges) :
+    cubeTriLin (B 5, B i, S) = 0 := by
+  change cubeTriLin (B₅, B i, S) = 0
+  rw [B₅_cubic]
+  fin_cases i <;>
+    simp at hi <;>
+    simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
+
+lemma B₆_Bi_cubic {i : Fin 7} (hi : 6 ≠ i) (S : (SM 3).charges) :
+    cubeTriLin (B 6, B i, S) = 0 := by
+  change cubeTriLin (B₆, B i, S) = 0
+  rw [B₆_cubic]
+  fin_cases i <;>
+    simp at hi <;>
+    simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
+
+lemma Bi_Bj_ne_cubic {i j : Fin 7} (h : i ≠ j) (S : (SM 3).charges) :
+    cubeTriLin (B i, B j, S) = 0 := by
+  fin_cases i
+  exact B₀_Bi_cubic h S
+  exact B₁_Bi_cubic h S
+  exact B₂_Bi_cubic h S
+  exact B₃_Bi_cubic h S
+  exact B₄_Bi_cubic h S
+  exact B₅_Bi_cubic h S
+  exact B₆_Bi_cubic h S
+
+lemma B₀_B₀_Bi_cubic {i : Fin 7} :
+    cubeTriLin (B 0, B 0, B i) = 0 := by
+  change cubeTriLin (B₀, B₀, B i) = 0
+  rw [B₀_cubic]
+  fin_cases i <;>
+  simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
+
+lemma B₁_B₁_Bi_cubic {i : Fin 7} :
+    cubeTriLin (B 1, B 1, B i) = 0 := by
+  change cubeTriLin (B₁, B₁, B i) = 0
+  rw [B₁_cubic]
+  fin_cases i <;>
+  simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
+
+lemma B₂_B₂_Bi_cubic {i : Fin 7} :
+    cubeTriLin (B 2, B 2, B i) = 0 := by
+  change cubeTriLin (B₂, B₂, B i) = 0
+  rw [B₂_cubic]
+  fin_cases i <;>
+  simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
+
+lemma B₃_B₃_Bi_cubic {i : Fin 7} :
+    cubeTriLin (B 3, B 3, B i) = 0 := by
+  change cubeTriLin (B₃, B₃, B i) = 0
+  rw [B₃_cubic]
+  fin_cases i <;>
+  simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
+
+lemma B₄_B₄_Bi_cubic {i : Fin 7} :
+    cubeTriLin (B 4, B 4, B i) = 0 := by
+  change cubeTriLin (B₄, B₄, B i) = 0
+  rw [B₄_cubic]
+  fin_cases i <;>
+  simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
+
+lemma B₅_B₅_Bi_cubic {i : Fin 7} :
+    cubeTriLin (B 5, B 5, B i) = 0 := by
+  change cubeTriLin (B₅, B₅, B i) = 0
+  rw [B₅_cubic]
+  fin_cases i <;>
+  simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
+
+lemma B₆_B₆_Bi_cubic {i : Fin 7} :
+    cubeTriLin (B 6, B 6, B i) = 0 := by
+  change cubeTriLin (B₆, B₆, B i) = 0
+  rw [B₆_cubic]
+  fin_cases i <;>
+  simp [B₀, B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat, finProdFinEquiv]
+
+
+lemma Bi_Bi_Bj_cubic (i j : Fin 7) :
+    cubeTriLin (B i, B i, B j) = 0 := by
+  fin_cases i
+  exact B₀_B₀_Bi_cubic
+  exact B₁_B₁_Bi_cubic
+  exact B₂_B₂_Bi_cubic
+  exact B₃_B₃_Bi_cubic
+  exact B₄_B₄_Bi_cubic
+  exact B₅_B₅_Bi_cubic
+  exact B₆_B₆_Bi_cubic
+
+lemma Bi_Bj_Bk_cubic (i j k : Fin 7) :
+    cubeTriLin (B i, B j, B k) = 0 := by
+  by_cases hij : i ≠ j
+  exact Bi_Bj_ne_cubic hij (B k)
+  simp at hij
+  rw [hij]
+  exact Bi_Bi_Bj_cubic j k
+
+theorem B_in_accCube (f : Fin 7 → ℚ) : accCube (∑ i, f i • B i) = 0 := by
+  change cubeTriLin _ = 0
+  rw [cubeTriLin.map_sum₁₂₃]
+  apply Fintype.sum_eq_zero
+  intro i
+  apply Fintype.sum_eq_zero
+  intro k
+  apply Fintype.sum_eq_zero
+  intro l
+  rw [cubeTriLin.map_smul₁, cubeTriLin.map_smul₂, cubeTriLin.map_smul₃]
+  rw [Bi_Bj_Bk_cubic]
+  simp
+
+lemma B_sum_is_sol (f : Fin 7 → ℚ) : (SM 3).isSolution (∑ i, f i • B i) := by
+  let X := chargeToAF (∑ i, f i • B i) (by
+    rw [map_sum]
+    apply Fintype.sum_eq_zero
+    intro i
+    rw [map_smul]
+    have h : accGrav (B i) = 0 := by
+      fin_cases i <;> rfl
+    rw [h]
+    simp)
+    (by
+      rw [map_sum]
+      apply Fintype.sum_eq_zero
+      intro i
+      rw [map_smul]
+      have h : accSU2 (B i) = 0 := by
+        fin_cases i <;> rfl
+      rw [h]
+      simp)
+    (by
+      rw [map_sum]
+      apply Fintype.sum_eq_zero
+      intro i
+      rw [map_smul]
+      have h : accSU3 (B i) = 0 := by
+        fin_cases i <;> rfl
+      rw [h]
+      simp)
+    (B_in_accCube f)
+  use X
+  rfl
+
+theorem basis_linear_independent : LinearIndependent ℚ B := by
+  apply Fintype.linearIndependent_iff.mpr
+  intro f h
+  have h0 := congrFun h (0 : Fin 18)
+  have h1 := congrFun h (3 : Fin 18)
+  have h2 := congrFun h (6 : Fin 18)
+  have h3 := congrFun h (9 : Fin 18)
+  have h4 := congrFun h (12 : Fin 18)
+  have h5 := congrFun h (15 : Fin 18)
+  have h6 := congrFun h (5 : Fin 18)
+  rw [@Fin.sum_univ_seven] at h0 h1 h2 h3 h4 h5 h6
+  simp [HSMul.hSMul] at h0 h1 h2 h3 h4 h5 h6
+  rw [B₀, B₁, B₂, B₃, B₄, B₅, B₆] at h0 h1 h2 h3 h4 h5 h6
+  simp [Fin.divNat, Fin.modNat] at h0 h1 h2 h3 h4 h5 h6
+  intro i
+  match i with
+  | 0 => exact h0
+  | 1 => exact h1
+  | 2 => exact h2
+  | 3 => exact h3
+  | 4 => exact h4
+  | 5 => exact h5
+  | 6 => exact h6
+
+end PlaneSeven
+
+theorem seven_dim_plane_exists : ∃ (B : Fin 7 → (SM 3).charges),
+    LinearIndependent ℚ B ∧ ∀ (f : Fin 7 → ℚ), (SM 3).isSolution (∑ i, f i • B i)  := by
+  use PlaneSeven.B
+  apply And.intro
+  exact PlaneSeven.basis_linear_independent
+  exact PlaneSeven.B_sum_is_sol
+
+
+end SM
+end SMRHN
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean
new file mode 100644
index 0000000..a116fa5
--- /dev/null
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/BoundPlaneDim.lean
@@ -0,0 +1,73 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.AnomalyCancellation.SMNu.PlusU1.Basic
+import HepLean.AnomalyCancellation.SMNu.PlusU1.FamilyMaps
+import HepLean.AnomalyCancellation.SMNu.PlusU1.PlaneNonSols
+/-!
+# Bound on plane dimension
+
+We place an upper bound on the dimension of a plane of charges on which every point is a solution.
+The upper bound is 7, proven in the theorem `plane_exists_dim_le_7`.
+
+-/
+universe v u
+
+namespace SMRHN
+namespace PlusU1
+
+open SMνCharges
+open SMνACCs
+open BigOperators
+
+/-- A proposition which is true if for a given `n` a plane of charges of dimension `n` exists
+in which each point is a solution. -/
+def existsPlane (n : ℕ) : Prop := ∃ (B : Fin n → (PlusU1 3).charges),
+   LinearIndependent ℚ B ∧ ∀ (f : Fin n → ℚ), (PlusU1 3).isSolution (∑ i, f i • B i)
+
+lemma exists_plane_exists_basis {n : ℕ} (hE : existsPlane n) :
+    ∃ (B : Fin 11 ⊕ Fin n → (PlusU1 3).charges), LinearIndependent ℚ B := by
+  obtain ⟨E, hE1, hE2⟩ := hE
+  obtain ⟨B, hB1, hB2⟩ := eleven_dim_plane_of_no_sols_exists
+  let Y := Sum.elim B E
+  use Y
+  apply Fintype.linearIndependent_iff.mpr
+  intro g hg
+  rw [@Fintype.sum_sum_type] at hg
+  rw [@add_eq_zero_iff_eq_neg] at hg
+  rw [← @Finset.sum_neg_distrib] at hg
+  have h1 : ∑ x : Fin n, -(g (Sum.inr x) • Y (Sum.inr x)) =
+      ∑ x : Fin n, (-g (Sum.inr x)) • Y (Sum.inr x):= by
+    apply Finset.sum_congr
+    simp only
+    intro i _
+    simp
+  rw [h1] at hg
+  have h2 : ∑ a₁ : Fin 11, g (Sum.inl a₁) • Y (Sum.inl a₁) = 0 := by
+    apply hB2
+    erw [hg]
+    exact hE2 fun i => -g (Sum.inr i)
+  rw [Fintype.linearIndependent_iff] at hB1 hE1
+  have h3 : ∀ i, g (Sum.inl i) = 0 := hB1 (fun i => (g (Sum.inl i))) h2
+  rw [h2] at hg
+  have h4 : ∀ i, - g (Sum.inr i) = 0 := hE1 (fun i => (- g (Sum.inr i))) hg.symm
+  simp at h4
+  intro i
+  match i with
+  | Sum.inl i => exact h3 i
+  | Sum.inr i => exact h4 i
+
+
+theorem plane_exists_dim_le_7 {n : ℕ} (hn : existsPlane n) : n ≤ 7 := by
+  obtain ⟨B, hB⟩ := exists_plane_exists_basis hn
+  have h1 := LinearIndependent.fintype_card_le_finrank hB
+  simp at h1
+  rw [show FiniteDimensional.finrank ℚ (PlusU1 3).charges = 18 from
+    FiniteDimensional.finrank_fin_fun ℚ] at h1
+  exact Nat.le_of_add_le_add_left h1
+
+
+end PlusU1
+end SMRHN
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean
new file mode 100644
index 0000000..98e74a0
--- /dev/null
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/PlaneNonSols.lean
@@ -0,0 +1,265 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.AnomalyCancellation.SMNu.PlusU1.Basic
+import HepLean.AnomalyCancellation.SMNu.PlusU1.FamilyMaps
+/-!
+# Plane of non-solutions
+
+Working in the three family case, we show that there exists an eleven dimensional plane in the
+vector space of charges on which there are no solutions.
+
+The main result of this file is `eleven_dim_plane_of_no_sols_exists`, which states that
+an 11 dimensional plane of charges exists on which there are no solutions except the origin.
+-/
+
+universe v u
+
+namespace SMRHN
+namespace PlusU1
+
+open SMνCharges
+open SMνACCs
+open BigOperators
+
+namespace ElevenPlane
+
+/-- A charge assignment forming one of the basis elements of the plane. -/
+def B₀ : (PlusU1 3).charges := ![1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
+
+/-- A charge assignment forming one of the basis elements of the plane. -/
+def B₁ : (PlusU1 3).charges := ![0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
+
+/-- A charge assignment forming one of the basis elements of the plane. -/
+def B₂ : (PlusU1 3).charges := ![0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
+
+/-- A charge assignment forming one of the basis elements of the plane. -/
+def B₃ : (PlusU1 3).charges := ![0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
+
+/-- A charge assignment forming one of the basis elements of the plane. -/
+def B₄ : (PlusU1 3).charges := ![0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
+
+/-- A charge assignment forming one of the basis elements of the plane. -/
+def B₅ : (PlusU1 3).charges := ![0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0]
+
+/-- A charge assignment forming one of the basis elements of the plane. -/
+def B₆ : (PlusU1 3).charges := ![0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0]
+
+/-- A charge assignment forming one of the basis elements of the plane. -/
+def B₇ : (PlusU1 3).charges := ![0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0]
+
+/-- A charge assignment forming one of the basis elements of the plane. -/
+def B₈  : (PlusU1 3).charges := ![0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0]
+
+/-- A charge assignment forming one of the basis elements of the plane. -/
+def B₉ : (PlusU1 3).charges := ![0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 2, 0]
+
+/-- A charge assignment forming one of the basis elements of the plane. -/
+def B₁₀ : (PlusU1 3).charges := ![0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1]
+
+/-- The charge assignment forming a basis of the plane. -/
+def B : Fin 11 → (PlusU1 3).charges := fun i =>
+  match i with
+  | 0 => B₀
+  | 1 => B₁
+  | 2 => B₂
+  | 3 => B₃
+  | 4 => B₄
+  | 5 => B₅
+  | 6 => B₆
+  | 7 => B₇
+  | 8 => B₈
+  | 9 => B₉
+  | 10 => B₁₀
+
+lemma Bi_Bj_quad {i j : Fin 11} (hi : i ≠ j) : quadBiLin (B i, B j) = 0 := by
+  fin_cases i <;> fin_cases j
+  any_goals rfl
+  all_goals simp at hi
+
+lemma Bi_sum_quad (i : Fin 11) (f : Fin 11 → ℚ) :
+    quadBiLin (B i, ∑ k, f k • B k) = f i * quadBiLin (B i, B i)  := by
+  rw [quadBiLin.map_sum₂]
+  rw [Fintype.sum_eq_single i]
+  rw [quadBiLin.map_smul₂]
+  intro k hij
+  rw [quadBiLin.map_smul₂, Bi_Bj_quad hij.symm]
+  simp
+
+/-- The coefficents of the quadratic equation in our basis. -/
+@[simp]
+def quadCoeff : Fin 11 → ℚ := ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0]
+
+lemma quadCoeff_eq_bilinear (i : Fin 11) : quadCoeff i = quadBiLin (B i, B i) := by
+  fin_cases i
+  all_goals rfl
+
+lemma on_accQuad (f : Fin 11 → ℚ) :
+    accQuad (∑ i, f i • B i) = ∑ i, quadCoeff i * (f i)^2  := by
+  change quadBiLin _ = _
+  rw [quadBiLin.map_sum₁]
+  apply Fintype.sum_congr
+  intro i
+  rw [quadBiLin.map_smul₁, Bi_sum_quad, quadCoeff_eq_bilinear]
+  ring
+
+
+lemma isSolution_quadCoeff_f_sq_zero (f : Fin 11 → ℚ) (hS : (PlusU1 3).isSolution (∑ i, f i • B i))
+    (k : Fin 11)  : quadCoeff k * (f k)^2 = 0 := by
+  obtain ⟨S, hS⟩ := hS
+  have hQ := quadSol S.1
+  rw [hS, on_accQuad] at hQ
+  rw [Fintype.sum_eq_zero_iff_of_nonneg] at hQ
+  exact congrFun hQ k
+  intro i
+  simp only [Pi.zero_apply, quadCoeff]
+  rw [mul_nonneg_iff]
+  apply Or.inl
+  apply And.intro
+  fin_cases i <;> rfl
+  exact sq_nonneg (f i)
+
+lemma isSolution_f0 (f : Fin 11 → ℚ) (hS : (PlusU1 3).isSolution (∑ i, f i • B i)) : f 0 = 0 := by
+  simpa using (isSolution_quadCoeff_f_sq_zero f hS 0)
+
+lemma isSolution_f1 (f : Fin 11 → ℚ) (hS : (PlusU1 3).isSolution (∑ i, f i • B i)) : f 1 = 0 := by
+  simpa using (isSolution_quadCoeff_f_sq_zero f hS 1)
+
+lemma isSolution_f2 (f : Fin 11 → ℚ) (hS : (PlusU1 3).isSolution (∑ i, f i • B i)) : f 2 = 0 := by
+  simpa using (isSolution_quadCoeff_f_sq_zero f hS 2)
+
+lemma isSolution_f3 (f : Fin 11 → ℚ) (hS : (PlusU1 3).isSolution (∑ i, f i • B i)) : f 3 = 0 := by
+  simpa using (isSolution_quadCoeff_f_sq_zero f hS 3)
+
+lemma isSolution_f4 (f : Fin 11 → ℚ) (hS : (PlusU1 3).isSolution (∑ i, f i • B i)) : f 4 = 0 := by
+  simpa using (isSolution_quadCoeff_f_sq_zero f hS 4)
+
+lemma isSolution_f5 (f : Fin 11 → ℚ) (hS : (PlusU1 3).isSolution (∑ i, f i • B i)) : f 5 = 0 := by
+  have h := isSolution_quadCoeff_f_sq_zero f hS 5
+  rw [mul_eq_zero] at h
+  change 1 = 0 ∨ _ = _ at h
+  simpa using h
+
+lemma isSolution_f6 (f : Fin 11 → ℚ) (hS : (PlusU1 3).isSolution (∑ i, f i • B i)) : f 6 = 0 := by
+  have h := isSolution_quadCoeff_f_sq_zero f hS 6
+  rw [mul_eq_zero] at h
+  change 1 = 0 ∨ _ = _ at h
+  simpa using h
+
+lemma isSolution_f7 (f : Fin 11 → ℚ) (hS : (PlusU1 3).isSolution (∑ i, f i • B i)) : f 7 = 0 := by
+  have h := isSolution_quadCoeff_f_sq_zero f hS 7
+  rw [mul_eq_zero] at h
+  change 1 = 0 ∨ _ = _ at h
+  simpa using h
+
+lemma isSolution_f8 (f : Fin 11 → ℚ) (hS : (PlusU1 3).isSolution (∑ i, f i • B i)) : f 8 = 0 := by
+  have h := isSolution_quadCoeff_f_sq_zero f hS 8
+  rw [mul_eq_zero] at h
+  change 1 = 0 ∨ _ = _ at h
+  simpa using h
+
+lemma isSolution_sum_part (f : Fin 11 → ℚ) (hS : (PlusU1 3).isSolution (∑ i, f i • B i)) :
+    ∑ i, f i • B i = f 9 • B₉ + f 10 • B₁₀ := by
+  rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc, Fin.sum_univ_castSucc, Fin.sum_univ_eight]
+  change f 0 • B 0 + f 1 • B 1 + f 2 • B 2 + f 3 • B 3 + f 4 • B 4 + f 5 • B 5 + f 6 • B 6 +
+  f 7 • B 7 + f 8 • B 8 + f 9 • B 9 + f 10 • B 10 = f 9 • B₉ + f 10 • B₁₀
+  rw [isSolution_f0 f hS, isSolution_f1 f hS, isSolution_f2 f hS, isSolution_f3 f hS,
+    isSolution_f4 f hS, isSolution_f5 f hS,
+    isSolution_f6 f hS, isSolution_f7 f hS, isSolution_f8 f hS]
+  simp
+  rfl
+
+lemma isSolution_grav  (f : Fin 11 → ℚ) (hS : (PlusU1 3).isSolution (∑ i, f i • B i)) :
+    f 10 = - 3 * f 9 := by
+  have hx := isSolution_sum_part f hS
+  obtain ⟨S, hS'⟩ := hS
+  have hg := gravSol S.toLinSols
+  rw [hS'] at hg
+  rw [hx] at hg
+  rw [accGrav.map_add, accGrav.map_smul, accGrav.map_smul] at hg
+  rw [show accGrav B₉ = 3 by rfl] at hg
+  rw [show accGrav B₁₀ = 1 by rfl] at hg
+  simp at hg
+  linear_combination hg
+
+lemma isSolution_sum_part' (f : Fin 11 → ℚ) (hS : (PlusU1 3).isSolution (∑ i, f i • B i)) :
+    ∑ i, f i • B i = f 9 • B₉ + (- 3 * f 9) • B₁₀ := by
+  rw [isSolution_sum_part f hS]
+  rw [isSolution_grav f hS]
+
+lemma isSolution_f9 (f : Fin 11 → ℚ) (hS : (PlusU1 3).isSolution (∑ i, f i • B i)) :
+    f 9 = 0 := by
+  have hx := isSolution_sum_part' f hS
+  obtain ⟨S, hS'⟩ := hS
+  have hc := cubeSol S
+  rw [hS'] at hc
+  rw [hx] at hc
+  change cubeTriLin.toCubic _ = _ at hc
+  rw [cubeTriLin.toCubic_add] at hc
+  erw [accCube.map_smul] at hc
+  erw [accCube.map_smul (- 3 * f 9) B₁₀] at hc
+  rw [cubeTriLin.map_smul₁, cubeTriLin.map_smul₁, cubeTriLin.map_smul₂, cubeTriLin.map_smul₂,
+    cubeTriLin.map_smul₃, cubeTriLin.map_smul₃] at hc
+  rw [show accCube B₉ = 9 by rfl] at hc
+  rw [show accCube B₁₀ = 1 by rfl] at hc
+  rw [show cubeTriLin (B₉, B₉, B₁₀) = 0 by rfl] at hc
+  rw [show cubeTriLin (B₁₀, B₁₀, B₉) = 0 by rfl] at hc
+  simp at hc
+  have h1 : f 9 ^ 3 * 9 + (-(3 * f 9)) ^ 3 = - 18 * f 9 ^ 3 := by
+    ring
+  rw [h1] at hc
+  simpa using hc
+
+lemma isSolution_f10 (f : Fin 11 → ℚ) (hS : (PlusU1 3).isSolution (∑ i, f i • B i)) :
+    f 10 = 0 := by
+  rw [isSolution_grav f hS, isSolution_f9 f hS]
+  simp
+
+lemma isSolution_f_zero (f : Fin 11 → ℚ) (hS : (PlusU1 3).isSolution (∑ i, f i • B i))
+    (k : Fin 11) : f k = 0 := by
+  fin_cases k
+  exact isSolution_f0 f hS
+  exact isSolution_f1 f hS
+  exact isSolution_f2 f hS
+  exact isSolution_f3 f hS
+  exact isSolution_f4 f hS
+  exact isSolution_f5 f hS
+  exact isSolution_f6 f hS
+  exact isSolution_f7 f hS
+  exact isSolution_f8 f hS
+  exact isSolution_f9 f hS
+  exact isSolution_f10 f hS
+
+
+lemma isSolution_only_if_zero (f : Fin 11 → ℚ) (hS : (PlusU1 3).isSolution (∑ i, f i • B i)) :
+    ∑ i, f i • B i = 0 := by
+  rw [isSolution_sum_part f hS]
+  rw [isSolution_grav f hS]
+  rw [isSolution_f9 f hS]
+  simp
+
+
+theorem basis_linear_independent : LinearIndependent ℚ B := by
+  apply Fintype.linearIndependent_iff.mpr
+  intro f h
+  let X : (PlusU1 3).Sols := chargeToAF 0 (by rfl) (by rfl) (by rfl) (by rfl) (by rfl) (by rfl)
+  have hS : (PlusU1 3).isSolution (∑ i, f i • B i) := by
+    use X
+    rw [h]
+    rfl
+  exact isSolution_f_zero f hS
+
+end ElevenPlane
+
+theorem eleven_dim_plane_of_no_sols_exists : ∃ (B : Fin 11 → (PlusU1 3).charges),
+    LinearIndependent ℚ B ∧
+    ∀ (f : Fin 11 → ℚ), (PlusU1 3).isSolution (∑ i, f i • B i) → ∑ i, f i • B i = 0 := by
+  use ElevenPlane.B
+  apply And.intro
+  exact ElevenPlane.basis_linear_independent
+  exact ElevenPlane.isSolution_only_if_zero
+
+end PlusU1
+end SMRHN