Physlib.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.PlusU1.QuadSolToSol

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.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

@[expose] public section

A helper function for what follows.

def α₁ (S : (PlusU1 n).QuadSols) : ℚ := - 3 * cubeTriLin S.val S.val (BL n).val

A helper function for what follows.

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 := byn:ℕS:(PlusU1 n).QuadSolsa:ℚb:ℚh1:α₁ S = 0h2:α₂ S = 0⊢ accCube (BL.addQuad S a b).val = 0
  erw [BL.add_AFL_cuben:ℕS:(PlusU1 n).QuadSolsa:ℚb:ℚh1:α₁ S = 0h2:α₂ S = 0⊢ a ^ 2 * (a * accCube S.val + 3 * b * ((cubeTriLin S.val) S.val) (BL n).val) = 0]n:ℕS:(PlusU1 n).QuadSolsa:ℚb:ℚh1:α₁ S = 0h2:α₂ S = 0⊢ a ^ 2 * (a * accCube S.val + 3 * b * ((cubeTriLin S.val) S.val) (BL n).val) = 0
  simp_all [α₁, α₂]All goals completed! 🐙lemma α₂_AF (S : (PlusU1 n).Sols) : α₂ S.toQuadSols = 0 := S.2lemma BL_add_α₁_α₂_cube (S : (PlusU1 n).QuadSols) :
    accCube (BL.addQuad S (α₁ S) (α₂ S)).val = 0 := byn:ℕS:(PlusU1 n).QuadSols⊢ accCube (BL.addQuad S (α₁ S) (α₂ S)).val = 0
  erw [BL.add_AFL_cuben:ℕS:(PlusU1 n).QuadSols⊢ α₁ S ^ 2 * (α₁ S * accCube S.val + 3 * α₂ S * ((cubeTriLin S.val) S.val) (BL n).val) = 0]n:ℕS:(PlusU1 n).QuadSols⊢ α₁ S ^ 2 * (α₁ S * accCube S.val + 3 * α₂ S * ((cubeTriLin S.val) S.val) (BL n).val) = 0
  simp only [α₁, BL_val, neg_mul, even_two, Even.neg_pow, α₂, mul_eq_zero, ne_eq,
    OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff, false_or]n:ℕS:(PlusU1 n).QuadSols⊢ ((cubeTriLin S.val) S.val) ((familyUniversal n) BL₁.val) = 0 ∨
  -(3 * ((cubeTriLin S.val) S.val) ((familyUniversal n) BL₁.val) * accCube S.val) +
      3 * accCube S.val * ((cubeTriLin S.val) S.val) ((familyUniversal n) BL₁.val) =
    0
  rightn:ℕS:(PlusU1 n).QuadSols⊢ -(3 * ((cubeTriLin S.val) S.val) ((familyUniversal n) BL₁.val) * accCube S.val) +
    3 * accCube S.val * ((cubeTriLin S.val) S.val) ((familyUniversal n) BL₁.val) =
  0
  field_simpn:ℕS:(PlusU1 n).QuadSols⊢ 3 * ((cubeTriLin S.val) S.val) ((familyUniversal n) BL₁.val) * accCube S.val * (-1 + 1) = 0
  ringAll goals completed! 🐙

