From ec47df149381259da31e5ca83edc30a8ca370479 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Thu, 18 Apr 2024 09:26:45 -0400
Subject: [PATCH] feat: Add theorems related to Sols

---
 HepLean.lean                                  |   4 +
 .../SMNu/PlusU1/BMinusL.lean                  | 117 ++++++++++++++
 .../SMNu/PlusU1/HyperCharge.lean              | 146 +++++++++++++++++
 .../SMNu/PlusU1/QuadSol.lean                  | 146 +++++++++++++++++
 .../SMNu/PlusU1/QuadSolToSol.lean             | 147 ++++++++++++++++++
 5 files changed, 560 insertions(+)
 create mode 100644 HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean
 create mode 100644 HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean
 create mode 100644 HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSol.lean
 create mode 100644 HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean

diff --git a/HepLean.lean b/HepLean.lean
index f1f78df..eaa29e3 100644
--- a/HepLean.lean
+++ b/HepLean.lean
@@ -23,4 +23,8 @@ import HepLean.AnomalyCancellation.SMNu.Ordinary.Basic
 import HepLean.AnomalyCancellation.SMNu.Ordinary.FamilyMaps
 import HepLean.AnomalyCancellation.SMNu.Permutations
 import HepLean.AnomalyCancellation.SMNu.PlusU1.Basic
+import HepLean.AnomalyCancellation.SMNu.PlusU1.BMinusL
 import HepLean.AnomalyCancellation.SMNu.PlusU1.FamilyMaps
