feat: Add results related to MSSM

2024-04-17 16:23:40 -04:00 · 2024-04-17 16:23:40 -04:00 · 01d4c0c81b
commit 01d4c0c81b
parent c13a474330
10 changed files with 1553 additions and 2 deletions
--- a/HepLean/AnomalyCancellation/MSSMNu/B3.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/B3.lean
@ -0,0 +1,79 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.AnomalyCancellation.MSSMNu.Basic
+/-!
+# The definition of the solution B₃ and properties thereof
+
+We define $B_3$ and show that it is a double point of the cubic.
+
+# References
+
+The main reference for the material in this file is:
+
+- https://arxiv.org/pdf/2107.07926.pdf
+
+-/
+
+universe v u
+
+namespace MSSMACC
+open MSSMCharges
+open MSSMACCs
+open BigOperators
+
+/-- $B_3$ is the charge which is $B-L$ in all families, but with the third
+family of the opposite sign. -/
+def B₃AsCharge : MSSMACC.charges := toSpecies.symm
+  ⟨fun s => fun i =>
+    match s, i with
+    | 0, 0 => 1
+    | 0, 1 => 1
+    | 0, 2 => - 1
+    | 1, 0 => - 1
+    | 1, 1 => - 1
+    | 1, 2 =>  1
+    | 2, 0 => - 1
+    | 2, 1 => - 1
+    | 2, 2 =>  1
+    | 3, 0 => - 3
+    | 3, 1 => - 3
+    | 3, 2 => 3
+    | 4, 0 => 3
+    | 4, 1 => 3
+    | 4, 2 => - 3
+    | 5, 0 => 3
+    | 5, 1 => 3
+    | 5, 2 => - 3,
+  fun s =>
+    match s with
+    | 0 => -3
+    | 1 => 3⟩
+
+/-- $B_3$ as a solution. -/
+def B₃ : MSSMACC.Sols :=
+  MSSMACC.AnomalyFreeMk B₃AsCharge (by rfl) (by rfl) (by rfl) (by rfl) (by rfl) (by rfl)
+
+lemma B₃_val : B₃.val = B₃AsCharge := by
+  rfl
+
+lemma doublePoint_B₃_B₃ (R : MSSMACC.LinSols) : cubeTriLin (B₃.val, B₃.val, R.val) = 0 := by
+  rw [← TriLinearSymm.toFun_eq_coe]
+  simp only [cubeTriLin, cubeTriLinToFun, MSSMSpecies_numberCharges]
+  rw [Fin.sum_univ_three]
+  rw [B₃_val]
+  rw [B₃AsCharge]
+  repeat rw [toSMSpecies_toSpecies_inv]
+  rw [Hd_toSpecies_inv, Hu_toSpecies_inv]
+  simp only [mul_one, Fin.isValue, toSMSpecies_apply, one_mul, mul_neg, neg_neg, neg_mul, Hd_apply,
+    Fin.reduceFinMk, Hu_apply]
+  have hLin := R.linearSol
+  simp at hLin
+  have h0 := hLin 0
+  have h2 := hLin 2
+  simp [Fin.sum_univ_three] at h0 h2
+  linear_combination 9 * h0 - 24 * h2
+
+end MSSMACC
--- a/HepLean/AnomalyCancellation/MSSMNu/Basic.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/Basic.lean
@ -27,7 +27,7 @@ open BigOperators
@[simps!]
 def MSSMCharges : ACCSystemCharges := ACCSystemChargesMk 20

-/-- THe vector spaces of charges of one species of fermions in the MSSM. -/
+/-- The vector spaces of charges of one species of fermions in the MSSM. -/
@[simps!]
 def MSSMSpecies : ACCSystemCharges := ACCSystemChargesMk 3