lemma BL_add_α₁_α₂_AF (S : (PlusU1 n).Sols) :
    BL.addQuad S.1 (α₁ S.1) (α₂ S.1) = (α₁ S.1) • S.1 := byn:ℕS:(PlusU1 n).Sols⊢ BL.addQuad S.toQuadSols (α₁ S.toQuadSols) (α₂ S.toQuadSols) = α₁ S.toQuadSols • S.toQuadSols
  rw [α₂_AF,n:ℕS:(PlusU1 n).Sols⊢ BL.addQuad S.toQuadSols (α₁ S.toQuadSols) 0 = α₁ S.toQuadSols • S.toQuadSolsAll goals completed! 🐙 BL.addQuad_zeron:ℕS:(PlusU1 n).Sols⊢ α₁ S.toQuadSols • S.toQuadSols = α₁ S.toQuadSols • S.toQuadSolsAll goals completed! 🐙]All goals completed! 🐙

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 := byn:ℕS:(PlusU1 n).Sols⊢ generic S.toQuadSols = α₁ S.toQuadSols • S
  apply ACCSystem.Sols.extn:ℕS:(PlusU1 n).Sols⊢ (generic S.toQuadSols).val = (α₁ S.toQuadSols • S).val
  change (BL.addQuad S.1 (α₁ S.1) (α₂ S.1)).val = _n:ℕS:(PlusU1 n).Sols⊢ (BL.addQuad S.toQuadSols (α₁ S.toQuadSols) (α₂ S.toQuadSols)).val = (α₁ S.toQuadSols • S).val
  rw [BL_add_α₁_α₂_AFn:ℕS:(PlusU1 n).Sols⊢ (α₁ S.toQuadSols • S.toQuadSols).val = (α₁ S.toQuadSols • S).valn:ℕS:(PlusU1 n).Sols⊢ (α₁ S.toQuadSols • S.toQuadSols).val = (α₁ S.toQuadSols • S).val]n:ℕS:(PlusU1 n).Sols⊢ (α₁ S.toQuadSols • S.toQuadSols).val = (α₁ S.toQuadSols • S).val
  rflAll goals completed! 🐙



