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

theorem SMRHN.PlusU1.QuadSol.add_AFL_quad {n : ℕ} (C : (PlusU1 n).QuadSols) (S : (PlusU1 n).LinSols) (a b : ℚ) : SMνACCs.accQuad (a • S.val + b • C.val) = a * (a * SMνACCs.accQuad S.val + 2 * b * (SMνACCs.quadBiLin S.val) C.val)

def SMRHN.PlusU1.QuadSol.α₁ {n : ℕ} (C : (PlusU1 n).QuadSols) (S : (PlusU1 n).LinSols) : ℚ

A helper function for what comes later.

def SMRHN.PlusU1.QuadSol.α₂ {n : ℕ} (S : (PlusU1 n).LinSols) : ℚ

A helper function for what comes later.

theorem SMRHN.PlusU1.QuadSol.α₂_AFQ {n : ℕ} (S : (PlusU1 n).QuadSols) : α₂ S.toLinSols = 0

theorem SMRHN.PlusU1.QuadSol.accQuad_α₁_α₂ {n : ℕ} (C : (PlusU1 n).QuadSols) (S : (PlusU1 n).LinSols) : SMνACCs.accQuad (α₁ C S • S + α₂ S • C.toLinSols).val = 0

theorem SMRHN.PlusU1.QuadSol.accQuad_α₁_α₂_zero {n : ℕ} (C : (PlusU1 n).QuadSols) (S : (PlusU1 n).LinSols) (h1 : α₁ C S = 0) (h2 : α₂ S = 0) (a b : ℚ) : SMνACCs.accQuad (a • S + b • C.toLinSols).val = 0

def SMRHN.PlusU1.QuadSol.genericToQuad {n : ℕ} (C : (PlusU1 n).QuadSols) (S : (PlusU1 n).LinSols) : (PlusU1 n).QuadSols

The construction of a QuadSol from a LinSols in the generic case.

theorem SMRHN.PlusU1.QuadSol.genericToQuad_on_quad {n : ℕ} (C S : (PlusU1 n).QuadSols) : genericToQuad C S.toLinSols = α₁ C S.toLinSols • S

theorem SMRHN.PlusU1.QuadSol.genericToQuad_neq_zero {n : ℕ} (C S : (PlusU1 n).QuadSols) (h : α₁ C S.toLinSols ≠ 0) : (α₁ C S.toLinSols)⁻¹ • genericToQuad C S.toLinSols = S

def SMRHN.PlusU1.QuadSol.specialToQuad {n : ℕ} (C : (PlusU1 n).QuadSols) (S : (PlusU1 n).LinSols) (a b : ℚ) (h1 : α₁ C S = 0) (h2 : α₂ S = 0) : (PlusU1 n).QuadSols

The construction of a QuadSol from a LinSols in the special case when α₁ C S = 0 and α₂ S = 0.

theorem SMRHN.PlusU1.QuadSol.special_on_quad {n : ℕ} (C S : (PlusU1 n).QuadSols) (h1 : α₁ C S.toLinSols = 0) : specialToQuad C S.toLinSols 1 0 h1 ⋯ = S

def SMRHN.PlusU1.QuadSol.toQuad {n : ℕ} (C : (PlusU1 n).QuadSols) : (PlusU1 n).LinSols × ℚ × ℚ → (PlusU1 n).QuadSols

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 SMRHN.PlusU1.QuadSol.toQuadInv {n : ℕ} (C : (PlusU1 n).QuadSols) : (PlusU1 n).QuadSols → (PlusU1 n).LinSols × ℚ × ℚ

A function from QuadSols to LinSols × ℚ × ℚ which is a right inverse to toQuad.

theorem SMRHN.PlusU1.QuadSol.toQuadInv_fst {n : ℕ} (C S : (PlusU1 n).QuadSols) : (toQuadInv C S).1 = S.toLinSols

theorem SMRHN.PlusU1.QuadSol.toQuadInv_α₁_α₂ {n : ℕ} (C S : (PlusU1 n).QuadSols) : α₁ C S.toLinSols = 0 ↔ α₁ C (toQuadInv C S).1 = 0 ∧ α₂ (toQuadInv C S).1 = 0

theorem SMRHN.PlusU1.QuadSol.toQuadInv_special {n : ℕ} (C S : (PlusU1 n).QuadSols) (h : α₁ C S.toLinSols = 0) : specialToQuad C (toQuadInv C S).1 (toQuadInv C S).2.1 (toQuadInv C S).2.2 ⋯ ⋯ = S

theorem SMRHN.PlusU1.QuadSol.toQuadInv_generic {n : ℕ} (C S : (PlusU1 n).QuadSols) (h : α₁ C S.toLinSols ≠ 0) : (toQuadInv C S).2.1 • genericToQuad C (toQuadInv C S).1 = S

theorem SMRHN.PlusU1.QuadSol.toQuad_rightInverse {n : ℕ} (C : (PlusU1 n).QuadSols) : Function.RightInverse (toQuadInv C) (toQuad C)

theorem SMRHN.PlusU1.QuadSol.toQuad_surjective {n : ℕ} (C : (PlusU1 n).QuadSols) : Function.Surjective (toQuad C)