+import HepLean.AnomalyCancellation.SMNu.PlusU1.HyperCharge
+import HepLean.AnomalyCancellation.SMNu.PlusU1.QuadSol
+import HepLean.AnomalyCancellation.SMNu.PlusU1.QuadSolToSol
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean
new file mode 100644
index 0000000..13f9daa
--- /dev/null
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean
@@ -0,0 +1,117 @@
+/-
+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
+/-!
+# B Minus L in SM with RHN.
+
+Relavent definitions for the SM `B-L`.
+
+-/
+universe v u
+
+namespace SMRHN
+namespace PlusU1
+
+open SMνCharges
+open SMνACCs
+open BigOperators
+
+variable {n : ℕ}
+
+/-- $B - L$ in the 1-family case. -/
+@[simps!]
+def BL₁ : (PlusU1 1).Sols where
+  val := fun i =>
+    match i with
+    | (0 : Fin 6) => 1
+    | (1 : Fin 6) => -1
+    | (2 : Fin 6) => -1
+    | (3 : Fin 6) => -3
+    | (4 : Fin 6) => 3
+    | (5 : Fin 6) => 3
+  linearSol := by
+    intro i
+    simp at i
+    match i with
+    | 0 => rfl
+    | 1 => rfl
+    | 2 => rfl
+    | 3 => rfl
+  quadSol := by
+    intro i
+    simp at i
+    match i with
+    | 0 => rfl
+  cubicSol := by rfl
+
+/-- $B - L$ in the $n$-family case. -/
+@[simps!]
+def BL (n : ℕ) : (PlusU1 n).Sols :=
+  familyUniversalAF n BL₁
+
+namespace BL
+
+variable {n : ℕ}
+
+lemma on_quadBiLin (S : (PlusU1 n).charges) :
+    quadBiLin ((BL n).val, S) = 1/2 * accYY S + 3/2 * accSU2 S - 2 * accSU3 S := by
+  erw [familyUniversal_quadBiLin]
+  rw [accYY_decomp, accSU2_decomp, accSU3_decomp]
+  simp
+  ring
+
+lemma on_quadBiLin_AFL (S : (PlusU1 n).LinSols) : quadBiLin ((BL n).val, S.val) = 0 := by
+  rw [on_quadBiLin]
+  rw [YYsol S, SU2Sol S, SU3Sol S]
+  simp
+
+lemma add_AFL_quad (S : (PlusU1 n).LinSols) (a b : ℚ) :
+    accQuad (a • S.val + b • (BL n).val) = a ^ 2 * accQuad S.val := by
+  erw [BiLinearSymm.toHomogeneousQuad_add, quadSol (b • (BL n)).1]
+  rw [quadBiLin.map_smul₁, quadBiLin.map_smul₂, quadBiLin.swap, on_quadBiLin_AFL]
+  erw [accQuad.map_smul]
+  simp
+
+lemma add_quad (S : (PlusU1 n).QuadSols) (a b : ℚ) :
+    accQuad (a • S.val + b • (BL n).val) = 0 := by
+  rw [add_AFL_quad, quadSol S]
+  simp
+
+/-- The `QuadSol` obtained by adding $B-L$ to a `QuadSol`. -/
+def addQuad (S : (PlusU1 n).QuadSols) (a b : ℚ) : (PlusU1 n).QuadSols :=
+  linearToQuad (a • S.1 + b • (BL n).1.1) (add_quad S a b)
+
+lemma addQuad_zero (S : (PlusU1 n).QuadSols) (a : ℚ): addQuad S a 0 = a • S := by
+  simp [addQuad, linearToQuad]
+  rfl
+
+lemma on_cubeTriLin (S : (PlusU1 n).charges) :
+    cubeTriLin ((BL n).val, (BL n).val, S) = 9 * accGrav S - 24 * accSU3 S := by
+  erw [familyUniversal_cubeTriLin']
+  rw [accGrav_decomp, accSU3_decomp]
+  simp
+  ring
+
+lemma on_cubeTriLin_AFL (S : (PlusU1 n).LinSols) :
+    cubeTriLin ((BL n).val, (BL n).val, S.val) = 0 := by
+  rw [on_cubeTriLin]
+  rw [gravSol S, SU3Sol S]
+  simp
+
+lemma add_AFL_cube (S : (PlusU1 n).LinSols) (a b : ℚ) :
+    accCube (a • S.val + b • (BL n).val) =
+    a ^ 2 * (a * accCube S.val + 3 * b * cubeTriLin (S.val, S.val, (BL n).val)) := by
+  erw [TriLinearSymm.toCubic_add, cubeSol (b • (BL n)), accCube.map_smul]
+  repeat rw [cubeTriLin.map_smul₁, cubeTriLin.map_smul₂, cubeTriLin.map_smul₃]
+  rw [on_cubeTriLin_AFL]
+  simp
+  ring
+
+
+end BL
+end PlusU1
+end SMRHN
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean
new file mode 100644
index 0000000..91e6454
--- /dev/null
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/HyperCharge.lean
@@ -0,0 +1,146 @@
+/-
+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
+/-!
+# Hypercharge in SM with RHN.
+
+Relavent definitions for the SM hypercharge.
+
+-/
+universe v u
+
+namespace SMRHN
+namespace PlusU1
+
+open SMνCharges
+open SMνACCs
+open BigOperators
+
+/-- The hypercharge for 1 family. -/
+@[simps!]
+def Y₁ : (PlusU1 1).Sols where
+  val := fun i =>
+    match i with
+    | (0 : Fin 6) => 1
+    | (1 : Fin 6)  => -4
+    | (2 : Fin 6)  => 2
+    | (3 : Fin 6)  => -3
+    | (4 : Fin 6)  => 6
+    | (5 : Fin 6)  => 0
+  linearSol := by
+    intro i
+    simp at i
+    match i with
+    | 0 => rfl
+    | 1 => rfl
+    | 2 => rfl
+    | 3 => rfl
+  quadSol := by
+    intro i
+    simp at i
+    match i with
+    | 0 => rfl
+  cubicSol := by rfl
+
+/-- The hypercharge for `n` family. -/
+@[simps!]
+def Y (n : ℕ) : (PlusU1 n).Sols :=
+  familyUniversalAF n Y₁
+
+namespace Y
+
+variable {n : ℕ}
+
+lemma on_quadBiLin (S : (PlusU1 n).charges) :
+    quadBiLin ((Y n).val, S) = accYY S := by
+  erw [familyUniversal_quadBiLin]
+  rw [accYY_decomp]
+  simp
+  ring_nf
+  simp
+
+lemma on_quadBiLin_AFL (S : (PlusU1 n).LinSols) : quadBiLin ((Y n).val, S.val) = 0 := by
+  rw [on_quadBiLin]
+  rw [YYsol S]
+
+
+lemma add_AFL_quad (S : (PlusU1 n).LinSols) (a b : ℚ) :
+    accQuad (a • S.val + b • (Y n).val) = a ^ 2 * accQuad S.val := by
+  erw [BiLinearSymm.toHomogeneousQuad_add, quadSol (b • (Y n)).1]
+  rw [quadBiLin.map_smul₁, quadBiLin.map_smul₂, quadBiLin.swap, on_quadBiLin_AFL]
+  erw [accQuad.map_smul]
+  simp
+
+lemma add_quad (S : (PlusU1 n).QuadSols) (a b : ℚ) :
+    accQuad (a • S.val + b • (Y n).val) = 0 := by
+  rw [add_AFL_quad, quadSol S]
+  simp
+
+/-- The `QuadSol` obtained by adding hypercharge to a `QuadSol`. -/
+def addQuad (S : (PlusU1 n).QuadSols) (a b : ℚ) : (PlusU1 n).QuadSols :=
+  linearToQuad (a • S.1 + b • (Y n).1.1) (add_quad S a b)
+
+lemma addQuad_zero (S : (PlusU1 n).QuadSols) (a : ℚ): addQuad S a 0 = a • S := by
+  simp [addQuad, linearToQuad]
+  rfl
+
+lemma on_cubeTriLin (S : (PlusU1 n).charges) :
+    cubeTriLin ((Y n).val, (Y n).val, S) =  6 * accYY S := by
+  erw [familyUniversal_cubeTriLin']
+  rw [accYY_decomp]
+  simp
+  ring
+
+lemma on_cubeTriLin_AFL (S : (PlusU1 n).LinSols) :
+    cubeTriLin ((Y n).val, (Y n).val, S.val) = 0 := by
+  rw [on_cubeTriLin]
+  rw [YYsol S]
+  simp
+
+lemma on_cubeTriLin' (S : (PlusU1 n).charges) :
+    cubeTriLin ((Y n).val, S, S) =  6 * accQuad S := by
+  erw [familyUniversal_cubeTriLin]
+  rw [accQuad_decomp]
+  simp
+  ring_nf
+
+lemma on_cubeTriLin'_ALQ (S : (PlusU1 n).QuadSols) :
+    cubeTriLin ((Y n).val, S.val, S.val) = 0 := by
+  rw [on_cubeTriLin']
+  rw [quadSol S]
+  simp
+
+lemma add_AFL_cube (S : (PlusU1 n).LinSols) (a b : ℚ) :
+    accCube (a • S.val + b • (Y n).val) =
+    a ^ 2 * (a * accCube S.val + 3 * b * cubeTriLin (S.val, S.val, (Y n).val)) := by
+  erw [TriLinearSymm.toCubic_add, cubeSol (b • (Y n)), accCube.map_smul]
+  repeat rw [cubeTriLin.map_smul₁, cubeTriLin.map_smul₂, cubeTriLin.map_smul₃]
+  rw [on_cubeTriLin_AFL]
+  simp
+  ring
+
+lemma add_AFQ_cube (S : (PlusU1 n).QuadSols) (a b : ℚ) :
+    accCube (a • S.val + b • (Y n).val) = a ^ 3 *  accCube S.val := by
+  rw [add_AFL_cube]
+  rw [cubeTriLin.swap₃]
+  rw [on_cubeTriLin'_ALQ]
+  ring
+
+lemma add_AF_cube (S : (PlusU1 n).Sols) (a b : ℚ) :
+    accCube (a • S.val + b • (Y n).val) = 0 := by
+  rw [add_AFQ_cube]
+  rw [cubeSol S]
+  simp
+
+/-- The `Sol` obtained by adding hypercharge to a `Sol`. -/
+def addCube (S : (PlusU1 n).Sols) (a b : ℚ) : (PlusU1 n).Sols :=
+  quadToAF (addQuad S.1 a b) (add_AF_cube S a b)
+
+
+end Y
+end PlusU1
+end SMRHN
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSol.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSol.lean
new file mode 100644
index 0000000..36c528d
--- /dev/null
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSol.lean
@@ -0,0 +1,146 @@
+/-
+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
+/-!
+# Properties of Quad Sols for SM with RHN
+
+We give a series of properties held by solutions to the quadratic equation.
+
+In particular given a quad solution we define a map from linear solutions to quadratic solutions
+and show that it is a surjection. The main reference for this is:
+
+- https://arxiv.org/abs/2006.03588
+
+-/
+
+universe v u
+
+namespace SMRHN
+namespace PlusU1
+
+open SMνCharges
+open SMνACCs
+open BigOperators
+
+namespace QuadSol
+
+variable {n : ℕ}
+variable (C : (PlusU1 n).QuadSols)
+
+lemma add_AFL_quad (S : (PlusU1 n).LinSols) (a b : ℚ) :
+    accQuad (a • S.val + b • C.val) =
+    a * (a * accQuad S.val + 2 * b * quadBiLin (S.val, C.val)) := by
+  erw [BiLinearSymm.toHomogeneousQuad_add, quadSol (b • C)]
+  rw [quadBiLin.map_smul₁, quadBiLin.map_smul₂]
+  erw [accQuad.map_smul]
+  ring
+
+/-- A helper function for what comes later. -/
+def α₁ (S : (PlusU1 n).LinSols) : ℚ := - 2 * quadBiLin (S.val, C.val)
+
+/-- A helper function for what comes later. -/
+def α₂ (S : (PlusU1 n).LinSols) : ℚ := accQuad S.val
+
+lemma α₂_AFQ (S : (PlusU1 n).QuadSols) : α₂ S.1 = 0 := quadSol S
+
+lemma accQuad_α₁_α₂ (S : (PlusU1 n).LinSols) :
+    accQuad ((α₁ C S) • S + α₂ S • C.1).val = 0 := by
+  erw [add_AFL_quad]
+  rw [α₁, α₂]
+  ring
+
+lemma accQuad_α₁_α₂_zero (S : (PlusU1 n).LinSols) (h1 : α₁ C S = 0)
+    (h2 : α₂ S = 0) (a b : ℚ) : accQuad (a • S + b • C.1).val = 0 := by
+  erw [add_AFL_quad]
+  simp [α₁, α₂] at h1 h2
+  field_simp [h1, h2]
+
+/-- The construction of a `QuadSol` from a `LinSols` in the generic case. -/
+def genericToQuad (S : (PlusU1 n).LinSols) :
+    (PlusU1 n).QuadSols :=
+  linearToQuad ((α₁ C S) • S + α₂ S • C.1)  (accQuad_α₁_α₂ C S)
+
+lemma genericToQuad_on_quad (S : (PlusU1 n).QuadSols) :
+    genericToQuad C S.1 = (α₁ C S.1) • S := by
+  apply ACCSystemQuad.QuadSols.ext
+  change ((α₁ C S.1) • S.val + α₂ S.1 • C.val) = (α₁ C S.1) • S.val
+  rw [α₂_AFQ]
+  simp
+
+lemma genericToQuad_neq_zero (S : (PlusU1 n).QuadSols) (h : α₁ C S.1 ≠ 0) :
+    (α₁ C S.1)⁻¹ • genericToQuad C S.1 = S := by
+  rw [genericToQuad_on_quad, smul_smul, inv_mul_cancel h, one_smul]
+
+
+/-- The construction of a `QuadSol` from a `LinSols` in the special case when `α₁ C S = 0` and
+  `α₂ S = 0`. -/
+def specialToQuad (S : (PlusU1 n).LinSols) (a b : ℚ) (h1 : α₁ C S = 0)
+    (h2 : α₂ S = 0) : (PlusU1 n).QuadSols :=
+  linearToQuad (a • S + b • C.1) (accQuad_α₁_α₂_zero C S h1 h2 a b)
+
+lemma special_on_quad (S : (PlusU1 n).QuadSols)  (h1 : α₁ C S.1 = 0) :
+    specialToQuad C S.1 1 0 h1 (α₂_AFQ S) = S := by
+  apply ACCSystemQuad.QuadSols.ext
+  change (1 • S.val + 0 • C.val) = S.val
+  simp
+
+/-- The construction of a `QuadSols` from a `LinSols` and two rationals taking account of the
+generic and special cases. This function is a surjection. -/
+def toQuad : (PlusU1 n).LinSols × ℚ × ℚ → (PlusU1 n).QuadSols := fun S =>
+  if h : α₁ C S.1 = 0 ∧ α₂ S.1 = 0 then
+    specialToQuad C S.1 S.2.1 S.2.2 h.1 h.2
+  else
+    S.2.1 • genericToQuad C S.1
+
+/-- A function from `QuadSols` to `LinSols × ℚ × ℚ` which is a right inverse to `toQuad`. -/
+@[simp]
+def toQuadInv : (PlusU1 n).QuadSols → (PlusU1 n).LinSols × ℚ × ℚ := fun S =>
+  if α₁ C S.1 = 0 then
+    (S.1, 1, 0)
+  else
+    (S.1, (α₁ C S.1)⁻¹, 0)
+
+lemma toQuadInv_fst (S : (PlusU1 n).QuadSols) :
+    (toQuadInv C S).1 = S.1 := by
+  rw [toQuadInv]
+  split
+  rfl
+  rfl
+
+lemma toQuadInv_α₁_α₂ (S : (PlusU1 n).QuadSols) :
+    α₁ C S.1 = 0 ↔ α₁ C (toQuadInv C S).1 = 0 ∧ α₂ (toQuadInv C S).1 = 0 := by
+  rw [toQuadInv_fst, α₂_AFQ]
+  simp
+
+lemma toQuadInv_special (S : (PlusU1 n).QuadSols) (h : α₁ C S.1 = 0) :
+    specialToQuad C (toQuadInv C S).1 (toQuadInv C S).2.1 (toQuadInv C S).2.2
+    ((toQuadInv_α₁_α₂ C S).mp h).1 ((toQuadInv_α₁_α₂ C S).mp h).2 = S := by
+  simp only [toQuadInv_fst]
+  rw [show (toQuadInv C S).2.1 = 1 by rw [toQuadInv, if_pos h]]
+  rw [show (toQuadInv C S).2.2 = 0 by rw [toQuadInv, if_pos h]]
+  rw [special_on_quad]
+
+lemma toQuadInv_generic (S : (PlusU1 n).QuadSols) (h : α₁ C S.1 ≠ 0) :
+    (toQuadInv C S).2.1 • genericToQuad C (toQuadInv C S).1  = S := by
+  simp only [toQuadInv_fst]
+  rw [show (toQuadInv C S).2.1  = (α₁ C S.1)⁻¹ by rw [toQuadInv, if_neg h]]
+  rw [genericToQuad_neq_zero C S h]
+
+lemma toQuad_rightInverse : Function.RightInverse (@toQuadInv n C) (toQuad C) := by
+  intro S
+  by_cases h : α₁ C S.1 = 0
+  rw [toQuad, dif_pos ((toQuadInv_α₁_α₂ C S).mp h)]
+  exact toQuadInv_special C S h
+  rw [toQuad, dif_neg ((toQuadInv_α₁_α₂ C S).mpr.mt h)]
+  exact toQuadInv_generic C S h
+
+theorem toQuad_surjective : Function.Surjective (toQuad C) :=
+  Function.RightInverse.surjective (toQuad_rightInverse C)
+
+end QuadSol
+end PlusU1
+end SMRHN
diff --git a/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean b/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean
new file mode 100644
index 0000000..8e62257
--- /dev/null
+++ b/HepLean/AnomalyCancellation/SMNu/PlusU1/QuadSolToSol.lean
@@ -0,0 +1,147 @@
+/-
+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.BMinusL
+/-!
+# Solutions from quad solutions
+
+We use $B-L$ to form a surjective map from quad solutions to solutions. The main reference
+for this material is:
+
+- https://arxiv.org/abs/2006.03588
+
+-/
+
+universe v u
+
+namespace SMRHN
+namespace PlusU1
+
+namespace QuadSolToSol
+
+open SMνCharges
+open SMνACCs
+open BigOperators
+
+variable {n : ℕ}
+/-- A helper function for what follows. -/
+@[simp]
+def α₁ (S : (PlusU1 n).QuadSols) : ℚ := - 3 * cubeTriLin (S.val, S.val, (BL n).val)
+
+/-- A helper function for what follows. -/
+@[simp]
+def α₂ (S : (PlusU1 n).QuadSols) : ℚ := accCube S.val
+
+lemma cube_α₁_α₂_zero (S : (PlusU1 n).QuadSols) (a b : ℚ) (h1 : α₁ S = 0) (h2 : α₂ S = 0) :
+    accCube (BL.addQuad S a b).val = 0 := by
+  erw [BL.add_AFL_cube]
+  simp_all
+
+lemma α₂_AF (S : (PlusU1 n).Sols) : α₂ S.toQuadSols = 0 := S.2
+
+lemma BL_add_α₁_α₂_cube (S : (PlusU1 n).QuadSols) :
+    accCube (BL.addQuad S (α₁ S) (α₂ S)).val = 0 := by
+  erw [BL.add_AFL_cube]
+  field_simp
+  ring_nf
+
+lemma BL_add_α₁_α₂_AF (S : (PlusU1 n).Sols) :
+    BL.addQuad S.1 (α₁ S.1) (α₂ S.1) = (α₁ S.1) • S.1 := by
+  rw [α₂_AF, BL.addQuad_zero]
+
+/-- The construction of a `Sol` from a `QuadSol` in the generic case. -/
+def generic (S : (PlusU1 n).QuadSols) : (PlusU1 n).Sols :=
+  quadToAF (BL.addQuad S (α₁ S) (α₂ S)) (BL_add_α₁_α₂_cube S)
+
+lemma generic_on_AF (S : (PlusU1 n).Sols) : generic S.1 = (α₁ S.1) • S := by
+  apply ACCSystem.Sols.ext
+  change (BL.addQuad S.1 (α₁ S.1) (α₂ S.1)).val = _
+  rw [BL_add_α₁_α₂_AF]
+  rfl
+
+lemma generic_on_AF_α₁_ne_zero (S : (PlusU1 n).Sols) (h : α₁ S.1 ≠ 0) :
+    (α₁ S.1)⁻¹ • generic S.1 = S := by
+  rw [generic_on_AF, smul_smul, inv_mul_cancel h, one_smul]
+
+/-- The construction of a `Sol` from a `QuadSol` in the case when `α₁ S = 0` and `α₂ S = 0`. -/
+def special (S : (PlusU1 n).QuadSols) (a b : ℚ) (h1 : α₁ S = 0) (h2 : α₂ S = 0) :
+    (PlusU1 n).Sols :=
+  quadToAF (BL.addQuad S a b) (cube_α₁_α₂_zero S a b h1 h2)
+
+lemma special_on_AF (S : (PlusU1 n).Sols)  (h1 : α₁ S.1 = 0) :
+    special S.1 1 0 h1 (α₂_AF S) = S := by
+  apply ACCSystem.Sols.ext
+  change (BL.addQuad S.1 1 0).val = _
+  rw [BL.addQuad_zero]
+  simp
+
+
+end QuadSolToSol
+
+
+open QuadSolToSol
+/-- A map from `QuadSols × ℚ × ℚ` to `Sols` taking account of the special and generic cases.
+We will show that this map is a surjection. -/
+def quadSolToSol {n : ℕ} : (PlusU1 n).QuadSols × ℚ × ℚ → (PlusU1 n).Sols := fun S =>
+  if h1 : α₁ S.1 = 0 ∧  α₂ S.1 = 0 then
+    special S.1 S.2.1 S.2.2 h1.1 h1.2
+  else
+    S.2.1 • generic S.1
+
+/-- A map from `Sols` to `QuadSols × ℚ × ℚ` which forms a right-inverse to `quadSolToSol`, as
+shown in `quadSolToSolInv_rightInverse`. -/
+def quadSolToSolInv {n : ℕ} : (PlusU1 n).Sols → (PlusU1 n).QuadSols × ℚ × ℚ :=
+    fun S =>
+  if α₁ S.1 = 0 then
+    (S.1, 1, 0)
+  else
+    (S.1, (α₁ S.1)⁻¹, 0)
+
+lemma quadSolToSolInv_1 (S : (PlusU1 n).Sols)  :
+    (quadSolToSolInv S).1 = S.1 := by
+  simp [quadSolToSolInv]
+  split
+  rfl
+  rfl
+
+lemma quadSolToSolInv_α₁_α₂_zero (S : (PlusU1 n).Sols) (h : α₁ S.1 = 0) :
+    α₁ (quadSolToSolInv S).1 = 0 ∧ α₂ (quadSolToSolInv S).1 = 0 := by
+  rw [quadSolToSolInv_1, α₂_AF S, h]
+  simp
+
+lemma quadSolToSolInv_α₁_α₂_neq_zero (S : (PlusU1 n).Sols) (h : α₁ S.1 ≠  0) :
+   ¬  (α₁ (quadSolToSolInv S).1 = 0 ∧ α₂ (quadSolToSolInv S).1 = 0) := by
+  rw [not_and, quadSolToSolInv_1, α₂_AF S]
+  intro hn
+  simp_all
+
+lemma quadSolToSolInv_special (S : (PlusU1 n).Sols) (h : α₁ S.1 = 0) :
+    special (quadSolToSolInv S).1 (quadSolToSolInv S).2.1 (quadSolToSolInv S).2.2
+    (quadSolToSolInv_α₁_α₂_zero S h).1 (quadSolToSolInv_α₁_α₂_zero S h).2   = S := by
+  simp [quadSolToSolInv_1]
+  rw [show (quadSolToSolInv S).2.1  = 1 by rw [quadSolToSolInv, if_pos h]]
+  rw [show (quadSolToSolInv S).2.2  = 0 by rw [quadSolToSolInv, if_pos h]]
+  rw [special_on_AF]
+
+lemma quadSolToSolInv_generic (S : (PlusU1 n).Sols) (h : α₁ S.1 ≠ 0) :
+    (quadSolToSolInv S).2.1 • generic (quadSolToSolInv S).1  = S := by
+  simp [quadSolToSolInv_1]
+  rw [show (quadSolToSolInv S).2.1  = (α₁ S.1)⁻¹ by rw [quadSolToSolInv, if_neg h]]
+  rw [generic_on_AF_α₁_ne_zero S h]
+
+lemma quadSolToSolInv_rightInverse : Function.RightInverse (@quadSolToSolInv n) quadSolToSol := by
+  intro S
+  by_cases h : α₁ S.1 = 0
+  rw [quadSolToSol, dif_pos (quadSolToSolInv_α₁_α₂_zero S h)]
+  exact quadSolToSolInv_special S h
+  rw [quadSolToSol, dif_neg (quadSolToSolInv_α₁_α₂_neq_zero S h)]
+  exact quadSolToSolInv_generic S h
+
+theorem quadSolToSol_surjective : Function.Surjective (@quadSolToSol n) :=
+  Function.RightInverse.surjective quadSolToSolInv_rightInverse
+
+end PlusU1
+end SMRHN