Physlib.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.QuadSol

Imports

/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.Basic

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

@[expose] public section



set_option backward.isDefEq.respectTransparency false in
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) := byn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).LinSolsa:ℚb:ℚ⊢ accQuad (a • S.val + b • C.val) = a * (a * accQuad S.val + 2 * b * (quadBiLin S.val) C.val)
  erw [BiLinearSymm.toHomogeneousQuad_add,n:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).LinSolsa:ℚb:ℚ⊢ quadBiLin.toHomogeneousQuad (a • S.val) + quadBiLin.toHomogeneousQuad (b • C.val) +
    2 * (quadBiLin (a • S.val)) (b • C.val) =
  a * (a * accQuad S.val + 2 * b * (quadBiLin S.val) C.val) quadSol (b • C)n:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).LinSolsa:ℚb:ℚ⊢ quadBiLin.toHomogeneousQuad (a • S.val) + 0 + 2 * (quadBiLin (a • S.val)) (b • C.val) =
  a * (a * accQuad S.val + 2 * b * (quadBiLin S.val) C.val)]n:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).LinSolsa:ℚb:ℚ⊢ quadBiLin.toHomogeneousQuad (a • S.val) + 0 + 2 * (quadBiLin (a • S.val)) (b • C.val) =
  a * (a * accQuad S.val + 2 * b * (quadBiLin S.val) C.val)
  rw [quadBiLin.map_smul₁,n:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).LinSolsa:ℚb:ℚ⊢ quadBiLin.toHomogeneousQuad (a • S.val) + 0 + 2 * (a * (quadBiLin S.val) (b • C.val)) =
  a * (a * accQuad S.val + 2 * b * (quadBiLin S.val) C.val)n:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).LinSolsa:ℚb:ℚ⊢ quadBiLin.toHomogeneousQuad (a • S.val) + 0 + 2 * (a * (b * (quadBiLin S.val) C.val)) =
  a * (a * accQuad S.val + 2 * b * (quadBiLin S.val) C.val) quadBiLin.map_smul₂n:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).LinSolsa:ℚb:ℚ⊢ quadBiLin.toHomogeneousQuad (a • S.val) + 0 + 2 * (a * (b * (quadBiLin S.val) C.val)) =
  a * (a * accQuad S.val + 2 * b * (quadBiLin S.val) C.val)n:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).LinSolsa:ℚb:ℚ⊢ quadBiLin.toHomogeneousQuad (a • S.val) + 0 + 2 * (a * (b * (quadBiLin S.val) C.val)) =
  a * (a * accQuad S.val + 2 * b * (quadBiLin S.val) C.val)]n:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).LinSolsa:ℚb:ℚ⊢ quadBiLin.toHomogeneousQuad (a • S.val) + 0 + 2 * (a * (b * (quadBiLin S.val) C.val)) =
  a * (a * accQuad S.val + 2 * b * (quadBiLin S.val) C.val)
  erw [accQuad.map_smuln:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).LinSolsa:ℚb:ℚ⊢ a ^ 2 * accQuad S.val + 0 + 2 * (a * (b * (quadBiLin S.val) C.val)) =
  a * (a * accQuad S.val + 2 * b * (quadBiLin S.val) C.val)]n:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).LinSolsa:ℚb:ℚ⊢ a ^ 2 * accQuad S.val + 0 + 2 * (a * (b * (quadBiLin S.val) C.val)) =
  a * (a * accQuad S.val + 2 * b * (quadBiLin S.val) C.val)
  ringAll goals completed! 🐙

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 Slemma accQuad_α₁_α₂ (S : (PlusU1 n).LinSols) :
    accQuad ((α₁ C S) • S + α₂ S • C.1).val = 0 := byn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).LinSols⊢ accQuad (α₁ C S • S + α₂ S • C.toLinSols).val = 0
  erw [add_AFL_quad,n:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).LinSols⊢ α₁ C S * (α₁ C S * accQuad S.val + 2 * α₂ S * (quadBiLin S.val) C.val) = 0 α₁,n:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).LinSols⊢ -2 * (quadBiLin S.val) C.val * (-2 * (quadBiLin S.val) C.val * accQuad S.val + 2 * α₂ S * (quadBiLin S.val) C.val) = 0 α₂n:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).LinSols⊢ -2 * (quadBiLin S.val) C.val *
    (-2 * (quadBiLin S.val) C.val * accQuad S.val + 2 * accQuad S.val * (quadBiLin S.val) C.val) =
  0]n:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).LinSols⊢ -2 * (quadBiLin S.val) C.val *
    (-2 * (quadBiLin S.val) C.val * accQuad S.val + 2 * accQuad S.val * (quadBiLin S.val) C.val) =
  0
  ringAll goals completed! 🐙lemma accQuad_α₁_α₂_zero (S : (PlusU1 n).LinSols) (h1 : α₁ C S = 0)
    (h2 : α₂ S = 0) (a b : ℚ) : accQuad (a • S + b • C.1).val = 0 := byn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).LinSolsh1:α₁ C S = 0h2:α₂ S = 0a:ℚb:ℚ⊢ accQuad (a • S + b • C.toLinSols).val = 0
  erw [add_AFL_quadn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).LinSolsh1:α₁ C S = 0h2:α₂ S = 0a:ℚb:ℚ⊢ a * (a * accQuad S.val + 2 * b * (quadBiLin S.val) C.val) = 0]n:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).LinSolsh1:α₁ C S = 0h2:α₂ S = 0a:ℚb:ℚ⊢ a * (a * accQuad S.val + 2 * b * (quadBiLin S.val) C.val) = 0
  simp only [α₁, quadBiLin_toFun_apply, Fin.isValue, neg_mul, neg_eq_zero, mul_eq_zero,
    OfNat.ofNat_ne_zero, false_or, α₂, HomogeneousQuadratic, accQuad] at h1 h2n:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).LinSolsh2:quadBiLin.toHomogeneousQuad S.val = 0a:ℚb:ℚh1:∑ x,
    (toSpeciesEquiv S.val 0 x * toSpeciesEquiv C.val 0 x +
            -(2 * (toSpeciesEquiv S.val 1 x * toSpeciesEquiv C.val 1 x)) +
          toSpeciesEquiv S.val 2 x * toSpeciesEquiv C.val 2 x +
        -(toSpeciesEquiv S.val 3 x * toSpeciesEquiv C.val 3 x) +
      toSpeciesEquiv S.val 4 x * toSpeciesEquiv C.val 4 x) =
  0⊢ a * (a * accQuad S.val + 2 * b * (quadBiLin S.val) C.val) = 0
  simp [h1, h2]All goals completed! 🐙

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 := byn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSols⊢ genericToQuad C S.toLinSols = α₁ C S.toLinSols • S
  apply ACCSystemQuad.QuadSols.extn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSols⊢ (genericToQuad C S.toLinSols).val = (α₁ C S.toLinSols • S).val
  change ((α₁ C S.1) • S.val + α₂ S.1 • C.val) = (α₁ C S.1) • S.valn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSols⊢ α₁ C S.toLinSols • S.val + α₂ S.toLinSols • C.val = α₁ C S.toLinSols • S.val
  simp [α₂_AFQ]All goals completed! 🐙