lemma generic_on_AF_α₁_ne_zero (S : (PlusU1 n).Sols) (h : α₁ S.1 ≠ 0) :
    (α₁ S.1)⁻¹ • generic S.1 = S := byn:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols ≠ 0⊢ (α₁ S.toQuadSols)⁻¹ • generic S.toQuadSols = S
  rw [generic_on_AF,n:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols ≠ 0⊢ (α₁ S.toQuadSols)⁻¹ • α₁ S.toQuadSols • S = SAll goals completed! 🐙 smul_smul,n:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols ≠ 0⊢ ((α₁ S.toQuadSols)⁻¹ * α₁ S.toQuadSols) • S = SAll goals completed! 🐙 inv_mul_cancel₀ h,n:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols ≠ 0⊢ 1 • S = SAll goals completed! 🐙 one_smuln:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols ≠ 0⊢ S = SAll goals completed! 🐙]All goals completed! 🐙

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 := byn:ℕS:(PlusU1 n).Solsh1:α₁ S.toQuadSols = 0⊢ special S.toQuadSols 1 0 h1 ⋯ = S
  apply ACCSystem.Sols.extn:ℕS:(PlusU1 n).Solsh1:α₁ S.toQuadSols = 0⊢ (special S.toQuadSols 1 0 h1 ⋯).val = S.val
  change (BL.addQuad S.1 1 0).val = _n:ℕS:(PlusU1 n).Solsh1:α₁ S.toQuadSols = 0⊢ (BL.addQuad S.toQuadSols 1 0).val = S.val
  rw [BL.addQuad_zeron:ℕS:(PlusU1 n).Solsh1:α₁ S.toQuadSols = 0⊢ (1 • S.toQuadSols).val = S.valn:ℕS:(PlusU1 n).Solsh1:α₁ S.toQuadSols = 0⊢ (1 • S.toQuadSols).val = S.val]n:ℕS:(PlusU1 n).Solsh1:α₁ S.toQuadSols = 0⊢ (1 • S.toQuadSols).val = S.val
  simpAll goals completed! 🐙

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 := byn:ℕS:(PlusU1 n).Sols⊢ (quadSolToSolInv S).1 = S.toQuadSols
  simp only [quadSolToSolInv, α₁, BL_val, SMνACCs.cubeTriLin_toFun_apply_apply, Fin.isValue,
    neg_mul, neg_eq_zero, mul_eq_zero, OfNat.ofNat_ne_zero, false_or]n:ℕS:(PlusU1 n).Sols⊢ (if
        ∑ i,
            (6 *
                        (SMνCharges.toSpeciesEquiv S.val 0 i * SMνCharges.toSpeciesEquiv S.val 0 i *
                          SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 0 i) +
                      3 *
                        (SMνCharges.toSpeciesEquiv S.val 1 i * SMνCharges.toSpeciesEquiv S.val 1 i *
                          SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 1 i) +
                    3 *
                      (SMνCharges.toSpeciesEquiv S.val 2 i * SMνCharges.toSpeciesEquiv S.val 2 i *
                        SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 2 i) +
                  2 *
                    (SMνCharges.toSpeciesEquiv S.val 3 i * SMνCharges.toSpeciesEquiv S.val 3 i *
                      SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 3 i) +
                SMνCharges.toSpeciesEquiv S.val 4 i * SMνCharges.toSpeciesEquiv S.val 4 i *
                  SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 4 i +
              SMνCharges.toSpeciesEquiv S.val 5 i * SMνCharges.toSpeciesEquiv S.val 5 i *
                SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 5 i) =
          0 then
      (S.toQuadSols, 1, 0)
    else
      (S.toQuadSols,
        (-(3 *
              ∑ i,
                (6 *
                            (SMνCharges.toSpeciesEquiv S.val 0 i * SMνCharges.toSpeciesEquiv S.val 0 i *
                              SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 0 i) +
                          3 *
                            (SMνCharges.toSpeciesEquiv S.val 1 i * SMνCharges.toSpeciesEquiv S.val 1 i *
                              SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 1 i) +
                        3 *
                          (SMνCharges.toSpeciesEquiv S.val 2 i * SMνCharges.toSpeciesEquiv S.val 2 i *
                            SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 2 i) +
                      2 *
                        (SMνCharges.toSpeciesEquiv S.val 3 i * SMνCharges.toSpeciesEquiv S.val 3 i *
                          SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 3 i) +
                    SMνCharges.toSpeciesEquiv S.val 4 i * SMνCharges.toSpeciesEquiv S.val 4 i *
                      SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 4 i +
                  SMνCharges.toSpeciesEquiv S.val 5 i * SMνCharges.toSpeciesEquiv S.val 5 i *
                    SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 5 i)))⁻¹,
        0)).1 =
  S.toQuadSols
  splitisTruen:ℕS:(PlusU1 n).Solsh✝:∑ i,
    (6 *
                (SMνCharges.toSpeciesEquiv S.val 0 i * SMνCharges.toSpeciesEquiv S.val 0 i *
                  SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 0 i) +
              3 *
                (SMνCharges.toSpeciesEquiv S.val 1 i * SMνCharges.toSpeciesEquiv S.val 1 i *
                  SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 1 i) +
            3 *
              (SMνCharges.toSpeciesEquiv S.val 2 i * SMνCharges.toSpeciesEquiv S.val 2 i *
                SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 2 i) +
          2 *
            (SMνCharges.toSpeciesEquiv S.val 3 i * SMνCharges.toSpeciesEquiv S.val 3 i *
              SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 3 i) +
        SMνCharges.toSpeciesEquiv S.val 4 i * SMνCharges.toSpeciesEquiv S.val 4 i *
          SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 4 i +
      SMνCharges.toSpeciesEquiv S.val 5 i * SMνCharges.toSpeciesEquiv S.val 5 i *
        SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 5 i) =
  0⊢ (S.toQuadSols, 1, 0).1 = S.toQuadSolsisFalsen:ℕS:(PlusU1 n).Solsh✝:¬∑ i,
      (6 *
                  (SMνCharges.toSpeciesEquiv S.val 0 i * SMνCharges.toSpeciesEquiv S.val 0 i *
                    SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 0 i) +
                3 *
                  (SMνCharges.toSpeciesEquiv S.val 1 i * SMνCharges.toSpeciesEquiv S.val 1 i *
                    SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 1 i) +
              3 *
                (SMνCharges.toSpeciesEquiv S.val 2 i * SMνCharges.toSpeciesEquiv S.val 2 i *
                  SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 2 i) +
            2 *
              (SMνCharges.toSpeciesEquiv S.val 3 i * SMνCharges.toSpeciesEquiv S.val 3 i *
                SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 3 i) +
          SMνCharges.toSpeciesEquiv S.val 4 i * SMνCharges.toSpeciesEquiv S.val 4 i *
            SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 4 i +
        SMνCharges.toSpeciesEquiv S.val 5 i * SMνCharges.toSpeciesEquiv S.val 5 i *
          SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 5 i) =
    0⊢ (S.toQuadSols,
      (-(3 *
            ∑ i,
              (6 *
                          (SMνCharges.toSpeciesEquiv S.val 0 i * SMνCharges.toSpeciesEquiv S.val 0 i *
                            SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 0 i) +
                        3 *
                          (SMνCharges.toSpeciesEquiv S.val 1 i * SMνCharges.toSpeciesEquiv S.val 1 i *
                            SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 1 i) +
                      3 *
                        (SMνCharges.toSpeciesEquiv S.val 2 i * SMνCharges.toSpeciesEquiv S.val 2 i *
                          SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 2 i) +
                    2 *
                      (SMνCharges.toSpeciesEquiv S.val 3 i * SMνCharges.toSpeciesEquiv S.val 3 i *
                        SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 3 i) +
                  SMνCharges.toSpeciesEquiv S.val 4 i * SMνCharges.toSpeciesEquiv S.val 4 i *
                    SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 4 i +
                SMνCharges.toSpeciesEquiv S.val 5 i * SMνCharges.toSpeciesEquiv S.val 5 i *
                  SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 5 i)))⁻¹,
      0).1 =
  S.toQuadSols <;>isTruen:ℕS:(PlusU1 n).Solsh✝:∑ i,
    (6 *
                (SMνCharges.toSpeciesEquiv S.val 0 i * SMνCharges.toSpeciesEquiv S.val 0 i *
                  SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 0 i) +
              3 *
                (SMνCharges.toSpeciesEquiv S.val 1 i * SMνCharges.toSpeciesEquiv S.val 1 i *
                  SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 1 i) +
            3 *
              (SMνCharges.toSpeciesEquiv S.val 2 i * SMνCharges.toSpeciesEquiv S.val 2 i *
                SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 2 i) +
          2 *
            (SMνCharges.toSpeciesEquiv S.val 3 i * SMνCharges.toSpeciesEquiv S.val 3 i *
              SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 3 i) +
        SMνCharges.toSpeciesEquiv S.val 4 i * SMνCharges.toSpeciesEquiv S.val 4 i *
          SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 4 i +
      SMνCharges.toSpeciesEquiv S.val 5 i * SMνCharges.toSpeciesEquiv S.val 5 i *
        SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 5 i) =
  0⊢ (S.toQuadSols, 1, 0).1 = S.toQuadSolsisFalsen:ℕS:(PlusU1 n).Solsh✝:¬∑ i,
      (6 *
                  (SMνCharges.toSpeciesEquiv S.val 0 i * SMνCharges.toSpeciesEquiv S.val 0 i *
                    SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 0 i) +
                3 *
                  (SMνCharges.toSpeciesEquiv S.val 1 i * SMνCharges.toSpeciesEquiv S.val 1 i *
                    SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 1 i) +
              3 *
                (SMνCharges.toSpeciesEquiv S.val 2 i * SMνCharges.toSpeciesEquiv S.val 2 i *
                  SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 2 i) +
            2 *
              (SMνCharges.toSpeciesEquiv S.val 3 i * SMνCharges.toSpeciesEquiv S.val 3 i *
                SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 3 i) +
          SMνCharges.toSpeciesEquiv S.val 4 i * SMνCharges.toSpeciesEquiv S.val 4 i *
            SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 4 i +
        SMνCharges.toSpeciesEquiv S.val 5 i * SMνCharges.toSpeciesEquiv S.val 5 i *
          SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 5 i) =
    0⊢ (S.toQuadSols,
      (-(3 *
            ∑ i,
              (6 *
                          (SMνCharges.toSpeciesEquiv S.val 0 i * SMνCharges.toSpeciesEquiv S.val 0 i *
                            SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 0 i) +
                        3 *
                          (SMνCharges.toSpeciesEquiv S.val 1 i * SMνCharges.toSpeciesEquiv S.val 1 i *
                            SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 1 i) +
                      3 *
                        (SMνCharges.toSpeciesEquiv S.val 2 i * SMνCharges.toSpeciesEquiv S.val 2 i *
                          SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 2 i) +
                    2 *
                      (SMνCharges.toSpeciesEquiv S.val 3 i * SMνCharges.toSpeciesEquiv S.val 3 i *
                        SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 3 i) +
                  SMνCharges.toSpeciesEquiv S.val 4 i * SMνCharges.toSpeciesEquiv S.val 4 i *
                    SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 4 i +
                SMνCharges.toSpeciesEquiv S.val 5 i * SMνCharges.toSpeciesEquiv S.val 5 i *
                  SMνCharges.toSpeciesEquiv ((familyUniversal n) BL₁.val) 5 i)))⁻¹,
      0).1 =
  S.toQuadSols rflAll goals completed! 🐙