--- a/HepLean/AnomalyCancellation/MSSMNu/HyperCharge.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/HyperCharge.lean
@ -0,0 +1,54 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.AnomalyCancellation.MSSMNu.Basic
+import Mathlib.Tactic.Polyrith
+/-!
+# Hypercharge in MSSM.
+
+Relavent definitions for the MSSM hypercharge.
+
+-/
+
+universe v u
+
+namespace MSSMACC
+open MSSMCharges
+open MSSMACCs
+open BigOperators
+
+/-- The hypercharge as an element of `MSSMACC.charges`. -/
+def YAsCharge : MSSMACC.charges := toSpecies.invFun
+  ⟨fun s => fun i =>
+    match s, i with
+    | 0, 0 => 1
+    | 0, 1 => 1
+    | 0, 2 => 1
+    | 1, 0 => -4
+    | 1, 1 => -4
+    | 1, 2 => -4
+    | 2, 0 => 2
+    | 2, 1 => 2
+    | 2, 2 => 2
+    | 3, 0 => -3
+    | 3, 1 => -3
+    | 3, 2 => -3
+    | 4, 0 => 6
+    | 4, 1 => 6
+    | 4, 2 => 6
+    | 5, 0 => 0
+    | 5, 1 => 0
+    | 5, 2 => 0,
+  fun s =>
+    match s with
+    | 0 => -3
+    | 1 => 3⟩
+
+/-- The hypercharge as an element of `MSSMACC.Sols`. -/
+def Y : MSSMACC.Sols :=
+  MSSMACC.AnomalyFreeMk YAsCharge (by rfl) (by rfl) (by rfl) (by rfl) (by rfl) (by rfl)
+
+
+end MSSMACC
--- a/HepLean/AnomalyCancellation/MSSMNu/LineY3B3.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/LineY3B3.lean
@ -0,0 +1,92 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.AnomalyCancellation.MSSMNu.Basic
+import HepLean.AnomalyCancellation.MSSMNu.Y3
+import HepLean.AnomalyCancellation.MSSMNu.B3
+import Mathlib.Tactic.Polyrith
+/-!
+# The line through B₃ and Y₃
+
+We give properties of lines through `B₃` and `Y₃`. We show that every point on this line
+is a solution to the quadratic  `lineY₃B₃Charges_quad` and a double point of the cubic
+`lineY₃B₃_doublePoint`.
+
+# References
+
+The main reference for the material in this file is:
+
+- https://arxiv.org/pdf/2107.07926.pdf
+
+-/
+
+universe v u
+
+namespace MSSMACC
+open MSSMCharges
+open MSSMACCs
+open BigOperators
+
+/-- The line through $Y_3$ and $B_3$ as `LinSols`. -/
+def lineY₃B₃Charges (a b : ℚ) : MSSMACC.LinSols := a • Y₃.1.1 + b • B₃.1.1
+
+lemma lineY₃B₃Charges_quad (a b : ℚ) : accQuad (lineY₃B₃Charges a b).val = 0 := by
+  change accQuad (a • Y₃.val + b • B₃.val) = 0
+  rw [accQuad]
+  rw [quadBiLin.toHomogeneousQuad_add]
+  rw [quadBiLin.toHomogeneousQuad.map_smul]
+  rw [quadBiLin.toHomogeneousQuad.map_smul]
+  rw [quadBiLin.map_smul₁, quadBiLin.map_smul₂]
+  erw [quadSol Y₃.1, quadSol B₃.1]
+  simp
+  apply Or.inr ∘ Or.inr
+  rfl
+
+lemma lineY₃B₃Charges_cubic (a b : ℚ) : accCube (lineY₃B₃Charges a b).val = 0 := by
+  change accCube (a • Y₃.val + b • B₃.val) = 0
+  rw [accCube]
+  rw [cubeTriLin.toCubic_add]
+  rw [cubeTriLin.toCubic.map_smul]
+  rw [cubeTriLin.toCubic.map_smul]
+  rw [cubeTriLin.map_smul₁, cubeTriLin.map_smul₂, cubeTriLin.map_smul₃]
+  rw [cubeTriLin.map_smul₁, cubeTriLin.map_smul₂, cubeTriLin.map_smul₃]
+  erw [Y₃.cubicSol,  B₃.cubicSol]
+  rw [show cubeTriLin (Y₃.val, Y₃.val, B₃.val) = 0 by rfl]
+  rw [show cubeTriLin (B₃.val, B₃.val, Y₃.val) = 0 by rfl]
+  simp
+
+/-- The line through $Y_3$ and $B_3$ as `Sols`. -/
+def lineY₃B₃ (a b : ℚ) : MSSMACC.Sols :=
+  AnomalyFreeMk' (lineY₃B₃Charges a b) (lineY₃B₃Charges_quad a b) (lineY₃B₃Charges_cubic a b)
+
+lemma doublePoint_Y₃_B₃ (R : MSSMACC.LinSols) :
+    cubeTriLin (Y₃.val, B₃.val, R.val) = 0 := by
+  rw [← TriLinearSymm.toFun_eq_coe]
+  simp only [cubeTriLin, cubeTriLinToFun, MSSMSpecies_numberCharges]
+  rw [Fin.sum_univ_three]
+  rw [B₃_val, Y₃_val]
+  rw [B₃AsCharge, Y₃AsCharge]
+  repeat rw [toSMSpecies_toSpecies_inv]
+  rw [Hd_toSpecies_inv, Hu_toSpecies_inv]
+  rw [Hd_toSpecies_inv, Hu_toSpecies_inv]
+  simp
+  have hLin := R.linearSol
+  simp at hLin
+  have h1 := hLin 1
+  have h2 := hLin 2
+  have h3 := hLin 3
+  simp [Fin.sum_univ_three] at h1 h2 h3
+  linear_combination -(12 * h2) + 9 * h1 + 3 * h3
+
+lemma lineY₃B₃_doublePoint (R : MSSMACC.LinSols) (a b : ℚ) :
+    cubeTriLin ((lineY₃B₃ a b).val, (lineY₃B₃ a b).val, R.val) = 0 := by
+  change cubeTriLin (a • Y₃.val + b • B₃.val , a • Y₃.val + b • B₃.val, R.val ) = 0
+  rw [cubeTriLin.map_add₂, cubeTriLin.map_add₁, cubeTriLin.map_add₁]
+  repeat rw [cubeTriLin.map_smul₂, cubeTriLin.map_smul₁]
+  rw [doublePoint_B₃_B₃, doublePoint_Y₃_Y₃, doublePoint_Y₃_B₃]
+  rw [cubeTriLin.swap₁, doublePoint_Y₃_B₃]
+  simp
+
+end MSSMACC
--- a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3.lean
@ -0,0 +1,191 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.AnomalyCancellation.MSSMNu.Basic
+import HepLean.AnomalyCancellation.MSSMNu.LineY3B3
+import Mathlib.Tactic.Polyrith
+import Mathlib.Tactic.Linarith
+/-!
+# The type of solutions perpendicular to `Y₃` and `B₃`
+
+We define the type of solutions which are orthogonal to `Y₃` and `B₃` and prove some basic lemmas
+about them.
+
+# References
+
+The main reference for the material in this file is:
+
+- https://arxiv.org/pdf/2107.07926.pdf
+
+-/
+universe v u
+
+namespace MSSMACC
+open MSSMCharges
+open MSSMACCs
+open BigOperators
+
+/-- The type of linear solutions orthogonal to $Y_3$ and $B_3$. -/
+structure AnomalyFreePerp extends MSSMACC.LinSols where
+  perpY₃ : dot (Y₃.val, val) = 0
+  perpB₃ : dot (B₃.val, val) = 0
+
+/-- The projection of an object in `MSSMACC.AnomalyFreeLinear` onto the subspace
+  orthgonal to `Y₃` and`B₃`. -/
+def proj (T : MSSMACC.LinSols) : MSSMACC.AnomalyFreePerp :=
+  ⟨(dot (B₃.val, T.val) - dot (Y₃.val, T.val)) • Y₃.1.1
+  + (dot (Y₃.val, T.val) - 2 * dot (B₃.val, T.val)) • B₃.1.1
+  + dot (Y₃.val, B₃.val) • T,
+  by
+    change dot (_, _ • Y₃.val + _ • B₃.val + _ • T.val) = 0
+    rw [dot.map_add₂, dot.map_add₂]
+    rw [dot.map_smul₂, dot.map_smul₂, dot.map_smul₂]
+    rw [show dot (Y₃.val, B₃.val) = 108 by rfl]
+    rw [show dot (Y₃.val, Y₃.val) = 216 by rfl]
+    ring,
+  by
+    change dot (_, _ • Y₃.val + _ • B₃.val + _ • T.val) = 0
+    rw [dot.map_add₂, dot.map_add₂]
+    rw [dot.map_smul₂, dot.map_smul₂, dot.map_smul₂]
+    rw [show dot (Y₃.val, B₃.val) = 108 by rfl]
+    rw [show dot (B₃.val, Y₃.val) = 108 by rfl]
+    rw [show dot (B₃.val, B₃.val) = 108 by rfl]
+    ring⟩
+
+lemma proj_val (T : MSSMACC.LinSols) :
+    (proj T).val = (dot (B₃.val, T.val) - dot (Y₃.val, T.val)) • Y₃.val +
+    ( (dot (Y₃.val, T.val) - 2 * dot (B₃.val, T.val))) • B₃.val +
+    dot (Y₃.val, B₃.val) • T.val := by
+  rfl
+
+lemma Y₃_plus_B₃_plus_proj (T : MSSMACC.LinSols) (a b c : ℚ) :
+    a • Y₃.val + b • B₃.val + c • (proj T).val =
+    (a + c * (dot (B₃.val, T.val) - dot (Y₃.val, T.val))) • Y₃.val
+    + (b + c * (dot (Y₃.val, T.val) - 2 * dot (B₃.val, T.val))) • B₃.val
+    + (dot (Y₃.val, B₃.val) * c) • T.val:= by
+  rw [proj_val]
+  rw [DistribMulAction.smul_add, DistribMulAction.smul_add]
+  rw [add_assoc (_ • _ • Y₃.val), ← add_assoc (_ • Y₃.val + _ • B₃.val), add_assoc (_ • Y₃.val)]
+  rw [add_comm (_ • B₃.val) (_ • _ • Y₃.val), ← add_assoc (_ • Y₃.val)]
+  rw [← MulAction.mul_smul, ← Module.add_smul]
+  repeat rw [add_assoc]
+  apply congrArg
+  rw [← add_assoc, ← MulAction.mul_smul, ← Module.add_smul]
+  apply congrArg
+  simp only [HSMul.hSMul, SMul.smul, MSSMACC_numberCharges, Fin.isValue, Fin.reduceFinMk]
+  funext i
+  linarith
+
+
+
+lemma quad_Y₃_proj (T : MSSMACC.LinSols) :
+    quadBiLin (Y₃.val, (proj T).val) = dot (Y₃.val, B₃.val) * quadBiLin (Y₃.val, T.val) := by
+  rw [proj_val]
+  rw [quadBiLin.map_add₂, quadBiLin.map_add₂]
+  rw [quadBiLin.map_smul₂, quadBiLin.map_smul₂, quadBiLin.map_smul₂]
+  rw [show quadBiLin (Y₃.val, B₃.val) = 0 by rfl]
+  rw [show quadBiLin (Y₃.val, Y₃.val) = 0 by rfl]
+  ring
+
+lemma quad_B₃_proj (T : MSSMACC.LinSols) :
+    quadBiLin (B₃.val, (proj T).val) = dot (Y₃.val, B₃.val) * quadBiLin (B₃.val, T.val) := by
+  rw [proj_val]
+  rw [quadBiLin.map_add₂, quadBiLin.map_add₂]
+  rw [quadBiLin.map_smul₂, quadBiLin.map_smul₂, quadBiLin.map_smul₂]
+  rw [show quadBiLin (B₃.val, Y₃.val) = 0 by rfl]
+  rw [show quadBiLin (B₃.val, B₃.val) = 0 by rfl]
+  ring
+
+lemma quad_self_proj (T : MSSMACC.Sols) :
+    quadBiLin (T.val, (proj T.1.1).val) =
+    (dot (B₃.val, T.val) - dot (Y₃.val, T.val)) * quadBiLin (Y₃.val, T.val) +
+    (dot (Y₃.val, T.val) - 2 * dot (B₃.val, T.val)) * quadBiLin (B₃.val, T.val) := by
+  rw [proj_val]
+  rw [quadBiLin.map_add₂, quadBiLin.map_add₂]
+  rw [quadBiLin.map_smul₂, quadBiLin.map_smul₂, quadBiLin.map_smul₂]
+  erw [quadSol T.1]
+  rw [quadBiLin.swap T.val Y₃.val, quadBiLin.swap T.val B₃.val]
+  ring
+
+lemma quad_proj (T : MSSMACC.Sols) :
+    quadBiLin ((proj T.1.1).val, (proj T.1.1).val) = 2 * (dot (Y₃.val, B₃.val)) *
+     ((dot (B₃.val, T.val) - dot (Y₃.val, T.val)) * quadBiLin (Y₃.val, T.val) +
+   (dot (Y₃.val, T.val) - 2 * dot (B₃.val, T.val)) * quadBiLin (B₃.val, T.val) ) := by
+  nth_rewrite 1 [proj_val]
+  repeat rw [quadBiLin.map_add₁]
+  repeat rw [quadBiLin.map_smul₁]
+  rw [quad_Y₃_proj, quad_B₃_proj, quad_self_proj]
+  ring
+
+
+lemma cube_proj_proj_Y₃ (T : MSSMACC.LinSols) :
+    cubeTriLin ((proj T).val, (proj T).val, Y₃.val) =
+    (dot (Y₃.val, B₃.val))^2 * cubeTriLin (T.val, T.val, Y₃.val):= by
+  rw [proj_val]
+  rw [cubeTriLin.map_add₁, cubeTriLin.map_add₂]
+  erw [lineY₃B₃_doublePoint]
+  rw [cubeTriLin.map_add₂]
+  rw [cubeTriLin.swap₂]
+  rw [cubeTriLin.map_add₁, cubeTriLin.map_smul₁, cubeTriLin.map_smul₃]
+  rw [doublePoint_Y₃_Y₃]
+  rw [cubeTriLin.map_smul₁, cubeTriLin.map_smul₃, cubeTriLin.swap₁]
+  rw [doublePoint_Y₃_B₃]
+  rw [cubeTriLin.map_add₂]
+  rw [cubeTriLin.map_smul₁, cubeTriLin.map_smul₂]
+  rw [cubeTriLin.swap₁, cubeTriLin.swap₂]
+  rw [doublePoint_Y₃_Y₃]
+  rw [cubeTriLin.map_smul₁, cubeTriLin.map_smul₂]
+  rw [cubeTriLin.swap₁, cubeTriLin.swap₂, cubeTriLin.swap₁]
+  rw [doublePoint_Y₃_B₃]
+  rw [cubeTriLin.map_smul₁, cubeTriLin.map_smul₂]
+  ring
+
+lemma cube_proj_proj_B₃ (T : MSSMACC.LinSols) :
+    cubeTriLin ((proj T).val, (proj T).val, B₃.val) =
+    (dot (Y₃.val, B₃.val))^2 * cubeTriLin (T.val, T.val, B₃.val):= by
+  rw [proj_val]
+  rw [cubeTriLin.map_add₁, cubeTriLin.map_add₂]
+  erw [lineY₃B₃_doublePoint]
+  rw [cubeTriLin.map_add₂, cubeTriLin.swap₂, cubeTriLin.map_add₁, cubeTriLin.map_smul₁,
+    cubeTriLin.map_smul₃, doublePoint_Y₃_B₃]
+  rw [cubeTriLin.map_smul₁, cubeTriLin.map_smul₃, cubeTriLin.swap₁, doublePoint_B₃_B₃]
+  rw [cubeTriLin.map_add₂, cubeTriLin.map_smul₁, cubeTriLin.map_smul₂]
+  rw [cubeTriLin.swap₁, cubeTriLin.swap₂, doublePoint_Y₃_B₃]
+  rw [cubeTriLin.map_smul₁, cubeTriLin.map_smul₂, cubeTriLin.swap₁, cubeTriLin.swap₂,
+   cubeTriLin.swap₁, doublePoint_B₃_B₃]
+  rw [cubeTriLin.map_smul₁, cubeTriLin.map_smul₂]
+  ring
+
+lemma cube_proj_proj_self (T : MSSMACC.Sols) :
+    cubeTriLin ((proj T.1.1).val, (proj T.1.1).val, T.val) =
+    2 * dot (Y₃.val, B₃.val) *
+    ((dot (B₃.val, T.val) - dot (Y₃.val, T.val)) * cubeTriLin (T.val, T.val, Y₃.val)  +
+    ( dot (Y₃.val, T.val)- 2 * dot (B₃.val, T.val)) * cubeTriLin (T.val, T.val, B₃.val)) := by
+  rw [proj_val]
+  rw [cubeTriLin.map_add₁, cubeTriLin.map_add₂]
+  erw [lineY₃B₃_doublePoint]
+  repeat rw [cubeTriLin.map_add₁]
+  repeat rw [cubeTriLin.map_smul₁]
+  repeat rw [cubeTriLin.map_add₂]
+  repeat rw [cubeTriLin.map_smul₂]
+  erw [T.cubicSol]
+  rw [cubeTriLin.swap₁ Y₃.val T.val T.val, cubeTriLin.swap₂ T.val  Y₃.val T.val]
+  rw [cubeTriLin.swap₁ B₃.val T.val T.val, cubeTriLin.swap₂ T.val  B₃.val T.val]
+  ring
+
+lemma cube_proj (T : MSSMACC.Sols) :
+    cubeTriLin ((proj T.1.1).val, (proj T.1.1).val, (proj T.1.1).val) =
+    3 *  dot (Y₃.val, B₃.val) ^ 2 *
+    ((dot (B₃.val, T.val) - dot (Y₃.val, T.val)) * cubeTriLin (T.val, T.val, Y₃.val) +
+        (dot (Y₃.val, T.val) - 2 * dot (B₃.val, T.val)) * cubeTriLin (T.val, T.val, B₃.val)) := by
+  nth_rewrite 3 [proj_val]
+  repeat rw [cubeTriLin.map_add₃]
+  repeat rw [cubeTriLin.map_smul₃]
+  rw [cube_proj_proj_Y₃, cube_proj_proj_B₃, cube_proj_proj_self]
+  ring
+
+
+
+end MSSMACC
--- a/HepLean/AnomalyCancellation/MSSMNu/Permutations.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/Permutations.lean
@ -0,0 +1,156 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.AnomalyCancellation.MSSMNu.Basic
+import Mathlib.Tactic.Polyrith
+import HepLean.AnomalyCancellation.GroupActions
+universe v u
+/-!
+# Permutations of MSSM charges and solutions
+
+The three family MSSM charges has a family permutation of S₃⁶. This file defines this group
+and its action on the MSSM.
+
+-/
+open Nat
+open  Finset
+
+namespace MSSM
+
+open MSSMCharges
+open MSSMACCs
+open BigOperators
+
+/-- The group of family permutations is `S₃⁶`-/
+@[simp]
+def permGroup := Fin 6 → Equiv.Perm (Fin 3)
+
+@[simp]
+instance  : Group permGroup := Pi.group
+
+/-- The image of an element of `permGroup` under the representation on charges. -/
+@[simps!]
+def chargeMap (f : permGroup) : MSSMCharges.charges →ₗ[ℚ] MSSMCharges.charges where
+  toFun S := toSpecies.symm (fun i => toSMSpecies i S ∘ f i, Prod.snd (toSpecies S))
+  map_add' S T := by
+    simp only
+    rw [charges_eq_toSpecies_eq]
+    apply And.intro
+    intro i
+    rw [(toSMSpecies i).map_add]
+    rw [toSMSpecies_toSpecies_inv, toSMSpecies_toSpecies_inv, toSMSpecies_toSpecies_inv]
+    simp only
+    erw [(toSMSpecies i).map_add]
+    rfl
+    apply And.intro
+    rw [Hd.map_add, Hd_toSpecies_inv, Hd_toSpecies_inv, Hd_toSpecies_inv]
+    rfl
+    rw [Hu.map_add, Hu_toSpecies_inv, Hu_toSpecies_inv, Hu_toSpecies_inv]
+    rfl
+  map_smul' a S := by
+    simp only
+    rw [charges_eq_toSpecies_eq]
+    apply And.intro
+    intro i
+    rw [(toSMSpecies i).map_smul, toSMSpecies_toSpecies_inv, toSMSpecies_toSpecies_inv]
+    rfl
+    apply And.intro
+    rfl
+    rfl
+
+lemma chargeMap_toSpecies (f : permGroup) (S : MSSMCharges.charges) (j : Fin 6) :
+    toSMSpecies j (chargeMap f S) = toSMSpecies j S ∘ f j := by
+  erw [toSMSpecies_toSpecies_inv]
+
+/-- The representation of `permGroup` acting on the vector space of charges. -/
+@[simp]
+def repCharges : Representation ℚ (permGroup) (MSSMCharges).charges where
+  toFun f := chargeMap f⁻¹
+  map_mul' f g :=by
+    simp only [permGroup, mul_inv_rev]
+    apply LinearMap.ext
+    intro S
+    rw [charges_eq_toSpecies_eq]
+    apply And.intro
+    intro i
+    simp only [ Pi.mul_apply, Pi.inv_apply, Equiv.Perm.coe_mul, LinearMap.mul_apply]
+    rw [chargeMap_toSpecies, chargeMap_toSpecies]
+    simp only [Pi.mul_apply, Pi.inv_apply]
+    rw [chargeMap_toSpecies]
+    rfl
+    apply And.intro
+    rfl
+    rfl
+  map_one' := by
+    apply LinearMap.ext
+    intro S
+    rw [charges_eq_toSpecies_eq]
+    apply And.intro
+    intro i
+    erw [toSMSpecies_toSpecies_inv]
+    rfl
+    apply And.intro
+    rfl
+    rfl
+
+lemma repCharges_toSMSpecies (f : permGroup) (S : MSSMCharges.charges) (j : Fin 6) :
+    toSMSpecies j (repCharges f S) = toSMSpecies j S ∘ f⁻¹ j := by
+  erw [toSMSpecies_toSpecies_inv]
+
+lemma toSpecies_sum_invariant (m : ℕ) (f : permGroup) (S : MSSMCharges.charges) (j : Fin 6) :
+    ∑ i, ((fun a => a ^ m) ∘ toSMSpecies j (repCharges f S)) i =
+    ∑ i, ((fun a => a ^ m) ∘ toSMSpecies j S) i := by
+  erw [repCharges_toSMSpecies]
+  change  ∑ i : Fin 3, ((fun a => a ^ m) ∘ _) (⇑(f⁻¹ _) i) = ∑ i : Fin 3, ((fun a => a ^ m) ∘ _) i
+  refine Equiv.Perm.sum_comp _ _ _ ?_
+  simp only [permGroup, Fin.isValue, Pi.inv_apply, ne_eq, coe_univ, Set.subset_univ]
+
+lemma Hd_invariant (f : permGroup) (S : MSSMCharges.charges)  :
+    Hd (repCharges f S) = Hd S := rfl
+
+lemma Hu_invariant (f : permGroup) (S : MSSMCharges.charges)  :
+    Hu (repCharges f S) = Hu S := rfl
+
+lemma accGrav_invariant (f : permGroup) (S : MSSMCharges.charges)  :
+    accGrav (repCharges f S) = accGrav S :=
+  accGrav_ext
+    (by simpa using toSpecies_sum_invariant 1 f S)
+    (Hd_invariant f S)
+    (Hu_invariant f S)
+
+lemma accSU2_invariant (f : permGroup) (S : MSSMCharges.charges)  :
+    accSU2 (repCharges f S) = accSU2 S :=
+  accSU2_ext
+    (by simpa using toSpecies_sum_invariant 1 f S)
+    (Hd_invariant f S)
+    (Hu_invariant f S)
+
+lemma accSU3_invariant (f : permGroup) (S : MSSMCharges.charges)  :
+    accSU3 (repCharges f S) = accSU3 S :=
+  accSU3_ext
+    (by simpa using toSpecies_sum_invariant 1 f S)
+
+lemma accYY_invariant (f : permGroup) (S : MSSMCharges.charges)  :
+    accYY (repCharges f S) = accYY S :=
+  accYY_ext
+    (by simpa using toSpecies_sum_invariant 1 f S)
+    (Hd_invariant f S)
+    (Hu_invariant f S)
+
+lemma accQuad_invariant (f : permGroup) (S : MSSMCharges.charges)  :
+    accQuad (repCharges f S) = accQuad S :=
+  accQuad_ext
+    (toSpecies_sum_invariant 2 f S)
+    (Hd_invariant f S)
+    (Hu_invariant f S)
+
+lemma accCube_invariant (f : permGroup) (S : MSSMCharges.charges)  :
+    accCube (repCharges f S) = accCube S :=
+  accCube_ext
+    (by simpa using toSpecies_sum_invariant 3 f S)
+    (Hd_invariant f S)
+    (Hu_invariant f S)
+
+end MSSM
--- a/HepLean/AnomalyCancellation/MSSMNu/PlaneY3B3Orthog.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/PlaneY3B3Orthog.lean
@ -0,0 +1,255 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.AnomalyCancellation.MSSMNu.Basic
+import HepLean.AnomalyCancellation.MSSMNu.LineY3B3
+import HepLean.AnomalyCancellation.MSSMNu.OrthogY3B3
+import Mathlib.Tactic.Polyrith
+/-!
+# Plane Y₃ B₃ and an orthogonal third point
+
+The plane spanned by Y₃, B₃ and third orthogonal point.
+
+# References
+
+- https://arxiv.org/pdf/2107.07926.pdf
+
+-/
+
+
+
+universe v u
+
+namespace MSSMACC
+open MSSMCharges
+open MSSMACCs
+open BigOperators
+
+/-- The plane of linear solutions spanned by $Y_3$, $B_3$ and $R$, a point orthogonal
+to $Y_3$ and $B_3$. -/
+def planeY₃B₃ (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) : MSSMACC.LinSols :=
+  a • Y₃.1.1 + b • B₃.1.1 + c • R.1
+
+lemma planeY₃B₃_val (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) :
+    (planeY₃B₃ R a b c).val = a • Y₃.val + b • B₃.val + c • R.val := by
+  rfl
+
+lemma planeY₃B₃_smul (R : MSSMACC.AnomalyFreePerp) (a b c d : ℚ) :
+    planeY₃B₃ R (d * a) (d * b) (d * c) = d • planeY₃B₃ R a b c := by
+  apply ACCSystemLinear.LinSols.ext
+  change _ = d • (planeY₃B₃ R a b c).val
+  rw [planeY₃B₃_val, planeY₃B₃_val]
+  rw [smul_add, smul_add]
+  rw [smul_smul, smul_smul, smul_smul]
+
+
+lemma planeY₃B₃_eq (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) (h :  a = a' ∧ b = b' ∧ c = c') :
+    (planeY₃B₃ R a b c) = (planeY₃B₃ R a' b' c') := by
+  rw [h.1, h.2.1, h.2.2]
+
+lemma planeY₃B₃_val_eq' (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) (hR' : R.val ≠ 0)
+    (h : (planeY₃B₃ R a b c).val = (planeY₃B₃ R a' b' c').val) :
+     a = a' ∧ b = b' ∧ c = c' := by
+  rw [planeY₃B₃_val, planeY₃B₃_val] at h
+  have h1 := congrArg (fun S => dot (Y₃.val, S)) h
+  have h2 := congrArg (fun S => dot (B₃.val, S)) h
+  simp only [ Fin.isValue, ACCSystemCharges.chargesAddCommMonoid_add, Fin.reduceFinMk] at h1 h2
+  erw [dot.map_add₂, dot.map_add₂] at h1 h2
+  erw [dot.map_add₂ Y₃.val (a' • Y₃.val + b' • B₃.val) (c' • R.val)] at h1
+  erw [dot.map_add₂ B₃.val (a' • Y₃.val + b' • B₃.val) (c' • R.val)] at h2
+  rw [dot.map_add₂] at h1 h2
+  rw [dot.map_smul₂, dot.map_smul₂, dot.map_smul₂] at h1 h2
+  rw [dot.map_smul₂, dot.map_smul₂, dot.map_smul₂] at h1 h2
+  rw [R.perpY₃] at h1
+  rw [R.perpB₃] at h2
+  rw [show dot (Y₃.val, Y₃.val) = 216 by rfl] at h1
+  rw [show dot (B₃.val, B₃.val) = 108 by rfl] at h2
+  rw [show dot (Y₃.val, B₃.val) = 108 by rfl] at h1
+  rw [show dot (B₃.val, Y₃.val) = 108 by rfl] at h2
+  simp_all
+  have ha : a = a' := by
+    linear_combination h1 / 108 + -1 * h2 / 108
+  have hb : b = b' := by
+    linear_combination -1 * h1 / 108 + h2 / 54
+  rw [ha, hb] at h
+  have h1 := add_left_cancel h
+  have h1i : c • R.val + (- c') • R.val = 0 := by
+    rw [h1]
+    rw [← Module.add_smul]
+    simp
+  rw [← Module.add_smul] at h1i
+  have hR : ∃ i, R.val i ≠ 0 := by
+    by_contra h
+    simp at h
+    have h0 : R.val = 0 := by
+      funext i
+      apply h i
+    exact hR' h0
+  obtain ⟨i, hi⟩ := hR
+  have h2 := congrArg (fun S => S i) h1i
+  change _ = 0 at h2
+  simp [HSMul.hSMul] at h2
+  have hc :  c + -c' = 0 := by
+    cases h2 <;> rename_i h2
+    exact h2
+    exact (hi h2).elim
+  have hc : c = c' := by
+    linear_combination hc
+  rw [ha, hb, hc]
+  simp
+
+
+lemma planeY₃B₃_quad (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) :
+    accQuad (planeY₃B₃ R a b c).val = c * (2 * a * quadBiLin (Y₃.val, R.val)
+    + 2 * b * quadBiLin (B₃.val, R.val) + c * quadBiLin (R.val, R.val)) := by
+  rw [planeY₃B₃_val]
+  erw [BiLinearSymm.toHomogeneousQuad_add]
+  erw [lineY₃B₃Charges_quad]
+  rw [quadBiLin.toHomogeneousQuad.map_smul]
+  rw [quadBiLin.map_add₁, quadBiLin.map_smul₁, quadBiLin.map_smul₁]
+  rw [quadBiLin.map_smul₂, quadBiLin.map_smul₂]
+  rw [show (BiLinearSymm.toHomogeneousQuad quadBiLin) R.val = quadBiLin (R.val, R.val) by rfl]
+  ring
+
+lemma planeY₃B₃_cubic (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) :
+    accCube (planeY₃B₃ R a b c).val = c ^ 2 *
+    (3 * a *  cubeTriLin (R.val, R.val, Y₃.val)
+    + 3 * b *  cubeTriLin (R.val, R.val, B₃.val) + c * cubeTriLin (R.val, R.val, R.val) ) := by
+  rw [planeY₃B₃_val]
+  erw [TriLinearSymm.toCubic_add]
+  erw [lineY₃B₃Charges_cubic]
+  erw [lineY₃B₃_doublePoint (c • R.1) a b]
+  rw [cubeTriLin.toCubic.map_smul]
+  rw [cubeTriLin.map_smul₁, cubeTriLin.map_smul₂]
+  rw [cubeTriLin.map_add₃, cubeTriLin.map_smul₃, cubeTriLin.map_smul₃]
+  rw [show (TriLinearSymm.toCubic cubeTriLin) R.val = cubeTriLin (R.val, R.val, R.val) by rfl]
+  ring
+
+/-- The line in the plane spanned by $Y_3$, $B_3$ and $R$ which is in the quadratic,
+as `LinSols`. -/
+def lineQuadAFL (R : MSSMACC.AnomalyFreePerp) (c1 c2 c3 : ℚ) : MSSMACC.LinSols :=
+  planeY₃B₃ R (c2 * quadBiLin (R.val, R.val) - 2 * c3 * quadBiLin (B₃.val, R.val))
+  (2 * c3 * quadBiLin (Y₃.val, R.val) - c1 * quadBiLin (R.val, R.val))
+  (2 * c1 * quadBiLin (B₃.val, R.val) - 2 * c2 * quadBiLin (Y₃.val, R.val))
+
+lemma lineQuadAFL_quad (R : MSSMACC.AnomalyFreePerp) (c1 c2 c3 : ℚ) :
+    accQuad (lineQuadAFL R c1 c2 c3).val = 0 := by
+  erw [planeY₃B₃_quad]
+  rw [mul_eq_zero]
+  apply Or.inr
+  ring
+
+/-- The line in the plane spanned by $Y_3$, $B_3$ and $R$ which is in the quadratic. -/
+def lineQuad (R : MSSMACC.AnomalyFreePerp) (c1 c2 c3 : ℚ) : MSSMACC.QuadSols :=
+  AnomalyFreeQuadMk' (lineQuadAFL R c1 c2 c3) (lineQuadAFL_quad R c1 c2 c3)
+
+lemma lineQuad_val (R : MSSMACC.AnomalyFreePerp) (c1 c2 c3 : ℚ) :
+    (lineQuad R c1 c2 c3).val = (planeY₃B₃ R
+    (c2 * quadBiLin (R.val, R.val) - 2 * c3 * quadBiLin (B₃.val, R.val))
+    (2 * c3 * quadBiLin (Y₃.val, R.val) - c1 * quadBiLin (R.val, R.val))
+    (2 * c1 * quadBiLin (B₃.val, R.val) - 2 * c2 * quadBiLin (Y₃.val, R.val))).val  := by
+  rfl
+
+lemma lineQuad_smul (R : MSSMACC.AnomalyFreePerp) (a b c d : ℚ) :
+    lineQuad R (d * a) (d * b) (d * c) = d • lineQuad R a b c := by
+  apply ACCSystemQuad.QuadSols.ext
+  change _ = (d • planeY₃B₃ R _ _ _).val
+  rw [← planeY₃B₃_smul]
+  rw [lineQuad_val]
+  congr 2
+  ring_nf
+
+/-- A helper function to simplify following expressions. -/
+def α₁ (T : MSSMACC.AnomalyFreePerp) : ℚ :=
+  (3 * cubeTriLin (T.val, T.val, B₃.val) * quadBiLin (T.val, T.val) -
+   2 * cubeTriLin (T.val, T.val, T.val) * quadBiLin (B₃.val, T.val))
+
+/-- A helper function to simplify following expressions. -/
+def α₂ (T : MSSMACC.AnomalyFreePerp) : ℚ :=
+  (2 * cubeTriLin (T.val, T.val, T.val) * quadBiLin (Y₃.val, T.val) -
+  3 * cubeTriLin (T.val, T.val, Y₃.val) * quadBiLin (T.val, T.val))
+
+/-- A helper function to simplify following expressions. -/
+def α₃ (T : MSSMACC.AnomalyFreePerp) : ℚ :=
+  6 * ((cubeTriLin (T.val, T.val, Y₃.val)) * quadBiLin (B₃.val, T.val) -
+      (cubeTriLin (T.val, T.val, B₃.val)) * quadBiLin (Y₃.val, T.val))
+
+lemma lineQuad_cube (R : MSSMACC.AnomalyFreePerp) (c₁ c₂ c₃ : ℚ) :
+    accCube (lineQuad R c₁ c₂ c₃).val =
+    - 4 * ( c₁ * quadBiLin (B₃.val, R.val) - c₂ * quadBiLin (Y₃.val, R.val)) ^ 2 *
+    ( α₁ R * c₁ + α₂ R * c₂ + α₃ R * c₃ ) := by
+  rw [lineQuad_val]
+  rw [planeY₃B₃_cubic, α₁, α₂, α₃]
+  ring
+
+/-- The line in the plane spanned by $Y_3$, $B_3$ and $R$ which is in the cubic. -/
+def lineCube (R : MSSMACC.AnomalyFreePerp) (a₁ a₂ a₃ : ℚ) :
+    MSSMACC.LinSols :=
+  planeY₃B₃ R
+    (a₂ * cubeTriLin (R.val, R.val, R.val) - 3 * a₃ * cubeTriLin (R.val, R.val, B₃.val))
+    (3 * a₃ * cubeTriLin (R.val, R.val, Y₃.val) -  a₁ * cubeTriLin (R.val, R.val, R.val))
+    (3 * (a₁ * cubeTriLin (R.val, R.val, B₃.val) - a₂ * cubeTriLin (R.val, R.val, Y₃.val)))
+
+
+lemma lineCube_smul (R : MSSMACC.AnomalyFreePerp) (a b c d : ℚ) :
+    lineCube R (d * a) (d * b) (d * c) = d • lineCube R a b c := by
+  apply ACCSystemLinear.LinSols.ext
+  change _ = (d • planeY₃B₃ R _ _ _).val
+  rw [← planeY₃B₃_smul]
+  change (planeY₃B₃ R _ _ _).val = (planeY₃B₃ R _ _ _).val
+  congr 2
+  ring_nf
+
+lemma lineCube_cube (R : MSSMACC.AnomalyFreePerp) (a₁ a₂ a₃ : ℚ) :
+    accCube (lineCube R a₁ a₂ a₃).val = 0 := by
+  change accCube (planeY₃B₃ R _ _ _).val = 0
+  rw [planeY₃B₃_cubic]
+  ring_nf
+
+lemma lineCube_quad (R : MSSMACC.AnomalyFreePerp) (a₁ a₂ a₃ : ℚ) :
+    accQuad (lineCube R a₁ a₂ a₃).val =
+    3 * (a₁ * cubeTriLin (R.val, R.val, B₃.val) - a₂ * cubeTriLin (R.val, R.val, Y₃.val)) *
+    (α₁ R * a₁ + α₂ R * a₂ + α₃ R * a₃) := by
+  erw [planeY₃B₃_quad]
+  rw [α₁, α₂, α₃]
+  ring
+
+
+section proj
+
+lemma α₃_proj  (T : MSSMACC.Sols) : α₃ (proj T.1.1) =
+    6 * dot (Y₃.val, B₃.val) ^ 3 * (
+    cubeTriLin (T.val, T.val, Y₃.val) * quadBiLin (B₃.val, T.val) -
+    cubeTriLin (T.val, T.val, B₃.val) * quadBiLin (Y₃.val, T.val)) := by
+  rw [α₃]
+  rw [cube_proj_proj_Y₃, cube_proj_proj_B₃, quad_B₃_proj, quad_Y₃_proj]
+  ring
+
+lemma α₂_proj (T : MSSMACC.Sols) : α₂ (proj T.1.1) =
+    - α₃ (proj T.1.1) * (dot (Y₃.val, T.val) - 2 * dot (B₃.val, T.val))   := by
+  rw [α₃_proj, α₂]
+  rw [cube_proj_proj_Y₃, quad_Y₃_proj, quad_proj, cube_proj]
+  ring
+
+lemma α₁_proj (T : MSSMACC.Sols) : α₁ (proj T.1.1) =
+    - α₃ (proj T.1.1) * (dot (B₃.val, T.val) - dot (Y₃.val, T.val))   := by
+  rw [α₃_proj, α₁]
+  rw [cube_proj_proj_B₃, quad_B₃_proj, quad_proj, cube_proj]
+  ring
+
+lemma α₁_proj_zero (T : MSSMACC.Sols) (h1 : α₃ (proj T.1.1) = 0) :
+    α₁ (proj T.1.1) = 0 := by
+  rw [α₁_proj, h1]
+  simp
+
+lemma α₂_proj_zero (T : MSSMACC.Sols) (h1 : α₃ (proj T.1.1) = 0) :
+    α₂ (proj T.1.1) = 0 := by
+  rw [α₂_proj, h1]
+  simp
+
+end proj
+
+
+end MSSMACC
--- a/HepLean/AnomalyCancellation/MSSMNu/SolsParameterization.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/SolsParameterization.lean
@ -0,0 +1,639 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.AnomalyCancellation.MSSMNu.Basic
+import HepLean.AnomalyCancellation.MSSMNu.LineY3B3
+import HepLean.AnomalyCancellation.MSSMNu.PlaneY3B3Orthog
+import Mathlib.Tactic.Polyrith
+/-!
+# Parameterization of solutions to the MSSM anomaly cancellation equations
+
+This file uses planes through $Y_3$ and $B_3$ to form solutions to the anomaly cancellation
+conditions.
+
+Split into four cases:
+- The generic case.
+- `case₁`: The case when the quadratic and cubic lines agree (if they exist uniquely).
+- `case₂`: The case where the plane lies entirely within the quadratic.
+- `case₃`: The case where the plane lies entirely within the cubic and quadratic.
+
+# References
+
+The main reference for the material in this file is:
+
+- https://arxiv.org/pdf/2107.07926.pdf
+
+-/
+
+universe v u
+
+namespace MSSMACC
+open MSSMCharges
+open MSSMACCs
+open BigOperators
+
+/-- Given a `R ∈ LinSols` perpendicular to $Y_3$, and $B_3$, a solution to the quadratic. -/
+def genericQuad (R : MSSMACC.AnomalyFreePerp) : MSSMACC.QuadSols :=
+  lineQuad R
+    (3 * cubeTriLin (R.val, R.val, Y₃.val))
+    (3 * cubeTriLin (R.val, R.val, B₃.val))
+    (cubeTriLin (R.val, R.val, R.val))
+
+lemma genericQuad_cube (R : MSSMACC.AnomalyFreePerp) :
+    accCube (genericQuad R).val = 0 := by
+  rw [genericQuad]
+  rw [lineQuad_val]
+  rw [planeY₃B₃_cubic]
+  ring
+
+/-- Given a `R ∈ LinSols` perpendicular to $Y_3$, and $B_3$, a element of `Sols`. -/
+def generic (R : MSSMACC.AnomalyFreePerp) : MSSMACC.Sols :=
+  AnomalyFreeMk'' (genericQuad R) (genericQuad_cube R)
+
+lemma generic_eq_planeY₃B₃_on_α (R : MSSMACC.AnomalyFreePerp) :
+    (generic R).1.1 = planeY₃B₃ R (α₁ R) (α₂ R) (α₃ R) := by
+  change (planeY₃B₃ _ _ _ _) = _
+  apply planeY₃B₃_eq
+  rw [α₁, α₂, α₃]
+  ring_nf
+  simp
+
+/-- Case₁ is when the quadratic and cubic lines in the plane agree, which occurs when
+  `α₁ R = 0`, `α₂ R = 0` and `α₃ R = 0` (if they exist uniquely).  -/
+def case₁prop (R : MSSMACC.AnomalyFreePerp) : Prop :=
+    α₁ R = 0 ∧ α₂ R = 0 ∧ α₃ R = 0
+
+/-- Case₂ is defined when the plane lies entirely within the quadratic. -/
+def case₂prop (R : MSSMACC.AnomalyFreePerp) : Prop :=
+    quadBiLin (R.val, R.val) = 0 ∧ quadBiLin (Y₃.val, R.val) = 0 ∧ quadBiLin (B₃.val, R.val) = 0
+
+/-- Case₃ is defined when the plane lies entirely within the quadratic and cubic. -/
+def case₃prop (R : MSSMACC.AnomalyFreePerp) : Prop :=
+    quadBiLin (R.val, R.val) = 0 ∧ quadBiLin (Y₃.val, R.val) = 0 ∧ quadBiLin (B₃.val, R.val) = 0 ∧
+    cubeTriLin (R.val, R.val, R.val) = 0 ∧ cubeTriLin (R.val, R.val, B₃.val) = 0 ∧
+    cubeTriLin (R.val, R.val, Y₃.val) = 0
+
+instance (R : MSSMACC.AnomalyFreePerp) : Decidable (case₁prop R) := by
+  apply And.decidable
+
+instance (R : MSSMACC.AnomalyFreePerp) : Decidable (case₂prop R) := by
+  apply And.decidable
+
+instance (R : MSSMACC.AnomalyFreePerp) : Decidable (case₃prop R) := by
+  apply And.decidable
+
+section proj
+
+/-- On elements of `Sols`, `generic (proj _)` is equivalent to multiplying
+by `genericProjCoeff`.  -/
+def genericProjCoeff (T : MSSMACC.Sols) : ℚ :=
+    dot (Y₃.val, B₃.val) * α₃ (proj T.1.1)
+
+lemma generic_proj (T : MSSMACC.Sols) :
+    generic (proj T.1.1) = (genericProjCoeff T) • T := by
+  apply ACCSystem.Sols.ext
+  erw [generic_eq_planeY₃B₃_on_α]
+  rw [planeY₃B₃_val]
+  rw [Y₃_plus_B₃_plus_proj]
+  rw [α₁_proj, α₂_proj]
+  simp
+  rfl
+
+lemma genericProjCoeff_ne_zero (T : MSSMACC.Sols) (hT : genericProjCoeff T ≠ 0 ) :
+    (genericProjCoeff T)⁻¹ • generic (proj T.1.1) = T := by
+  rw [generic_proj, ← MulAction.mul_smul, mul_comm, mul_inv_cancel hT]
+  simp
+
+lemma genericProjCoeff_zero_α₃ (T : MSSMACC.Sols) (hT : genericProjCoeff T = 0) :
+    α₃ (proj T.1.1) = 0 := by
+  rw [genericProjCoeff, mul_eq_zero] at hT
+  rw [show dot (Y₃.val, B₃.val) = 108 by rfl] at hT
+  simp at hT
+  exact hT
+
+lemma genericProjCoeff_zero_α₂ (T : MSSMACC.Sols) (hT : genericProjCoeff T = 0) :
+    α₂ (proj T.1.1) = 0 := by
+  rw [α₂_proj, genericProjCoeff_zero_α₃ T hT]
+  simp
+
+lemma genericProjCoeff_zero_α₁ (T : MSSMACC.Sols) (hT : genericProjCoeff T = 0) :
+    α₁ (proj T.1.1) = 0 := by
+  rw [α₁_proj, genericProjCoeff_zero_α₃ T hT]
+  simp
+
+lemma genericProjCoeff_zero (T : MSSMACC.Sols) :
+    genericProjCoeff T = 0 ↔ case₁prop (proj T.1.1) := by
+  apply Iff.intro
+  intro hT
+  rw [case₁prop]
+  rw [genericProjCoeff_zero_α₁ T hT, genericProjCoeff_zero_α₂ T hT, genericProjCoeff_zero_α₃ T hT]
+  simp only [and_self]
+  intro h
+  rw [case₁prop] at h
+  rw [genericProjCoeff]
+  rw [h.2.2]
+  simp
+
+lemma genericProjCoeff_neq_zero_case₁ (T : MSSMACC.Sols) (hT : genericProjCoeff T ≠ 0) :
+    ¬ case₁prop (proj T.1.1) :=
+  (genericProjCoeff_zero T).mpr.mt hT
+
+lemma genericProjCoeff_neq_zero_case₂ (T : MSSMACC.Sols) (hT : genericProjCoeff T ≠ 0) :
+    ¬ case₂prop (proj T.1.1) := by
+  by_contra hn
+  rw [case₂prop] at hn
+  rw [genericProjCoeff, α₃] at hT
+  simp_all
+
+lemma genericProjCoeff_neq_zero_case₃ (T : MSSMACC.Sols) (hT : genericProjCoeff T ≠ 0) :
+    ¬ case₃prop (proj T.1.1) := by
+  by_contra hn
+  rw [case₃prop] at hn
+  rw [genericProjCoeff, α₃] at hT
+  simp_all
+
+end proj
+
+/-- The case when the quadratic and cubic lines agree (if they exist uniquely). -/
+def case₁ (R : MSSMACC.AnomalyFreePerp) (c₁ c₂ c₃ : ℚ)
+    (h : case₁prop R) : MSSMACC.Sols :=
+  AnomalyFreeMk'' (lineQuad R c₁ c₂ c₃)
+    (by
+      rw [lineQuad_cube]
+      rw [h.1, h.2.1, h.2.2]
+      simp)
+
+lemma case₁_smul (R : MSSMACC.AnomalyFreePerp) (c₁ c₂ c₃ d : ℚ)
+    (h : case₁prop R) : case₁ R (d * c₁) (d * c₂) (d * c₃) h = d • case₁ R c₁ c₂ c₃ h := by
+  apply ACCSystem.Sols.ext
+  change (lineQuad _ _ _ _).val = _
+  rw [lineQuad_smul]
+  rfl
+
+section proj
+
+/-- The coefficent which multiplies a solution on passing through `case₁`. -/
+def case₁ProjCoeff (T : MSSMACC.Sols) : ℚ :=
+    2 * (quadBiLin (Y₃.val, (proj T.1.1).val) ^ 2  +
+    quadBiLin (B₃.val, (proj T.1.1).val) ^ 2)
+
+/-- The first parameter in case₁ needed to form an inverse on Proj. -/
+def case₁ProjC₁ (T : MSSMACC.Sols) : ℚ := (quadBiLin (B₃.val, T.val))
+
+/-- The second parameter in case₁ needed to form an inverse on Proj. -/
+def case₁ProjC₂ (T : MSSMACC.Sols) : ℚ := (- quadBiLin (Y₃.val, T.val))
+
+/-- The third parameter in case₁ needed to form an inverse on Proj. -/
+def case₁ProjC₃ (T : MSSMACC.Sols) : ℚ :=
+  - quadBiLin (B₃.val, T.val) * ( dot (Y₃.val, T.val)- dot (B₃.val, T.val) )
+  - quadBiLin (Y₃.val, T.val) * ( dot (Y₃.val, T.val) - 2 * dot (B₃.val, T.val) )
+
+lemma case₁_proj (T : MSSMACC.Sols) (h1 : genericProjCoeff T = 0) :
+    case₁ (proj T.1.1)
+       (case₁ProjC₁ T)
+       (case₁ProjC₂ T)
+       (case₁ProjC₃ T)
+       ((genericProjCoeff_zero T).mp h1)
+       = (case₁ProjCoeff T) • T := by
+  apply ACCSystem.Sols.ext
+  change (lineQuad _ _ _ _).val = _
+  rw [lineQuad_val]
+  rw [planeY₃B₃_val]
+  rw [Y₃_plus_B₃_plus_proj]
+  rw [case₁ProjCoeff, case₁ProjC₁, case₁ProjC₂, case₁ProjC₃, quad_proj, quad_Y₃_proj, quad_B₃_proj]
+  ring_nf
+  simp
+  rfl
+
+lemma case₁ProjCoeff_ne_zero (T : MSSMACC.Sols) (h1 : genericProjCoeff T = 0)
+    (hT : case₁ProjCoeff T ≠ 0 ) :
+    (case₁ProjCoeff T)⁻¹ • case₁ (proj T.1.1)
+       (case₁ProjC₁ T)
+       (case₁ProjC₂ T)
+       (case₁ProjC₃ T)
+       ((genericProjCoeff_zero T).mp h1) = T := by
+  rw [case₁_proj T h1, ← MulAction.mul_smul, mul_comm, mul_inv_cancel hT]
+  simp
+
+lemma case₁ProjCoeff_zero_Y₃_B₃ (T : MSSMACC.Sols) (h1 : case₁ProjCoeff T = 0) :
+    quadBiLin (Y₃.val, (proj T.1.1).val) = 0 ∧
+    quadBiLin (B₃.val, (proj T.1.1).val) = 0 := by
+  rw [case₁ProjCoeff, mul_eq_zero] at h1
+  simp only [OfNat.ofNat_ne_zero,  Fin.isValue, Fin.reduceFinMk, false_or] at h1
+  have h : quadBiLin (Y₃.val, (proj T.1.1).val) ^ 2 = 0 ∧
+     quadBiLin (B₃.val, (proj T.1.1).val) ^ 2  = 0 :=
+    (add_eq_zero_iff' (sq_nonneg _) (sq_nonneg _)).mp h1
+  simp only [ Fin.isValue, Fin.reduceFinMk, ne_eq, OfNat.ofNat_ne_zero,
+    not_false_eq_true, pow_eq_zero_iff] at h
+  exact h
+
+lemma case₁ProjCoeff_zero_Y₃ (T : MSSMACC.Sols) (h1 : case₁ProjCoeff T = 0) :
+    quadBiLin (Y₃.val, (proj T.1.1).val) = 0 :=
+  (case₁ProjCoeff_zero_Y₃_B₃ T h1).left
+
+lemma case₁ProjCoeff_zero_B₃ (T : MSSMACC.Sols) (h1 : case₁ProjCoeff T = 0) :
+    quadBiLin (B₃.val, (proj T.1.1).val) = 0 :=
+  (case₁ProjCoeff_zero_Y₃_B₃ T h1).right
+
+lemma case₁ProjCoeff_zero_T (T : MSSMACC.Sols) (h1 : case₁ProjCoeff T = 0) :
+    quadBiLin (T.val, (proj T.1.1).val) = 0 := by
+  have hY3 : quadBiLin (T.val, Y₃.val) = 0 := by
+    have h11 := case₁ProjCoeff_zero_Y₃ T h1
+    rw [quad_Y₃_proj] at h11
+    rw [show dot (Y₃.val, B₃.val) = 108 by rfl] at h11
+    simp only [ Fin.isValue, Fin.reduceFinMk, mul_eq_zero, OfNat.ofNat_ne_zero,
+      false_or] at h11
+    erw [quadBiLin.swap] at h11
+    exact h11
+  have hB3 : quadBiLin (T.val, B₃.val) = 0 := by
+    have h11 := case₁ProjCoeff_zero_B₃ T h1
+    rw [quad_B₃_proj] at h11
+    rw [show dot (Y₃.val, B₃.val) = 108 by rfl] at h11
+    simp only [ Fin.isValue, Fin.reduceFinMk, mul_eq_zero, OfNat.ofNat_ne_zero,
+      false_or] at h11
+    erw [quadBiLin.swap] at h11
+    exact h11
+  rw [proj_val]
+  rw [quadBiLin.map_add₂, quadBiLin.map_add₂]
+  rw [quadBiLin.map_smul₂, quadBiLin.map_smul₂, quadBiLin.map_smul₂]
+  rw [hY3, hB3]
+  erw [quadSol T.1]
+  simp
+
+lemma case₁ProjCoeff_zero_self (T : MSSMACC.Sols) (h1 : case₁ProjCoeff T = 0)  :
+    quadBiLin ((proj T.1.1).val, (proj T.1.1).val) = 0 := by
+  nth_rewrite 1 [proj_val]
+  rw [quadBiLin.map_add₁, quadBiLin.map_add₁]
+  rw [quadBiLin.map_smul₁, quadBiLin.map_smul₁, quadBiLin.map_smul₁]
+  rw [case₁ProjCoeff_zero_Y₃ T h1, case₁ProjCoeff_zero_B₃ T h1, case₁ProjCoeff_zero_T T h1]
+  simp
+
+lemma case₁ProjCoeff_zero (T : MSSMACC.Sols) :
+    case₁ProjCoeff T = 0 ↔ case₂prop (proj T.1.1) := by
+  apply Iff.intro
+  intro h1
+  rw [case₂prop]
+  rw [case₁ProjCoeff_zero_self T h1, case₁ProjCoeff_zero_Y₃ T h1, case₁ProjCoeff_zero_B₃ T h1]
+  simp only [and_self]
+  intro h
+  rw [case₂prop] at h
+  rw [case₁ProjCoeff]
+  rw [h.2.1, h.2.2]
+  simp
+
+lemma case₁ProjCoeff_ne_zero_case₂ (T : MSSMACC.Sols) (h1 : case₁ProjCoeff T ≠ 0) :
+    ¬ case₂prop (proj T.1.1) :=
+  (case₁ProjCoeff_zero T).mpr.mt h1
+
+lemma case₁ProjCoeff_ne_zero_case₃ (T : MSSMACC.Sols) (h1 : case₁ProjCoeff T ≠ 0) :
+    ¬ case₃prop (proj T.1.1) := by
+  by_contra hn
+  rw [case₃prop] at hn
+  rw [case₁ProjCoeff] at h1
+  simp_all
+
+
+end proj
+
+/-- The case where the plane lies entirely within the quadratic. -/
+def case₂ (R : MSSMACC.AnomalyFreePerp) (a₁ a₂ a₃ : ℚ)
+    (h : case₂prop R) : MSSMACC.Sols :=
+  AnomalyFreeMk' (lineCube R a₁ a₂ a₃)
+    (by
+      erw [planeY₃B₃_quad]
+      rw [h.1, h.2.1, h.2.2]
+      simp)
+    (lineCube_cube R a₁ a₂ a₃)
+
+lemma case₂_smul (R : MSSMACC.AnomalyFreePerp) (c₁ c₂ c₃ d : ℚ)
+    (h : case₂prop R) : case₂ R (d * c₁) (d * c₂) (d * c₃) h = d • case₂ R c₁ c₂ c₃ h := by
+  apply ACCSystem.Sols.ext
+  change (lineCube _ _ _ _).val = _
+  rw [lineCube_smul]
+  rfl
+
+section proj
+
+/-- The coefficent which multiplies a solution on passing through `case₂`. -/
+def case₂ProjCoeff (T : MSSMACC.Sols) : ℚ :=
+    3 * dot (Y₃.val, B₃.val) ^ 3 * (cubeTriLin (T.val, T.val, Y₃.val) ^ 2  +
+    cubeTriLin (T.val, T.val, B₃.val) ^ 2 )
+
+/-- The first parameter in `case₂` needed to form an inverse on `Proj`. -/
+def case₂ProjC₁ (T : MSSMACC.Sols) : ℚ := cubeTriLin (T.val, T.val, B₃.val)
+
+/-- The second parameter in `case₂` needed to form an inverse on `Proj`. -/
+def case₂ProjC₂ (T : MSSMACC.Sols) : ℚ := - cubeTriLin (T.val, T.val, Y₃.val)
+
+/-- The third parameter in `case₂` needed to form an inverse on `Proj`. -/
+def case₂ProjC₃ (T : MSSMACC.Sols) : ℚ :=
+  (- cubeTriLin (T.val, T.val, B₃.val) * (dot (Y₃.val, T.val) - dot (B₃.val, T.val))
+  - cubeTriLin (T.val, T.val, Y₃.val) * (dot (Y₃.val, T.val) - 2 * dot (B₃.val, T.val)))
+
+lemma case₂_proj (T : MSSMACC.Sols) (h1 : case₁ProjCoeff T = 0) :
+    case₂ (proj T.1.1)
+       (case₂ProjC₁ T)
+       (case₂ProjC₂ T)
+       (case₂ProjC₃ T)
+       ((case₁ProjCoeff_zero T).mp h1)  = (case₂ProjCoeff T) • T := by
+  apply ACCSystem.Sols.ext
+  change (planeY₃B₃ _ _ _ _).val = _
+  rw [planeY₃B₃_val]
+  rw [Y₃_plus_B₃_plus_proj]
+  rw [case₂ProjCoeff, case₂ProjC₁, case₂ProjC₂, case₂ProjC₃, cube_proj, cube_proj_proj_B₃,
+    cube_proj_proj_Y₃]
+  ring_nf
+  simp
+  rfl
+
+lemma case₂ProjCoeff_ne_zero (T : MSSMACC.Sols) (h1 : case₁ProjCoeff T = 0)
+    (hT : case₂ProjCoeff T ≠ 0 ) :
+    (case₂ProjCoeff T)⁻¹ • case₂ (proj T.1.1)
+      (case₂ProjC₁ T)
+      (case₂ProjC₂ T)
+      (case₂ProjC₃ T)
+      ((case₁ProjCoeff_zero T).mp h1) = T := by
+  rw [case₂_proj T h1, ← MulAction.mul_smul, mul_comm, mul_inv_cancel hT]
+  simp
+
+lemma case₂ProjCoeff_zero_Y₃_B₃ (T : MSSMACC.Sols) (h1 : case₂ProjCoeff T = 0) :
+    cubeTriLin ((proj T.1.1).val, (proj T.1.1).val, Y₃.val) = 0 ∧
+    cubeTriLin ((proj T.1.1).val, (proj T.1.1).val, B₃.val) = 0 := by
+  rw [case₂ProjCoeff, mul_eq_zero] at h1
+  rw [show dot (Y₃.val, B₃.val) = 108 by rfl] at h1
+  simp at h1
+  have h : cubeTriLin (T.val, T.val, Y₃.val) ^ 2 = 0 ∧
+         cubeTriLin (T.val, T.val, B₃.val) ^ 2  = 0 :=
+    (add_eq_zero_iff' (sq_nonneg _) (sq_nonneg _)).mp h1
+  simp at h
+  have h1 := cube_proj_proj_B₃ T.1.1
+  erw [h.2] at h1
+  have h2 := cube_proj_proj_Y₃ T.1.1
+  erw [h.1] at h2
+  simp_all
+
+
+lemma case₂ProjCoeff_zero_Y₃ (T : MSSMACC.Sols) (h1 : case₂ProjCoeff T = 0) :
+    cubeTriLin ((proj T.1.1).val, (proj T.1.1).val, Y₃.val)  = 0 :=
+  (case₂ProjCoeff_zero_Y₃_B₃ T h1).left
+
+lemma case₂ProjCoeff_zero_B₃ (T : MSSMACC.Sols) (h1 : case₂ProjCoeff T = 0) :
+    cubeTriLin ((proj T.1.1).val, (proj T.1.1).val, B₃.val) = 0 :=
+  (case₂ProjCoeff_zero_Y₃_B₃ T h1).right
+
+
+lemma case₂ProjCoeff_zero_T (T : MSSMACC.Sols) (h1 : case₂ProjCoeff T = 0) :
+    cubeTriLin ((proj T.1.1).val, (proj T.1.1).val, T.val) = 0 := by
+  rw [cube_proj_proj_self]
+  have hr : cubeTriLin (T.val, T.val, Y₃.val) = 0 := by
+    have h11 := case₂ProjCoeff_zero_Y₃ T h1
+    rw [cube_proj_proj_Y₃] at h11
+    rw [show dot (Y₃.val, B₃.val) = 108 by rfl] at h11
+    simp at h11
+    exact h11
+  have h2 : cubeTriLin (T.val, T.val, B₃.val) = 0 := by
+    have h11 := case₂ProjCoeff_zero_B₃ T h1
+    rw [cube_proj_proj_B₃] at h11
+    rw [show dot (Y₃.val, B₃.val) = 108 by rfl] at h11
+    simp at h11
+    exact h11
+  rw [hr, h2]
+  simp
+
+lemma case₂ProjCoeff_zero_self (T : MSSMACC.Sols) (h1 : case₂ProjCoeff T = 0)  :
+    cubeTriLin ((proj T.1.1).val, (proj T.1.1).val, (proj T.1.1).val) = 0 := by
+  nth_rewrite 3 [proj_val]
+  rw [cubeTriLin.map_add₃, cubeTriLin.map_add₃]
+  rw [cubeTriLin.map_smul₃, cubeTriLin.map_smul₃, cubeTriLin.map_smul₃]
+  rw [case₂ProjCoeff_zero_Y₃ T h1, case₂ProjCoeff_zero_B₃ T h1, case₂ProjCoeff_zero_T T h1]
+  simp
+
+
+lemma case₂ProjCoeff_zero (T : MSSMACC.Sols) :
+    (case₁ProjCoeff T = 0 ∧ case₂ProjCoeff T = 0) ↔ case₃prop (proj T.1.1) := by
+  apply Iff.intro
+  intro h1
+  rw [case₃prop]
+  rw [case₂ProjCoeff_zero_self T h1.2, case₂ProjCoeff_zero_Y₃ T h1.2, case₂ProjCoeff_zero_B₃ T h1.2]
+  rw [case₁ProjCoeff_zero_self T h1.1, case₁ProjCoeff_zero_Y₃ T h1.1, case₁ProjCoeff_zero_B₃ T h1.1]
+  simp only [and_self]
+  intro h
+  rw [case₃prop] at h
+  rw [case₁ProjCoeff, case₂ProjCoeff]
+  simp_all only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, add_zero,
+    mul_zero,  mul_eq_zero, pow_eq_zero_iff, false_or, true_and]
+  erw [show dot (Y₃.val, B₃.val) = 108 by rfl]
+  simp only [OfNat.ofNat_ne_zero, false_or]
+  have h1' := cube_proj_proj_B₃ T.1.1
+  have h2' := cube_proj_proj_Y₃ T.1.1
+  erw [show dot (Y₃.val, B₃.val) = 108 by rfl] at h1' h2'
+  simp_all
+
+lemma case₂ProjCoeff_ne_zero_case₃ (T : MSSMACC.Sols) (h1 : case₂ProjCoeff T ≠ 0) :
+    ¬ case₃prop (proj T.1.1) := by
+  have h1 : ¬ (case₁ProjCoeff T = 0 ∧ case₂ProjCoeff T = 0) := by
+    simp_all
+  exact (case₂ProjCoeff_zero T).mpr.mt h1
+
+end proj
+
+/-- The case where the plane lies entirely within the quadratic and cubic. -/
+def case₃ (R : MSSMACC.AnomalyFreePerp) (b₁ b₂ b₃ : ℚ)
+    (h₃ : case₃prop R)  :
+    MSSMACC.Sols :=
+  AnomalyFreeMk' (planeY₃B₃ R b₁ b₂ b₃)
+  (by
+    rw [planeY₃B₃_quad]
+    rw [h₃.1, h₃.2.1, h₃.2.2.1]
+    simp)
+  (by
+    rw [planeY₃B₃_cubic]
+    rw [h₃.2.2.2.1, h₃.2.2.2.2.1, h₃.2.2.2.2.2]
+    simp)
+
+lemma case₃_smul (R : MSSMACC.AnomalyFreePerp) (c₁ c₂ c₃ d : ℚ)
+    (h : case₃prop R) : case₃ R (d * c₁) (d * c₂) (d * c₃) h = d • case₃ R c₁ c₂ c₃ h := by
+  apply ACCSystem.Sols.ext
+  change (planeY₃B₃ _ _ _ _).val = _
+  rw [planeY₃B₃_smul]
+  rfl
+
+
+section proj
+
+/-- The coefficent which multiplies a solution on passing through `case₃`. -/
+def case₃ProjCoeff : ℚ :=  dot (Y₃.val, B₃.val)
+
+/-- The first parameter in `case₃` needed to form an inverse on `Proj`. -/
+def case₃ProjC₁ (T : MSSMACC.Sols) : ℚ := (dot (Y₃.val, T.val) - dot (B₃.val, T.val))
+
+/-- The second parameter in `case₃` needed to form an inverse on `Proj`. -/
+def case₃ProjC₂ (T : MSSMACC.Sols) : ℚ := (2 * dot (B₃.val, T.val) - dot (Y₃.val, T.val))
+
+lemma case₃_proj (T : MSSMACC.Sols) (h0 : case₁ProjCoeff T = 0) (h1 : case₂ProjCoeff T = 0) :
+    case₃ (proj T.1.1)
+       (case₃ProjC₁ T)
+       (case₃ProjC₂ T)
+       1
+       ((case₂ProjCoeff_zero T).mp (And.intro h0 h1))  =  case₃ProjCoeff • T := by
+  apply ACCSystem.Sols.ext
+  change (planeY₃B₃ _ _ _ _).val = _
+  rw [planeY₃B₃_val]
+  rw [Y₃_plus_B₃_plus_proj]
+  rw [case₃ProjC₁, case₃ProjC₂]
+  ring_nf
+  simp
+  rfl
+
+lemma case₃_smul_coeff (T : MSSMACC.Sols) (h0 : case₁ProjCoeff T = 0) (h1 : case₂ProjCoeff T = 0) :
+    case₃ProjCoeff⁻¹ • case₃ (proj T.1.1)
+       (case₃ProjC₁ T)
+       (case₃ProjC₂ T)
+       1
+       ((case₂ProjCoeff_zero T).mp (And.intro h0 h1)) = T := by
+  rw [case₃_proj T h0 h1]
+  rw [← MulAction.mul_smul, mul_comm, mul_inv_cancel]
+  simp only [one_smul]
+  rw [case₃ProjCoeff]
+  rw [show dot (Y₃.val, B₃.val) = 108 by rfl]
+  simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true]
+
+end proj
+
+/-- A map from `MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ ` to `MSSMACC.Sols`.
+This allows generation of solutions given elements of `MSSMACC.AnomalyFreePerp` and
+three rational numbers. -/
+def parameterization :
+    MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ  →  MSSMACC.Sols := fun A =>
+  if h₃ : case₃prop A.1 then
+    case₃ A.1 A.2.1 A.2.2.1 A.2.2.2 h₃
+  else
+    if h₂ : case₂prop A.1 then
+      case₂  A.1 A.2.1 A.2.2.1 A.2.2.2 h₂
+    else
+      if h₁ : case₁prop A.1 then
+        case₁ A.1 A.2.1 A.2.2.1 A.2.2.2 h₁
+      else
+        A.2.1 • generic A.1
+
+lemma parameterization_smul (R : MSSMACC.AnomalyFreePerp) (a b c d : ℚ) :
+    parameterization (R, d * a, d * b, d * c) = d • parameterization (R, a, b, c) := by
+  rw [parameterization, parameterization]
+  by_cases h₃ : case₃prop R
+  rw [dif_pos h₃, dif_pos h₃]
+  rw [case₃_smul]
+  rw [dif_neg h₃, dif_neg h₃]
+  by_cases h₂ : case₂prop R
+  rw [dif_pos h₂, dif_pos h₂]
+  rw [case₂_smul]
+  rw [dif_neg h₂, dif_neg h₂]
+  by_cases h₁ : case₁prop R
+  rw [dif_pos h₁, dif_pos h₁]
+  rw [case₁_smul]
+  rw [dif_neg h₁, dif_neg h₁]
+  rw [mul_smul]
+
+lemma parameterization_not₁₂₃ (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ)
+    (h1 : ¬ case₁prop R) (h2 : ¬ case₂prop R) (h3 : ¬ case₃prop R) :
+    parameterization (R, a, b, c) = a • generic R := by
+  rw [parameterization]
+  rw [dif_neg h3]
+  rw [dif_neg h2]
+  rw [dif_neg h1]
+
+lemma parameterization_is₁_not₂₃ (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ)
+    (h1 : case₁prop R) (h2 : ¬ case₂prop R) (h3 : ¬ case₃prop R) :
+    parameterization (R, a, b, c) = case₁ R a b c h1:= by
+  rw [parameterization]
+  rw [dif_neg h3]
+  rw [dif_neg h2]
+  rw [dif_pos h1]
+
+lemma parameterization_is₁₂_not₃ (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) (h2 : case₂prop R)
+    (h3 : ¬ case₃prop R) : parameterization (R, a, b, c) = case₂ R a b c h2 := by
+  rw [parameterization]
+  rw [dif_neg h3]
+  rw [dif_pos h2]
+
+lemma parameterization_is₃ (R : MSSMACC.AnomalyFreePerp) (a b c : ℚ) (h3 : case₃prop R) :
+    parameterization (R, a, b, c) = case₃ R a b c h3 := by
+  rw [parameterization]
+  rw [dif_pos h3]
+
+/-- A right inverse of `parameterizaiton`. -/
+def inverse (R : MSSMACC.Sols) : MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ :=
+  if genericProjCoeff R ≠ 0 then
+    (proj R.1.1, (genericProjCoeff R)⁻¹, 0, 0)
+  else
+    if case₁ProjCoeff R ≠ 0 then
+      (proj R.1.1, (case₁ProjCoeff R)⁻¹ * case₁ProjC₁ R, (case₁ProjCoeff R)⁻¹ * case₁ProjC₂ R,
+        (case₁ProjCoeff R)⁻¹ * case₁ProjC₃ R)
+    else
+      if case₂ProjCoeff R ≠ 0 then
+        (proj R.1.1, (case₂ProjCoeff R)⁻¹ * case₂ProjC₁ R, (case₂ProjCoeff R)⁻¹ * case₂ProjC₂ R,
+          (case₂ProjCoeff R)⁻¹ * case₂ProjC₃ R)
+      else
+        (proj R.1.1, (case₃ProjCoeff)⁻¹ * case₃ProjC₁ R, (case₃ProjCoeff)⁻¹ * case₃ProjC₂ R,
+          (case₃ProjCoeff)⁻¹ * 1)
+
+lemma inverse_generic (R : MSSMACC.Sols) (h : genericProjCoeff R ≠ 0) :
+    inverse R = (proj R.1.1, (genericProjCoeff R)⁻¹, 0, 0) := by
+  rw [inverse, if_pos h]
+
+lemma inverse_case₁ (R : MSSMACC.Sols) (h0 : genericProjCoeff R = 0)
+    (h1 : case₁ProjCoeff R ≠ 0) : inverse R = (proj R.1.1, (case₁ProjCoeff R)⁻¹ * case₁ProjC₁ R,
+    (case₁ProjCoeff R)⁻¹ * case₁ProjC₂ R, (case₁ProjCoeff R)⁻¹ * case₁ProjC₃ R) := by
+  rw [inverse]
+  simp_all
+
+lemma inverse_case₂ (R : MSSMACC.Sols) (h0 : genericProjCoeff R = 0)
+    (h1 : case₁ProjCoeff R = 0) (h2 : case₂ProjCoeff R ≠ 0) : inverse R = (proj R.1.1,
+    (case₂ProjCoeff R)⁻¹ * case₂ProjC₁ R,
+    (case₂ProjCoeff R)⁻¹ * case₂ProjC₂ R, (case₂ProjCoeff R)⁻¹ * case₂ProjC₃ R) := by
+  rw [inverse]
+  simp_all
+
+lemma inverse_case₃ (R : MSSMACC.Sols) (h0 : genericProjCoeff R = 0)
+    (h1 : case₁ProjCoeff R = 0) (h2 : case₂ProjCoeff R = 0)  :
+    inverse R =  (proj R.1.1, (case₃ProjCoeff)⁻¹ * case₃ProjC₁ R,
+    (case₃ProjCoeff)⁻¹ * case₃ProjC₂ R,
+    (case₃ProjCoeff)⁻¹ * 1) := by
+  rw [inverse]
+  simp_all
+
+lemma inverse_parameterization (R : MSSMACC.Sols) :
+    parameterization (inverse R) = R := by
+  by_cases h0 : genericProjCoeff R ≠ 0
+  rw [inverse_generic R h0]
+  rw [parameterization_not₁₂₃ _ _ _ _ (genericProjCoeff_neq_zero_case₁ R h0)
+   (genericProjCoeff_neq_zero_case₂ R h0) (genericProjCoeff_neq_zero_case₃ R h0)]
+  rw [genericProjCoeff_ne_zero R h0]
+  by_cases h1 : case₁ProjCoeff R ≠ 0
+  simp at h0
+  rw [inverse_case₁ R h0 h1]
+  rw [parameterization_smul]
+  rw [parameterization_is₁_not₂₃ _ _ _ _ ((genericProjCoeff_zero R).mp h0)
+    (case₁ProjCoeff_ne_zero_case₂ R h1) (case₁ProjCoeff_ne_zero_case₃ R h1)]
+  rw [case₁ProjCoeff_ne_zero R h0 h1]
+  simp at h0 h1
+  by_cases h2 : case₂ProjCoeff R ≠ 0
+  rw [inverse_case₂ R h0 h1 h2]
+  rw [parameterization_smul]
+  rw [parameterization_is₁₂_not₃ _ _ _ _ ((case₁ProjCoeff_zero R).mp h1)
+    (case₂ProjCoeff_ne_zero_case₃ R h2)]
+  rw [case₂ProjCoeff_ne_zero R h1 h2]
+  simp at h2
+  rw [inverse_case₃ R h0 h1 h2]
+  rw [parameterization_smul]
+  rw [parameterization_is₃ _ _ _ _ ((case₂ProjCoeff_zero R).mp (And.intro h1 h2))]
+  rw [case₃_smul_coeff R h1 h2]
+
+theorem parameterization_surjective : Function.Surjective parameterization := by
+  intro T
+  use inverse T
+  exact inverse_parameterization T
+
+
+end MSSMACC
--- a/HepLean/AnomalyCancellation/MSSMNu/Y3.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/Y3.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.MSSMNu.Basic
+/-!
+# The definition of the solution Y₃ and properties thereof
+
+We define $Y_3$ and show that it is a double point of the cubic.
+
+# References
+
+The main reference for the material in this file is:
+
+- https://arxiv.org/pdf/2107.07926.pdf
+
+-/
+
+universe v u
+
+namespace MSSMACC
+open MSSMCharges
+open MSSMACCs
+open BigOperators
+
+/-- $Y_3$ is the charge which is hypercharge in all families, but with the third
+family of the opposite sign. -/
+def Y₃AsCharge : MSSMACC.charges := toSpecies.symm
+  ⟨fun s => fun i =>
+    match s, i with
+    | 0, 0 => 1
+    | 0, 1 => 1
+    | 0, 2 => - 1
+    | 1, 0 => -4
+    | 1, 1 => -4
+    | 1, 2 => 4
+    | 2, 0 => 2
+    | 2, 1 => 2
+    | 2, 2 => - 2
+    | 3, 0 => -3
+    | 3, 1 => -3
+    | 3, 2 => 3
+    | 4, 0 => 6
+    | 4, 1 => 6
+    | 4, 2 => - 6
+    | 5, 0 => 0
+    | 5, 1 => 0
+    | 5, 2 => 0,
+  fun s =>
+    match s with
+    | 0 => -3
+    | 1 => 3⟩
+
+/-- $Y_3$ as a solution. -/
+def Y₃ : MSSMACC.Sols :=
+  MSSMACC.AnomalyFreeMk Y₃AsCharge (by rfl) (by rfl) (by rfl) (by rfl) (by rfl) (by rfl)
+
+lemma Y₃_val : Y₃.val = Y₃AsCharge := by
+  rfl
+
+lemma doublePoint_Y₃_Y₃ (R : MSSMACC.LinSols) :
+    cubeTriLin (Y₃.val, Y₃.val, R.val) = 0 := by
+  rw [← TriLinearSymm.toFun_eq_coe]
+  simp only [cubeTriLin, cubeTriLinToFun, MSSMSpecies_numberCharges]
+  rw [Fin.sum_univ_three]
+  rw [Y₃_val]
+  rw [Y₃AsCharge]
+  repeat rw [toSMSpecies_toSpecies_inv]
+  rw [Hd_toSpecies_inv, Hu_toSpecies_inv]
+  simp
+  have hLin := R.linearSol
+  simp at hLin
+  have h3 := hLin 3
+  simp [Fin.sum_univ_three] at h3
+  linear_combination 6 * h3
+
+end MSSMACC