lemma genericToQuad_ne_zero (S : (PlusU1 n).QuadSols) (h : α₁ C S.1 ≠ 0) :
    (α₁ C S.1)⁻¹ • genericToQuad C S.1 = S := byn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh:α₁ C S.toLinSols ≠ 0⊢ (α₁ C S.toLinSols)⁻¹ • genericToQuad C S.toLinSols = S
  rw [genericToQuad_on_quad,n:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh:α₁ C S.toLinSols ≠ 0⊢ (α₁ C S.toLinSols)⁻¹ • α₁ C S.toLinSols • S = SAll goals completed! 🐙 smul_smul,n:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh:α₁ C S.toLinSols ≠ 0⊢ ((α₁ C S.toLinSols)⁻¹ * α₁ C S.toLinSols) • S = SAll goals completed! 🐙 Rat.inv_mul_cancel _ h,n:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh:α₁ C S.toLinSols ≠ 0⊢ 1 • S = SAll goals completed! 🐙 one_smuln:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh:α₁ C S.toLinSols ≠ 0⊢ S = SAll goals completed! 🐙]All goals completed! 🐙

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 := byn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh1:α₁ C S.toLinSols = 0⊢ specialToQuad C S.toLinSols 1 0 h1 ⋯ = S
  apply ACCSystemQuad.QuadSols.extn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh1:α₁ C S.toLinSols = 0⊢ (specialToQuad C S.toLinSols 1 0 h1 ⋯).val = S.val
  change (1 • S.val + 0 • C.val) = S.valn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh1:α₁ C S.toLinSols = 0⊢ 1 • S.val + 0 • C.val = S.val
  simpAll goals completed! 🐙

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 := byn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSols⊢ (toQuadInv C S).1 = S.toLinSols
  rw [toQuadInvn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSols⊢ (if α₁ C S.toLinSols = 0 then (S.toLinSols, 1, 0) else (S.toLinSols, (α₁ C S.toLinSols)⁻¹, 0)).1 = S.toLinSolsn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSols⊢ (if α₁ C S.toLinSols = 0 then (S.toLinSols, 1, 0) else (S.toLinSols, (α₁ C S.toLinSols)⁻¹, 0)).1 = S.toLinSols]n:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSols⊢ (if α₁ C S.toLinSols = 0 then (S.toLinSols, 1, 0) else (S.toLinSols, (α₁ C S.toLinSols)⁻¹, 0)).1 = S.toLinSols
  splitisTruen:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh✝:α₁ C S.toLinSols = 0⊢ (S.toLinSols, 1, 0).1 = S.toLinSolsisFalsen:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh✝:¬α₁ C S.toLinSols = 0⊢ (S.toLinSols, (α₁ C S.toLinSols)⁻¹, 0).1 = S.toLinSols <;>isTruen:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh✝:α₁ C S.toLinSols = 0⊢ (S.toLinSols, 1, 0).1 = S.toLinSolsisFalsen:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh✝:¬α₁ C S.toLinSols = 0⊢ (S.toLinSols, (α₁ C S.toLinSols)⁻¹, 0).1 = S.toLinSols rflAll goals completed! 🐙