lemma quadSolToSolInv_α₁_α₂_zero (S : (PlusU1 n).Sols) (h : α₁ S.1 = 0) :
    α₁ (quadSolToSolInv S).1 = 0 ∧ α₂ (quadSolToSolInv S).1 = 0 := byn:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols = 0⊢ α₁ (quadSolToSolInv S).1 = 0 ∧ α₂ (quadSolToSolInv S).1 = 0
  rw [quadSolToSolInv_1,n:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols = 0⊢ α₁ S.toQuadSols = 0 ∧ α₂ S.toQuadSols = 0n:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols = 0⊢ 0 = 0 ∧ 0 = 0 α₂_AF S,n:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols = 0⊢ α₁ S.toQuadSols = 0 ∧ 0 = 0n:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols = 0⊢ 0 = 0 ∧ 0 = 0 hn:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols = 0⊢ 0 = 0 ∧ 0 = 0n:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols = 0⊢ 0 = 0 ∧ 0 = 0]n:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols = 0⊢ 0 = 0 ∧ 0 = 0
  exact Prod.mk_eq_zero.mp rflAll goals completed! 🐙

lemma quadSolToSolInv_α₁_α₂_ne_zero (S : (PlusU1 n).Sols) (h : α₁ S.1 ≠ 0) :
    ¬ (α₁ (quadSolToSolInv S).1 = 0 ∧ α₂ (quadSolToSolInv S).1 = 0) := byn:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols ≠ 0⊢ ¬(α₁ (quadSolToSolInv S).1 = 0 ∧ α₂ (quadSolToSolInv S).1 = 0)
  rw [not_and,n:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols ≠ 0⊢ α₁ (quadSolToSolInv S).1 = 0 → ¬α₂ (quadSolToSolInv S).1 = 0n:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols ≠ 0⊢ α₁ S.toQuadSols = 0 → ¬0 = 0 quadSolToSolInv_1,n:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols ≠ 0⊢ α₁ S.toQuadSols = 0 → ¬α₂ S.toQuadSols = 0n:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols ≠ 0⊢ α₁ S.toQuadSols = 0 → ¬0 = 0 α₂_AF Sn:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols ≠ 0⊢ α₁ S.toQuadSols = 0 → ¬0 = 0n:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols ≠ 0⊢ α₁ S.toQuadSols = 0 → ¬0 = 0]n:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols ≠ 0⊢ α₁ S.toQuadSols = 0 → ¬0 = 0
  intro hnn:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols ≠ 0hn:α₁ S.toQuadSols = 0⊢ ¬0 = 0
  simp_allAll goals completed! 🐙

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 := byn:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols = 0⊢ special (quadSolToSolInv S).1 (quadSolToSolInv S).2.1 (quadSolToSolInv S).2.2 ⋯ ⋯ = S
  simp only [quadSolToSolInv_1]n:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols = 0⊢ special S.toQuadSols (quadSolToSolInv S).2.1 (quadSolToSolInv S).2.2 ⋯ ⋯ = S
  rw [show (quadSolToSolInv S).2.1 = 1 byn:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols = 0⊢ special (quadSolToSolInv S).1 (quadSolToSolInv S).2.1 (quadSolToSolInv S).2.2 ⋯ ⋯ = Sn:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols = 0⊢ special S.toQuadSols 1 (quadSolToSolInv S).2.2 ⋯ ⋯ = S rw [quadSolToSolInv,n:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols = 0⊢ (if α₁ S.toQuadSols = 0 then (S.toQuadSols, 1, 0) else (S.toQuadSols, (α₁ S.toQuadSols)⁻¹, 0)).2.1 = 1All goals completed! 🐙n:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols = 0⊢ special S.toQuadSols 1 (quadSolToSolInv S).2.2 ⋯ ⋯ = S if_pos hn:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols = 0⊢ (S.toQuadSols, 1, 0).2.1 = 1All goals completed! 🐙n:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols = 0⊢ special S.toQuadSols 1 (quadSolToSolInv S).2.2 ⋯ ⋯ = S]All goals completed! 🐙n:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols = 0⊢ special S.toQuadSols 1 (quadSolToSolInv S).2.2 ⋯ ⋯ = S]n:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols = 0⊢ special S.toQuadSols 1 (quadSolToSolInv S).2.2 ⋯ ⋯ = S
  rw [show (quadSolToSolInv S).2.2 = 0 byn:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols = 0⊢ special (quadSolToSolInv S).1 (quadSolToSolInv S).2.1 (quadSolToSolInv S).2.2 ⋯ ⋯ = Sn:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols = 0⊢ special S.toQuadSols 1 0 ⋯ ⋯ = S rw [quadSolToSolInv,n:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols = 0⊢ (if α₁ S.toQuadSols = 0 then (S.toQuadSols, 1, 0) else (S.toQuadSols, (α₁ S.toQuadSols)⁻¹, 0)).2.2 = 0All goals completed! 🐙n:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols = 0⊢ special S.toQuadSols 1 0 ⋯ ⋯ = S if_pos hn:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols = 0⊢ (S.toQuadSols, 1, 0).2.2 = 0All goals completed! 🐙n:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols = 0⊢ special S.toQuadSols 1 0 ⋯ ⋯ = S]All goals completed! 🐙n:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols = 0⊢ special S.toQuadSols 1 0 ⋯ ⋯ = S]n:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols = 0⊢ special S.toQuadSols 1 0 ⋯ ⋯ = S
  rw [special_on_AFn:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols = 0⊢ S = SAll goals completed! 🐙]All goals completed! 🐙

