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.SuperSymmetry.MSSMNu.AnomalyCancellation.OrthogY3B3.PlaneWithY3B3
From charges perpendicular to Y₃ and B₃ to solutions
The main aim of this file is to take charge assignments perpendicular to Y₃ and B₃ and
produce solutions to the anomaly cancellation conditions. In this regard we will define
a surjective map toSol from MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ to MSSMACC.Sols.
To define toSols we define a series of other maps from various subtypes of
MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ to MSSMACC.Sols. And show that these maps form a
surjection on certain subtypes of MSSMACC.Sols.
References
The main reference for the material in this file is:
https://arxiv.org/pdf/2107.07926.pdf
@[expose] public sectionA condition for the quad line in the plane spanned by R, Y₃ and B₃ to sit in the cubic, and for the cube line to sit in the quad.
def LineEqProp (R : MSSMACC.AnomalyFreePerp) : Prop := α₁ R = 0 ∧ α₂ R = 0 ∧ α₃ R = 0
The proposition LineEqProp is decidable.
instance (R : MSSMACC.AnomalyFreePerp) : Decidable (LineEqProp R) := instDecidableAnd
A condition on Sols which we will show in linEqPropSol_iff_proj_linEqProp that is equivalent
to the condition that the proj of the solution satisfies lineEqProp.
def LineEqPropSol (R : MSSMACC.Sols) : Prop :=
cubeTriLin R.val R.val Y₃.val * quadBiLin B₃.val R.val -
cubeTriLin R.val R.val B₃.val * quadBiLin Y₃.val R.val = 0
A rational which appears in toSolNS acting on sols, and which being zero is
equivalent to satisfying lineEqPropSol.
T:MSSMACC.Sols⊢ ((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val =
0 ↔
1259712 *
(((cubeTriLin T.val) T.val) Y₃.val * (quadBiLin B₃.val) T.val -
((cubeTriLin T.val) T.val) B₃.val * (quadBiLin Y₃.val) T.val) =
0
All goals completed! 🐙R:MSSMACC.Solsh:α₁ (proj R.toLinSols) = 0 ∧ α₂ (proj R.toLinSols) = 0 ∧ α₃ (proj R.toLinSols) = 0⊢ (dot Y₃.val) B₃.val * 0 = 0
All goals completed! 🐙
A condition which is satisfied if the plane spanned by R, Y₃ and B₃ lies
entirely in the quadratic surface.
def InQuadProp (R : MSSMACC.AnomalyFreePerp) : Prop :=
quadBiLin R.val R.val = 0 ∧ quadBiLin Y₃.val R.val = 0 ∧ quadBiLin B₃.val R.val = 0
The proposition InQuadProp is decidable.
instance (R : MSSMACC.AnomalyFreePerp) : Decidable (InQuadProp R) := instDecidableAnd
A condition which is satisfied if the plane spanned by the solutions R, Y₃ and B₃
lies entirely in the quadratic surface.
def InQuadSolProp (R : MSSMACC.Sols) : Prop :=
quadBiLin Y₃.val R.val = 0 ∧ quadBiLin B₃.val R.val = 0
A rational which has two properties. It is zero for a solution T if and only if
that solution satisfies inQuadSolProp. It appears in the definition of inQuadProj.
def quadCoeff (T : MSSMACC.Sols) : ℚ :=
2 * dot Y₃.val B₃.val ^ 2 *
(quadBiLin Y₃.val T.val ^ 2 + quadBiLin B₃.val T.val ^ 2)T:MSSMACC.Solsh:2 * 108 ^ 2 * ((quadBiLin Y₃.val) T.val ^ 2 + (quadBiLin B₃.val) T.val ^ 2) = 0⊢ InQuadSolProp T
T:MSSMACC.Solsh:(quadBiLin Y₃.val) T.val ^ 2 + (quadBiLin B₃.val) T.val ^ 2 = 0⊢ InQuadSolProp T
T:MSSMACC.Solsh:(quadBiLin Y₃.val) T.val ^ 2 = 0 ∧ (quadBiLin B₃.val) T.val ^ 2 = 0⊢ InQuadSolProp T
T:MSSMACC.Solsh:(quadBiLin Y₃.val) T.val = 0 ∧ (quadBiLin B₃.val) T.val = 0⊢ InQuadSolProp T
All goals completed! 🐙
The conditions inQuadSolProp R and inQuadProp (proj R.1.1) are equivalent. This is to be
expected since both R and proj R.1.1 define the same plane with Y₃ and B₃.
R:MSSMACC.Solsh:((dot B₃.val) R.val - (dot Y₃.val) R.val) * (quadBiLin Y₃.val) R.val +
((dot Y₃.val) R.val - 2 * (dot B₃.val) R.val) * (quadBiLin B₃.val) R.val =
0 ∧
(quadBiLin Y₃.val) R.val = 0 ∧ (quadBiLin B₃.val) R.val = 0⊢ 0 = 0 ∧ 0 = 0
All goals completed! 🐙
A condition which is satisfied if the plane spanned by R, Y₃ and B₃ lies
entirely in the cubic surface.
def InCubeProp (R : MSSMACC.AnomalyFreePerp) : Prop :=
cubeTriLin R.val R.val R.val = 0 ∧ cubeTriLin R.val R.val B₃.val = 0 ∧
cubeTriLin R.val R.val Y₃.val = 0
The proposition InCubeProp is decidable.
instance (R : MSSMACC.AnomalyFreePerp) : Decidable (InCubeProp R) := instDecidableAnd
A condition which is satisfied if the plane spanned by the solutions R, Y₃ and B₃
lies entirely in the cubic surface.
def InCubeSolProp (R : MSSMACC.Sols) : Prop :=
cubeTriLin R.val R.val B₃.val = 0 ∧ cubeTriLin R.val R.val Y₃.val = 0
A rational which has two properties. It is zero for a solution T if and only if
that solution satisfies inCubeSolProp. It appears in the definition of inLineEqProj.
def cubicCoeff (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)T:MSSMACC.Solsh:3 * 108 ^ 3 * (((cubeTriLin T.val) T.val) Y₃.val ^ 2 + ((cubeTriLin T.val) T.val) B₃.val ^ 2) = 0⊢ InCubeSolProp T
T:MSSMACC.Solsh:((cubeTriLin T.val) T.val) Y₃.val ^ 2 + ((cubeTriLin T.val) T.val) B₃.val ^ 2 = 0⊢ InCubeSolProp T
T:MSSMACC.Solsh:((cubeTriLin T.val) T.val) Y₃.val ^ 2 = 0 ∧ ((cubeTriLin T.val) T.val) B₃.val ^ 2 = 0⊢ InCubeSolProp T
T:MSSMACC.Solsh:((cubeTriLin T.val) T.val) Y₃.val = 0 ∧ ((cubeTriLin T.val) T.val) B₃.val = 0⊢ InCubeSolProp T
All goals completed! 🐙R:MSSMACC.Solsh:((dot B₃.val) R.val - (dot Y₃.val) R.val) * ((cubeTriLin R.val) R.val) Y₃.val +
((dot Y₃.val) R.val - 2 * (dot B₃.val) R.val) * ((cubeTriLin R.val) R.val) B₃.val =
0 ∧
((cubeTriLin R.val) R.val) B₃.val = 0 ∧ ((cubeTriLin R.val) R.val) Y₃.val = 0⊢ 0 = 0 ∧ 0 = 0
All goals completed! 🐙
Those charge assignments perpendicular to Y₃ and B₃ which satisfy the condition
lineEqProp.
def InLineEq : Type := {R : MSSMACC.AnomalyFreePerp // LineEqProp R}
Those charge assignments perpendicular to Y₃ and B₃ which satisfy the conditions
lineEqProp and inQuadProp.
def InQuad : Type := {R : InLineEq // InQuadProp R.val}
Those charge assignments perpendicular to Y₃ and B₃ which satisfy the conditions
lineEqProp, inQuadProp and inCubeProp.
def InQuadCube : Type := {R : InQuad // InCubeProp R.val.val}
Those solutions which do not satisfy the condition lineEqPropSol.
def NotInLineEqSol : Type := {R : MSSMACC.Sols // ¬ LineEqPropSol R}
Those solutions which satisfy the condition lineEqPropSol but not inQuadSolProp.
def InLineEqSol : Type := {R : MSSMACC.Sols // LineEqPropSol R ∧ ¬ InQuadSolProp R}
Those solutions which satisfy the condition lineEqPropSol and inQuadSolProp but
not inCubeSolProp.
def InQuadSol : Type := {R : MSSMACC.Sols // LineEqPropSol R ∧ InQuadSolProp R ∧ ¬ InCubeSolProp R}
Those solutions which satisfy the conditions lineEqPropSol, inQuadSolProp
and inCubeSolProp.
def InQuadCubeSol : Type :=
{R : MSSMACC.Sols // LineEqPropSol R ∧ InQuadSolProp R ∧ InCubeSolProp R}
Given an R perpendicular to Y₃ and B₃ a quadratic solution.
def toSolNSQuad (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)R:AnomalyFreePerp⊢ (2 * (3 * ((cubeTriLin R.val) R.val) Y₃.val) * (quadBiLin B₃.val) R.val -
2 * (3 * ((cubeTriLin R.val) R.val) B₃.val) * (quadBiLin Y₃.val) R.val) ^
2 *
(3 *
(3 * ((cubeTriLin R.val) R.val) B₃.val * (quadBiLin R.val) R.val -
2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin B₃.val) R.val) *
((cubeTriLin R.val) R.val) Y₃.val +
3 *
(2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin Y₃.val) R.val -
3 * ((cubeTriLin R.val) R.val) Y₃.val * (quadBiLin R.val) R.val) *
((cubeTriLin R.val) R.val) B₃.val +
(2 * (3 * ((cubeTriLin R.val) R.val) Y₃.val) * (quadBiLin B₃.val) R.val -
2 * (3 * ((cubeTriLin R.val) R.val) B₃.val) * (quadBiLin Y₃.val) R.val) *
((cubeTriLin R.val) R.val) R.val) =
0
All goals completed! 🐙R:AnomalyFreePerp⊢ 3 * ((cubeTriLin R.val) R.val) B₃.val * (quadBiLin R.val) R.val -
2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin B₃.val) R.val =
3 * ((cubeTriLin R.val) R.val) B₃.val * (quadBiLin R.val) R.val -
2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin B₃.val) R.val ∧
2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin Y₃.val) R.val -
3 * ((cubeTriLin R.val) R.val) Y₃.val * (quadBiLin R.val) R.val =
2 * ((cubeTriLin R.val) R.val) R.val * (quadBiLin Y₃.val) R.val -
3 * ((cubeTriLin R.val) R.val) Y₃.val * (quadBiLin R.val) R.val ∧
2 * (3 * ((cubeTriLin R.val) R.val) Y₃.val) * (quadBiLin B₃.val) R.val -
2 * (3 * ((cubeTriLin R.val) R.val) B₃.val) * (quadBiLin Y₃.val) R.val =
6 *
(((cubeTriLin R.val) R.val) Y₃.val * (quadBiLin B₃.val) R.val -
((cubeTriLin R.val) R.val) B₃.val * (quadBiLin Y₃.val) R.val)
R:AnomalyFreePerp⊢ True ∧ True ∧ True
All goals completed! 🐙
Given an R perpendicular to Y₃ and B₃, an element of Sols. This map is
not surjective.
def toSolNS : MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, a, _, _) =>
a • AnomalyFreeMk'' (toSolNSQuad R) (toSolNSQuad_cube R)
A map from Sols to MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ which on elements of
notInLineEqSol will produce a right inverse to toSolNS.
def toSolNSProj (T : MSSMACC.Sols) : MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ :=
(proj T.1.1, (lineEqCoeff T)⁻¹, 0, 0)T:NotInLineEqSolh1✝:α₃ (proj (↑T).toLinSols) * (dot Y₃.val) B₃.val = lineEqCoeff ↑Th1:¬lineEqCoeff ↑T = 0⊢ 1 • (↑T).val = (↑T).val
All goals completed! 🐙
A solution to the ACCs, given an element of inLineEq × ℚ × ℚ × ℚ.
x✝:InLineEq × ℚ × ℚ × ℚR:InLineEqc₁:ℚc₂:ℚc₃:ℚ⊢ -4 * (c₁ * (quadBiLin B₃.val) (↑R).val - c₂ * (quadBiLin Y₃.val) (↑R).val) ^ 2 * (0 * c₁ + 0 * c₂ + 0 * c₃) = 0
All goals completed! 🐙)
On elements of inLineEqSol a right-inverse to inLineEqSol.
def inLineEqProj (T : InLineEqSol) : InLineEq × ℚ × ℚ × ℚ :=
(⟨proj T.val.1.1, (linEqPropSol_iff_proj_linEqProp T.val).mp T.prop.1⟩,
(quadCoeff T.val)⁻¹ * quadBiLin B₃.val T.val.val,
(quadCoeff T.val)⁻¹ * (- quadBiLin Y₃.val T.val.val),
(quadCoeff T.val)⁻¹ *
(quadBiLin B₃.val T.val.val * (dot B₃.val T.val.val - dot Y₃.val T.val.val)
- quadBiLin Y₃.val T.val.val * (dot Y₃.val T.val.val - 2 * dot B₃.val T.val.val)))R:InLineEqc₁:ℚc₂:ℚc₃:ℚd:ℚ⊢ (d • lineQuad (↑R) c₁ c₂ c₃).val = (d • inLineEqToSol (R, c₁, c₂, c₃)).val
All goals completed! 🐙T:InLineEqSolh1:(quadBiLin Y₃.val) (↑T).val ^ 2 * (dot Y₃.val) B₃.val ^ 2 * 2 +
(dot Y₃.val) B₃.val ^ 2 * (quadBiLin B₃.val) (↑T).val ^ 2 * 2 =
quadCoeff ↑Th2:¬quadCoeff ↑T = 0⊢ 1 • (↑T).val = (↑T).val
All goals completed! 🐙
Given an element of inQuad × ℚ × ℚ × ℚ, a solution to the ACCs.
x✝:InQuad × ℚ × ℚ × ℚR:InQuada₁:ℚa₂:ℚa₃:ℚ⊢ 3 * (a₁ * ((cubeTriLin (↑↑R).val) (↑↑R).val) B₃.val - a₂ * ((cubeTriLin (↑↑R).val) (↑↑R).val) Y₃.val) *
(2 * (a₂ * ((cubeTriLin (↑↑R).val) (↑↑R).val) (↑↑R).val - 3 * a₃ * ((cubeTriLin (↑↑R).val) (↑↑R).val) B₃.val) * 0 +
2 * (3 * a₃ * ((cubeTriLin (↑↑R).val) (↑↑R).val) Y₃.val - a₁ * ((cubeTriLin (↑↑R).val) (↑↑R).val) (↑↑R).val) *
0 +
3 * (a₁ * ((cubeTriLin (↑↑R).val) (↑↑R).val) B₃.val - a₂ * ((cubeTriLin (↑↑R).val) (↑↑R).val) Y₃.val) * 0) =
0; All goals completed! 🐙)
(lineCube_cube R.val.val a₁ a₂ a₃)R:InQuadc₁:ℚc₂:ℚc₃:ℚd:ℚ⊢ (d • lineCube (↑↑R) c₁ c₂ c₃).val = (d • inQuadToSol (R, c₁, c₂, c₃)).val
All goals completed! 🐙
On elements of inQuadSol a right-inverse to inQuadToSol.
def inQuadProj (T : InQuadSol) : InQuad × ℚ × ℚ × ℚ :=
(⟨⟨proj T.val.1.1, (linEqPropSol_iff_proj_linEqProp T.val).mp T.prop.1⟩,
(inQuadSolProp_iff_proj_inQuadProp T.val).mp T.prop.2.1⟩,
(cubicCoeff T.val)⁻¹ * (cubeTriLin T.val.val T.val.val B₃.val),
(cubicCoeff T.val)⁻¹ * (- cubeTriLin T.val.val T.val.val Y₃.val),
(cubicCoeff T.val)⁻¹ *
(cubeTriLin T.val.val T.val.val B₃.val * (dot B₃.val T.val.val - dot Y₃.val T.val.val)
- cubeTriLin T.val.val T.val.val Y₃.val
* (dot Y₃.val T.val.val - 2 * dot B₃.val T.val.val)))T:InQuadSolh1:((cubeTriLin (↑T).val) (↑T).val) Y₃.val ^ 2 * (dot Y₃.val) B₃.val ^ 3 * 3 +
(dot Y₃.val) B₃.val ^ 3 * ((cubeTriLin (↑T).val) (↑T).val) B₃.val ^ 2 * 3 =
cubicCoeff ↑Th2:¬cubicCoeff ↑T = 0⊢ 1 • (↑T).val = (↑T).val
All goals completed! 🐙
Given a element of inQuadCube × ℚ × ℚ × ℚ, a solution to the ACCs.
x✝:InQuadCube × ℚ × ℚ × ℚR:InQuadCubeb₁:ℚb₂:ℚb₃:ℚ⊢ b₃ ^ 2 * (3 * b₁ * 0 + 3 * b₂ * 0 + b₃ * 0) = 0; All goals completed! 🐙)R:InQuadCubec₁:ℚc₂:ℚc₃:ℚd:ℚ⊢ (d • planeY₃B₃ (↑↑↑R) c₁ c₂ c₃).val = (d • inQuadCubeToSol (R, c₁, c₂, c₃)).val
All goals completed! 🐙
On elements of inQuadCubeSol a right-inverse to inQuadCubeToSol.
def inQuadCubeProj (T : InQuadCubeSol) : InQuadCube × ℚ × ℚ × ℚ :=
(⟨⟨⟨proj T.val.1.1, (linEqPropSol_iff_proj_linEqProp T.val).mp T.prop.1⟩,
(inQuadSolProp_iff_proj_inQuadProp T.val).mp T.prop.2.1⟩,
(inCubeSolProp_iff_proj_inCubeProp T.val).mp T.prop.2.2⟩,
(dot Y₃.val B₃.val)⁻¹ * (dot Y₃.val T.val.val - dot B₃.val T.val.val),
(dot Y₃.val B₃.val)⁻¹ * (2 * dot B₃.val T.val.val - dot Y₃.val T.val.val),
(dot Y₃.val B₃.val)⁻¹ * 1)T:InQuadCubeSol⊢ 108 ≠ 0
All goals completed! 🐙
A solution from an element of MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ. We will
show that this map is a surjection.
def toSol : MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ → MSSMACC.Sols := fun (R, a, b, c) =>
if h₃ : LineEqProp R ∧ InQuadProp R ∧ InCubeProp R then
inQuadCubeToSol (⟨⟨⟨R, h₃.1⟩, h₃.2.1⟩, h₃.2.2⟩, a, b, c)
else
if h₂ : LineEqProp R ∧ InQuadProp R then
inQuadToSol (⟨⟨R, h₂.1⟩, h₂.2⟩, a, b, c)
else
if h₁ : LineEqProp R then
inLineEqToSol (⟨R, h₁⟩, a, b, c)
else
toSolNS ⟨R, a, b, c⟩lemma toSol_toSolNSProj (T : NotInLineEqSol) :
∃ X, toSol X = T.val := T:NotInLineEqSol⊢ ∃ X, toSol X = ↑T
T:NotInLineEqSol⊢ toSol (toSolNSProj ↑T) = ↑T
T:NotInLineEqSolh1:¬(toSolNSProj ↑T).1.LineEqProp⊢ toSol (toSolNSProj ↑T) = ↑T
simp_rw T:NotInLineEqSolh1:¬(toSolNSProj ↑T).1.LineEqProp⊢ toSol (toSolNSProj ↑T) = ↑TT:NotInLineEqSolh1:¬(toSolNSProj ↑T).1.LineEqProp⊢ (if h₃ : (toSolNSProj ↑T).1.LineEqProp ∧ (toSolNSProj ↑T).1.InQuadProp ∧ (toSolNSProj ↑T).1.InCubeProp then
inQuadCubeToSol
(⟨⟨⟨(toSolNSProj ↑T).1, ⋯⟩, ⋯⟩, ⋯⟩, (toSolNSProj ↑T).2.1, (toSolNSProj ↑T).2.2.1, (toSolNSProj ↑T).2.2.2)
else
if h₂ : (toSolNSProj ↑T).1.LineEqProp ∧ (toSolNSProj ↑T).1.InQuadProp then
inQuadToSol (⟨⟨(toSolNSProj ↑T).1, ⋯⟩, ⋯⟩, (toSolNSProj ↑T).2.1, (toSolNSProj ↑T).2.2.1, (toSolNSProj ↑T).2.2.2)
else
if h₁ : (toSolNSProj ↑T).1.LineEqProp then
inLineEqToSol (⟨(toSolNSProj ↑T).1, h₁⟩, (toSolNSProj ↑T).2.1, (toSolNSProj ↑T).2.2.1, (toSolNSProj ↑T).2.2.2)
else toSolNS ((toSolNSProj ↑T).1, (toSolNSProj ↑T).2.1, (toSolNSProj ↑T).2.2.1, (toSolNSProj ↑T).2.2.2)) =
↑T T:NotInLineEqSolh1:¬(toSolNSProj ↑T).1.LineEqProp⊢ (if h : False ∧ (toSolNSProj ↑T).1.InQuadProp ∧ (toSolNSProj ↑T).1.InCubeProp then
inQuadCubeToSol
(⟨⟨⟨(toSolNSProj ↑T).1, ⋯⟩, ⋯⟩, ⋯⟩, (toSolNSProj ↑T).2.1, (toSolNSProj ↑T).2.2.1, (toSolNSProj ↑T).2.2.2)
else
if h : False ∧ (toSolNSProj ↑T).1.InQuadProp then
inQuadToSol (⟨⟨(toSolNSProj ↑T).1, ⋯⟩, ⋯⟩, (toSolNSProj ↑T).2.1, (toSolNSProj ↑T).2.2.1, (toSolNSProj ↑T).2.2.2)
else
if h : False then
inLineEqToSol (⟨(toSolNSProj ↑T).1, ⋯⟩, (toSolNSProj ↑T).2.1, (toSolNSProj ↑T).2.2.1, (toSolNSProj ↑T).2.2.2)
else toSolNS ((toSolNSProj ↑T).1, (toSolNSProj ↑T).2.1, (toSolNSProj ↑T).2.2.1, (toSolNSProj ↑T).2.2.2)) =
↑T]
All goals completed! 🐙lemma toSol_inLineEq (T : InLineEqSol) : ∃ X, toSol X = T.val := T:InLineEqSol⊢ ∃ X, toSol X = ↑T
T:InLineEqSolX:InLineEq × ℚ × ℚ × ℚ := inLineEqProj T⊢ ∃ X, toSol X = ↑T
T:InLineEqSolX:InLineEq × ℚ × ℚ × ℚ := inLineEqProj T⊢ toSol (↑X.1, X.2.1, X.2.2) = ↑T
T:InLineEqSolX:InLineEq × ℚ × ℚ × ℚ := inLineEqProj Tthis:¬(↑X.1).InQuadProp⊢ toSol (↑X.1, X.2.1, X.2.2) = ↑T
T:InLineEqSolX:InLineEq × ℚ × ℚ × ℚ := inLineEqProj Tthis✝:¬(↑X.1).InQuadPropthis:(↑X.1).LineEqProp⊢ toSol (↑X.1, X.2.1, X.2.2) = ↑T
T:InLineEqSolX:InLineEq × ℚ × ℚ × ℚ := inLineEqProj Tthis✝:¬(↑X.1).InQuadPropthis:(↑X.1).LineEqProp⊢ (if h : True ∧ False ∧ (↑X.1).InCubeProp then inQuadCubeToSol (⟨⟨⟨↑X.1, ⋯⟩, ⋯⟩, ⋯⟩, X.2.1, X.2.2.1, X.2.2.2)
else
if h : True ∧ False then inQuadToSol (⟨⟨↑X.1, ⋯⟩, ⋯⟩, X.2.1, X.2.2.1, X.2.2.2)
else
if h : True then inLineEqToSol (⟨↑X.1, ⋯⟩, X.2.1, X.2.2.1, X.2.2.2)
else toSolNS (↑X.1, X.2.1, X.2.2.1, X.2.2.2)) =
↑T
All goals completed! 🐙lemma toSol_inQuad (T : InQuadSol) : ∃ X, toSol X = T.val := T:InQuadSol⊢ ∃ X, toSol X = ↑T
T:InQuadSolX:InQuad × ℚ × ℚ × ℚ := inQuadProj T⊢ ∃ X, toSol X = ↑T
T:InQuadSolX:InQuad × ℚ × ℚ × ℚ := inQuadProj T⊢ toSol (↑↑X.1, X.2.1, X.2.2) = ↑T
T:InQuadSolX:InQuad × ℚ × ℚ × ℚ := inQuadProj Tthis:¬(↑↑X.1).InCubeProp⊢ toSol (↑↑X.1, X.2.1, X.2.2) = ↑T
T:InQuadSolX:InQuad × ℚ × ℚ × ℚ := inQuadProj Tthis✝:¬(↑↑X.1).InCubePropthis:(↑↑X.1).InQuadProp⊢ toSol (↑↑X.1, X.2.1, X.2.2) = ↑T
T:InQuadSolX:InQuad × ℚ × ℚ × ℚ := inQuadProj Tthis✝¹:¬(↑↑X.1).InCubePropthis✝:(↑↑X.1).InQuadPropthis:(↑↑X.1).LineEqProp⊢ toSol (↑↑X.1, X.2.1, X.2.2) = ↑T
T:InQuadSolX:InQuad × ℚ × ℚ × ℚ := inQuadProj Tthis✝¹:¬(↑↑X.1).InCubePropthis✝:(↑↑X.1).InQuadPropthis:(↑↑X.1).LineEqProp⊢ (if h : True ∧ True ∧ False then inQuadCubeToSol (⟨⟨⟨↑↑X.1, ⋯⟩, ⋯⟩, ⋯⟩, X.2.1, X.2.2.1, X.2.2.2)
else
if h : True ∧ True then inQuadToSol (⟨⟨↑↑X.1, ⋯⟩, ⋯⟩, X.2.1, X.2.2.1, X.2.2.2)
else
if h : True then inLineEqToSol (⟨↑↑X.1, ⋯⟩, X.2.1, X.2.2.1, X.2.2.2)
else toSolNS (↑↑X.1, X.2.1, X.2.2.1, X.2.2.2)) =
↑T
All goals completed! 🐙lemma toSol_inQuadCube (T : InQuadCubeSol) : ∃ X, toSol X = T.val := T:InQuadCubeSol⊢ ∃ X, toSol X = ↑T
T:InQuadCubeSolX:InQuadCube × ℚ × ℚ × ℚ := inQuadCubeProj T⊢ ∃ X, toSol X = ↑T
T:InQuadCubeSolX:InQuadCube × ℚ × ℚ × ℚ := inQuadCubeProj T⊢ toSol (↑↑↑X.1, X.2.1, X.2.2) = ↑T
T:InQuadCubeSolX:InQuadCube × ℚ × ℚ × ℚ := inQuadCubeProj Tthis:(↑↑↑X.1).InCubeProp⊢ toSol (↑↑↑X.1, X.2.1, X.2.2) = ↑T
T:InQuadCubeSolX:InQuadCube × ℚ × ℚ × ℚ := inQuadCubeProj Tthis✝:(↑↑↑X.1).InCubePropthis:(↑↑↑X.1).InQuadProp⊢ toSol (↑↑↑X.1, X.2.1, X.2.2) = ↑T
T:InQuadCubeSolX:InQuadCube × ℚ × ℚ × ℚ := inQuadCubeProj Tthis✝¹:(↑↑↑X.1).InCubePropthis✝:(↑↑↑X.1).InQuadPropthis:(↑↑↑X.1).LineEqProp⊢ toSol (↑↑↑X.1, X.2.1, X.2.2) = ↑T
T:InQuadCubeSolX:InQuadCube × ℚ × ℚ × ℚ := inQuadCubeProj Tthis✝¹:(↑↑↑X.1).InCubePropthis✝:(↑↑↑X.1).InQuadPropthis:(↑↑↑X.1).LineEqProp⊢ (if h : True ∧ True ∧ True then inQuadCubeToSol (⟨⟨⟨↑↑↑X.1, ⋯⟩, ⋯⟩, ⋯⟩, X.2.1, X.2.2.1, X.2.2.2)
else
if h : True ∧ True then inQuadToSol (⟨⟨↑↑↑X.1, ⋯⟩, ⋯⟩, X.2.1, X.2.2.1, X.2.2.2)
else
if h : True then inLineEqToSol (⟨↑↑↑X.1, ⋯⟩, X.2.1, X.2.2.1, X.2.2.2)
else toSolNS (↑↑↑X.1, X.2.1, X.2.2.1, X.2.2.2)) =
↑T
All goals completed! 🐙theorem toSol_surjective : Function.Surjective toSol := ⊢ Function.Surjective toSol
T:MSSMACC.Sols⊢ ∃ a, toSol a = T
T:MSSMACC.Solsh₁:¬LineEqPropSol T⊢ ∃ a, toSol a = TT:MSSMACC.Solsh₁:¬¬LineEqPropSol T⊢ ∃ a, toSol a = T
T:MSSMACC.Solsh₁:¬LineEqPropSol T⊢ ∃ a, toSol a = T All goals completed! 🐙
T:MSSMACC.Solsh₁:¬¬LineEqPropSol T⊢ ∃ a, toSol a = T T:MSSMACC.Solsh₁:LineEqPropSol T⊢ ∃ a, toSol a = T
T:MSSMACC.Solsh₁:LineEqPropSol Th₂:¬InQuadSolProp T⊢ ∃ a, toSol a = TT:MSSMACC.Solsh₁:LineEqPropSol Th₂:¬¬InQuadSolProp T⊢ ∃ a, toSol a = T
T:MSSMACC.Solsh₁:LineEqPropSol Th₂:¬InQuadSolProp T⊢ ∃ a, toSol a = T All goals completed! 🐙
T:MSSMACC.Solsh₁:LineEqPropSol Th₂:¬¬InQuadSolProp T⊢ ∃ a, toSol a = T T:MSSMACC.Solsh₁:LineEqPropSol Th₂:InQuadSolProp T⊢ ∃ a, toSol a = T
T:MSSMACC.Solsh₁:LineEqPropSol Th₂:InQuadSolProp Th₃:¬InCubeSolProp T⊢ ∃ a, toSol a = TT:MSSMACC.Solsh₁:LineEqPropSol Th₂:InQuadSolProp Th₃:¬¬InCubeSolProp T⊢ ∃ a, toSol a = T
T:MSSMACC.Solsh₁:LineEqPropSol Th₂:InQuadSolProp Th₃:¬InCubeSolProp T⊢ ∃ a, toSol a = T All goals completed! 🐙
T:MSSMACC.Solsh₁:LineEqPropSol Th₂:InQuadSolProp Th₃:¬¬InCubeSolProp T⊢ ∃ a, toSol a = T T:MSSMACC.Solsh₁:LineEqPropSol Th₂:InQuadSolProp Th₃:InCubeSolProp T⊢ ∃ a, toSol a = T
All goals completed! 🐙