lemma toQuadInv_α₁_α₂ (S : (PlusU1 n).QuadSols) :
    α₁ C S.1 = 0 ↔ α₁ C (toQuadInv C S).1 = 0 ∧ α₂ (toQuadInv C S).1 = 0 := byn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSols⊢ α₁ C S.toLinSols = 0 ↔ α₁ C (toQuadInv C S).1 = 0 ∧ α₂ (toQuadInv C S).1 = 0
  rw [toQuadInv_fst,n:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSols⊢ α₁ C S.toLinSols = 0 ↔ α₁ C S.toLinSols = 0 ∧ α₂ S.toLinSols = 0n:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSols⊢ α₁ C S.toLinSols = 0 ↔ α₁ C S.toLinSols = 0 ∧ 0 = 0 α₂_AFQn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSols⊢ α₁ C S.toLinSols = 0 ↔ α₁ C S.toLinSols = 0 ∧ 0 = 0n:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSols⊢ α₁ C S.toLinSols = 0 ↔ α₁ C S.toLinSols = 0 ∧ 0 = 0]n:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSols⊢ α₁ C S.toLinSols = 0 ↔ α₁ C S.toLinSols = 0 ∧ 0 = 0
  simpAll goals completed! 🐙

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 := byn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh:α₁ C S.toLinSols = 0⊢ specialToQuad C (toQuadInv C S).1 (toQuadInv C S).2.1 (toQuadInv C S).2.2 ⋯ ⋯ = S
  simp only [toQuadInv_fst]n:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh:α₁ C S.toLinSols = 0⊢ specialToQuad C S.toLinSols (toQuadInv C S).2.1 (toQuadInv C S).2.2 ⋯ ⋯ = S
  rw [show (toQuadInv C S).2.1 = 1 byn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh:α₁ C S.toLinSols = 0⊢ specialToQuad C (toQuadInv C S).1 (toQuadInv C S).2.1 (toQuadInv C S).2.2 ⋯ ⋯ = SAll goals completed! 🐙 rw [toQuadInv,n:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh:α₁ C S.toLinSols = 0⊢ (if α₁ C S.toLinSols = 0 then (S.toLinSols, 1, 0) else (S.toLinSols, (α₁ C S.toLinSols)⁻¹, 0)).2.1 = 1All goals completed! 🐙All goals completed! 🐙 if_pos hn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh:α₁ C S.toLinSols = 0⊢ (S.toLinSols, 1, 0).2.1 = 1All goals completed! 🐙All goals completed! 🐙]All goals completed! 🐙All goals completed! 🐙,
    show (toQuadInv C S).2.2 = 0 byn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh:α₁ C S.toLinSols = 0⊢ specialToQuad C (toQuadInv C S).1 (toQuadInv C S).2.1 (toQuadInv C S).2.2 ⋯ ⋯ = SAll goals completed! 🐙 rw [toQuadInv,n:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh:α₁ C S.toLinSols = 0⊢ (if α₁ C S.toLinSols = 0 then (S.toLinSols, 1, 0) else (S.toLinSols, (α₁ C S.toLinSols)⁻¹, 0)).2.2 = 0All goals completed! 🐙All goals completed! 🐙 if_pos hn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh:α₁ C S.toLinSols = 0⊢ (S.toLinSols, 1, 0).2.2 = 0All goals completed! 🐙All goals completed! 🐙]All goals completed! 🐙All goals completed! 🐙, special_on_quadn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh:α₁ C S.toLinSols = 0⊢ S = SAll goals completed! 🐙]All goals completed! 🐙