lemma quadSolToSolInv_generic (S : (PlusU1 n).Sols) (h : α₁ S.1 ≠ 0) :
    (quadSolToSolInv S).2.1 • generic (quadSolToSolInv S).1 = S := byn:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols ≠ 0⊢ (quadSolToSolInv S).2.1 • generic (quadSolToSolInv S).1 = S
  simp only [quadSolToSolInv_1]n:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols ≠ 0⊢ (quadSolToSolInv S).2.1 • generic S.toQuadSols = S
  rw [show (quadSolToSolInv S).2.1 = (α₁ S.1)⁻¹ byn:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols ≠ 0⊢ (quadSolToSolInv S).2.1 • generic (quadSolToSolInv S).1 = Sn:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols ≠ 0⊢ (α₁ S.toQuadSols)⁻¹ • generic S.toQuadSols = S rw [quadSolToSolInv,n:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols ≠ 0⊢ (if α₁ S.toQuadSols = 0 then (S.toQuadSols, 1, 0) else (S.toQuadSols, (α₁ S.toQuadSols)⁻¹, 0)).2.1 = (α₁ S.toQuadSols)⁻¹All goals completed! 🐙n:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols ≠ 0⊢ (α₁ S.toQuadSols)⁻¹ • generic S.toQuadSols = S if_neg hn:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols ≠ 0⊢ (S.toQuadSols, (α₁ S.toQuadSols)⁻¹, 0).2.1 = (α₁ S.toQuadSols)⁻¹All goals completed! 🐙n:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols ≠ 0⊢ (α₁ S.toQuadSols)⁻¹ • generic S.toQuadSols = S]All goals completed! 🐙n:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols ≠ 0⊢ (α₁ S.toQuadSols)⁻¹ • generic S.toQuadSols = S]n:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols ≠ 0⊢ (α₁ S.toQuadSols)⁻¹ • generic S.toQuadSols = S
  rw [generic_on_AF_α₁_ne_zero S hn:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols ≠ 0⊢ S = SAll goals completed! 🐙]All goals completed! 🐙