lemma toQuadInv_generic (S : (PlusU1 n).QuadSols) (h : α₁ C S.1 ≠ 0) :
    (toQuadInv C S).2.1 • genericToQuad C (toQuadInv C S).1 = S := byn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh:α₁ C S.toLinSols ≠ 0⊢ (toQuadInv C S).2.1 • genericToQuad C (toQuadInv C S).1 = S
  simp only [toQuadInv_fst]n:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh:α₁ C S.toLinSols ≠ 0⊢ (toQuadInv C S).2.1 • genericToQuad C S.toLinSols = S
  rw [show (toQuadInv C S).2.1 = (α₁ C S.1)⁻¹ byn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh:α₁ C S.toLinSols ≠ 0⊢ (toQuadInv C S).2.1 • genericToQuad C (toQuadInv C S).1 = SAll goals completed! 🐙 rw [toQuadInv,n:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh:α₁ C S.toLinSols ≠ 0⊢ (if α₁ C S.toLinSols = 0 then (S.toLinSols, 1, 0) else (S.toLinSols, (α₁ C S.toLinSols)⁻¹, 0)).2.1 =
  (α₁ C S.toLinSols)⁻¹All goals completed! 🐙All goals completed! 🐙 if_neg hn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh:α₁ C S.toLinSols ≠ 0⊢ (S.toLinSols, (α₁ C S.toLinSols)⁻¹, 0).2.1 = (α₁ C S.toLinSols)⁻¹All goals completed! 🐙All goals completed! 🐙]All goals completed! 🐙All goals completed! 🐙,
    genericToQuad_ne_zero C S hn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh:α₁ C S.toLinSols ≠ 0⊢ S = SAll goals completed! 🐙]All goals completed! 🐙

lemma toQuad_rightInverse : Function.RightInverse (@toQuadInv n C) (toQuad C) := byn:ℕC:(PlusU1 n).QuadSols⊢ Function.RightInverse (toQuadInv C) (toQuad C)
  intro Sn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSols⊢ toQuad C (toQuadInv C S) = S
  by_cases h : α₁ C S.1 = 0posn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh:α₁ C S.toLinSols = 0⊢ toQuad C (toQuadInv C S) = Snegn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh:¬α₁ C S.toLinSols = 0⊢ toQuad C (toQuadInv C S) = S
  ·posn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh:α₁ C S.toLinSols = 0⊢ toQuad C (toQuadInv C S) = S rw [toQuad,posn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh:α₁ C S.toLinSols = 0⊢ (if h : α₁ C (toQuadInv C S).1 = 0 ∧ α₂ (toQuadInv C S).1 = 0 then
    specialToQuad C (toQuadInv C S).1 (toQuadInv C S).2.1 (toQuadInv C S).2.2 ⋯ ⋯
  else (toQuadInv C S).2.1 • genericToQuad C (toQuadInv C S).1) =
  Sposn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh:α₁ C S.toLinSols = 0⊢ specialToQuad C (toQuadInv C S).1 (toQuadInv C S).2.1 (toQuadInv C S).2.2 ⋯ ⋯ = S dif_pos ((toQuadInv_α₁_α₂ C S).mp h)posn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh:α₁ C S.toLinSols = 0⊢ specialToQuad C (toQuadInv C S).1 (toQuadInv C S).2.1 (toQuadInv C S).2.2 ⋯ ⋯ = Sposn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh:α₁ C S.toLinSols = 0⊢ specialToQuad C (toQuadInv C S).1 (toQuadInv C S).2.1 (toQuadInv C S).2.2 ⋯ ⋯ = S]posn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh:α₁ C S.toLinSols = 0⊢ specialToQuad C (toQuadInv C S).1 (toQuadInv C S).2.1 (toQuadInv C S).2.2 ⋯ ⋯ = S
    exact toQuadInv_special C S hAll goals completed! 🐙
  ·negn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh:¬α₁ C S.toLinSols = 0⊢ toQuad C (toQuadInv C S) = S rw [toQuad,negn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh:¬α₁ C S.toLinSols = 0⊢ (if h : α₁ C (toQuadInv C S).1 = 0 ∧ α₂ (toQuadInv C S).1 = 0 then
    specialToQuad C (toQuadInv C S).1 (toQuadInv C S).2.1 (toQuadInv C S).2.2 ⋯ ⋯
  else (toQuadInv C S).2.1 • genericToQuad C (toQuadInv C S).1) =
  Snegn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh:¬α₁ C S.toLinSols = 0⊢ (toQuadInv C S).2.1 • genericToQuad C (toQuadInv C S).1 = S dif_neg ((toQuadInv_α₁_α₂ C S).mpr.mt h)negn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh:¬α₁ C S.toLinSols = 0⊢ (toQuadInv C S).2.1 • genericToQuad C (toQuadInv C S).1 = Snegn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh:¬α₁ C S.toLinSols = 0⊢ (toQuadInv C S).2.1 • genericToQuad C (toQuadInv C S).1 = S]negn:ℕC:(PlusU1 n).QuadSolsS:(PlusU1 n).QuadSolsh:¬α₁ C S.toLinSols = 0⊢ (toQuadInv C S).2.1 • genericToQuad C (toQuadInv C S).1 = S
    exact toQuadInv_generic C S hAll goals completed! 🐙theorem toQuad_surjective : Function.Surjective (toQuad C) :=
  Function.RightInverse.surjective (toQuad_rightInverse C)