lemma quadSolToSolInv_rightInverse : Function.RightInverse (@quadSolToSolInv n) quadSolToSol := byn:ℕ⊢ Function.RightInverse quadSolToSolInv quadSolToSol
  intro Sn:ℕS:(PlusU1 n).Sols⊢ quadSolToSol (quadSolToSolInv S) = S
  by_cases h : α₁ S.1 = 0posn:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols = 0⊢ quadSolToSol (quadSolToSolInv S) = Snegn:ℕS:(PlusU1 n).Solsh:¬α₁ S.toQuadSols = 0⊢ quadSolToSol (quadSolToSolInv S) = S
  ·posn:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols = 0⊢ quadSolToSol (quadSolToSolInv S) = S rw [quadSolToSol,posn:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols = 0⊢ (if h1 : α₁ (quadSolToSolInv S).1 = 0 ∧ α₂ (quadSolToSolInv S).1 = 0 then
    special (quadSolToSolInv S).1 (quadSolToSolInv S).2.1 (quadSolToSolInv S).2.2 ⋯ ⋯
  else (quadSolToSolInv S).2.1 • generic (quadSolToSolInv S).1) =
  Sposn:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols = 0⊢ special (quadSolToSolInv S).1 (quadSolToSolInv S).2.1 (quadSolToSolInv S).2.2 ⋯ ⋯ = S dif_pos (quadSolToSolInv_α₁_α₂_zero S h)posn:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols = 0⊢ special (quadSolToSolInv S).1 (quadSolToSolInv S).2.1 (quadSolToSolInv S).2.2 ⋯ ⋯ = Sposn:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols = 0⊢ special (quadSolToSolInv S).1 (quadSolToSolInv S).2.1 (quadSolToSolInv S).2.2 ⋯ ⋯ = S]posn:ℕS:(PlusU1 n).Solsh:α₁ S.toQuadSols = 0⊢ special (quadSolToSolInv S).1 (quadSolToSolInv S).2.1 (quadSolToSolInv S).2.2 ⋯ ⋯ = S
    exact quadSolToSolInv_special S hAll goals completed! 🐙
  ·negn:ℕS:(PlusU1 n).Solsh:¬α₁ S.toQuadSols = 0⊢ quadSolToSol (quadSolToSolInv S) = S rw [quadSolToSol,negn:ℕS:(PlusU1 n).Solsh:¬α₁ S.toQuadSols = 0⊢ (if h1 : α₁ (quadSolToSolInv S).1 = 0 ∧ α₂ (quadSolToSolInv S).1 = 0 then
    special (quadSolToSolInv S).1 (quadSolToSolInv S).2.1 (quadSolToSolInv S).2.2 ⋯ ⋯
  else (quadSolToSolInv S).2.1 • generic (quadSolToSolInv S).1) =
  Snegn:ℕS:(PlusU1 n).Solsh:¬α₁ S.toQuadSols = 0⊢ (quadSolToSolInv S).2.1 • generic (quadSolToSolInv S).1 = S dif_neg (quadSolToSolInv_α₁_α₂_ne_zero S h)negn:ℕS:(PlusU1 n).Solsh:¬α₁ S.toQuadSols = 0⊢ (quadSolToSolInv S).2.1 • generic (quadSolToSolInv S).1 = Snegn:ℕS:(PlusU1 n).Solsh:¬α₁ S.toQuadSols = 0⊢ (quadSolToSolInv S).2.1 • generic (quadSolToSolInv S).1 = S]negn:ℕS:(PlusU1 n).Solsh:¬α₁ S.toQuadSols = 0⊢ (quadSolToSolInv S).2.1 • generic (quadSolToSolInv S).1 = S
    exact quadSolToSolInv_generic S hAll goals completed! 🐙theorem quadSolToSol_surjective : Function.Surjective (@quadSolToSol n) :=
  Function.RightInverse.surjective quadSolToSolInv_rightInverse