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

def MSSMACC.AnomalyFreePerp.LineEqProp (R : AnomalyFreePerp) : Prop

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

Equations

• R.LineEqProp = (MSSMACC.α₁ R = 0 ∧ MSSMACC.α₂ R = 0 ∧ MSSMACC.α₃ R = 0)

instance MSSMACC.AnomalyFreePerp.instDecidableLineEqProp (R : AnomalyFreePerp) : Decidable R.LineEqProp

The proposition LineEqProp is decidable.

Equations

• R.instDecidableLineEqProp = instDecidableAnd

def MSSMACC.AnomalyFreePerp.LineEqPropSol (R : MSSMACC.Sols) : Prop

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.

Equations

• One or more equations did not get rendered due to their size.

def MSSMACC.AnomalyFreePerp.lineEqCoeff (T : MSSMACC.Sols) : ℚ

A rational which appears in toSolNS acting on sols, and which being zero is equivalent to satisfying lineEqPropSol.

Equations

• MSSMACC.AnomalyFreePerp.lineEqCoeff T = (MSSMACC.dot MSSMACC.Y₃.val) MSSMACC.B₃.val * MSSMACC.α₃ (MSSMACC.proj T.toLinSols)

theorem MSSMACC.AnomalyFreePerp.lineEqPropSol_iff_lineEqCoeff_zero (T : MSSMACC.Sols) : LineEqPropSol T ↔ lineEqCoeff T = 0

theorem MSSMACC.AnomalyFreePerp.linEqPropSol_iff_proj_linEqProp (R : MSSMACC.Sols) : LineEqPropSol R ↔ (proj R.toLinSols).LineEqProp

def MSSMACC.AnomalyFreePerp.InQuadProp (R : AnomalyFreePerp) : Prop

A condition which is satisfied if the plane spanned by R, Y₃ and B₃ lies entirely in the quadratic surface.

Equations

• R.InQuadProp = ((MSSMACCs.quadBiLin R.val) R.val = 0 ∧ (MSSMACCs.quadBiLin MSSMACC.Y₃.val) R.val = 0 ∧ (MSSMACCs.quadBiLin MSSMACC.B₃.val) R.val = 0)

instance MSSMACC.AnomalyFreePerp.instDecidableInQuadProp (R : AnomalyFreePerp) : Decidable R.InQuadProp

The proposition InQuadProp is decidable.

Equations

• R.instDecidableInQuadProp = instDecidableAnd

def MSSMACC.AnomalyFreePerp.InQuadSolProp (R : MSSMACC.Sols) : Prop

A condition which is satisfied if the plane spanned by the solutions R, Y₃ and B₃ lies entirely in the quadratic surface.

Equations

• MSSMACC.AnomalyFreePerp.InQuadSolProp R = ((MSSMACCs.quadBiLin MSSMACC.Y₃.val) R.val = 0 ∧ (MSSMACCs.quadBiLin MSSMACC.B₃.val) R.val = 0)

def MSSMACC.AnomalyFreePerp.quadCoeff (T : MSSMACC.Sols) : ℚ

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.

Equations

• MSSMACC.AnomalyFreePerp.quadCoeff T = 2 * (MSSMACC.dot MSSMACC.Y₃.val) MSSMACC.B₃.val ^ 2 * ((MSSMACCs.quadBiLin MSSMACC.Y₃.val) T.val ^ 2 + (MSSMACCs.quadBiLin MSSMACC.B₃.val) T.val ^ 2)

theorem MSSMACC.AnomalyFreePerp.inQuadSolProp_iff_quadCoeff_zero (T : MSSMACC.Sols) : InQuadSolProp T ↔ quadCoeff T = 0

theorem MSSMACC.AnomalyFreePerp.inQuadSolProp_iff_proj_inQuadProp (R : MSSMACC.Sols) : InQuadSolProp R ↔ (proj R.toLinSols).InQuadProp

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

def MSSMACC.AnomalyFreePerp.InCubeProp (R : AnomalyFreePerp) : Prop

A condition which is satisfied if the plane spanned by R, Y₃ and B₃ lies entirely in the cubic surface.

Equations

• R.InCubeProp = (((MSSMACCs.cubeTriLin R.val) R.val) R.val = 0 ∧ ((MSSMACCs.cubeTriLin R.val) R.val) MSSMACC.B₃.val = 0 ∧ ((MSSMACCs.cubeTriLin R.val) R.val) MSSMACC.Y₃.val = 0)

instance MSSMACC.AnomalyFreePerp.instDecidableInCubeProp (R : AnomalyFreePerp) : Decidable R.InCubeProp

The proposition InCubeProp is decidable.

Equations

• R.instDecidableInCubeProp = instDecidableAnd

def MSSMACC.AnomalyFreePerp.InCubeSolProp (R : MSSMACC.Sols) : Prop

A condition which is satisfied if the plane spanned by the solutions R, Y₃ and B₃ lies entirely in the cubic surface.

Equations

• MSSMACC.AnomalyFreePerp.InCubeSolProp R = (((MSSMACCs.cubeTriLin R.val) R.val) MSSMACC.B₃.val = 0 ∧ ((MSSMACCs.cubeTriLin R.val) R.val) MSSMACC.Y₃.val = 0)

def MSSMACC.AnomalyFreePerp.cubicCoeff (T : MSSMACC.Sols) : ℚ

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.

Equations

• One or more equations did not get rendered due to their size.

theorem MSSMACC.AnomalyFreePerp.inCubeSolProp_iff_cubicCoeff_zero (T : MSSMACC.Sols) : InCubeSolProp T ↔ cubicCoeff T = 0

theorem MSSMACC.AnomalyFreePerp.inCubeSolProp_iff_proj_inCubeProp (R : MSSMACC.Sols) : InCubeSolProp R ↔ (proj R.toLinSols).InCubeProp

def MSSMACC.AnomalyFreePerp.InLineEq : Type

Those charge assignments perpendicular to Y₃ and B₃ which satisfy the condition lineEqProp.

Equations

• MSSMACC.AnomalyFreePerp.InLineEq = { R : MSSMACC.AnomalyFreePerp // R.LineEqProp }

def MSSMACC.AnomalyFreePerp.InQuad : Type

Those charge assignments perpendicular to Y₃ and B₃ which satisfy the conditions lineEqProp and inQuadProp.

Equations

• MSSMACC.AnomalyFreePerp.InQuad = { R : MSSMACC.AnomalyFreePerp.InLineEq // (↑R).InQuadProp }

def MSSMACC.AnomalyFreePerp.InQuadCube : Type

Those charge assignments perpendicular to Y₃ and B₃ which satisfy the conditions lineEqProp, inQuadProp and inCubeProp.

Equations

• MSSMACC.AnomalyFreePerp.InQuadCube = { R : MSSMACC.AnomalyFreePerp.InQuad // (↑↑R).InCubeProp }

def MSSMACC.AnomalyFreePerp.NotInLineEqSol : Type

Those solutions which do not satisfy the condition lineEqPropSol.

Equations

• MSSMACC.AnomalyFreePerp.NotInLineEqSol = { R : MSSMACC.Sols // ¬MSSMACC.AnomalyFreePerp.LineEqPropSol R }

def MSSMACC.AnomalyFreePerp.InLineEqSol : Type

Those solutions which satisfy the condition lineEqPropSol but not inQuadSolProp.

Equations

• MSSMACC.AnomalyFreePerp.InLineEqSol = { R : MSSMACC.Sols // MSSMACC.AnomalyFreePerp.LineEqPropSol R ∧ ¬MSSMACC.AnomalyFreePerp.InQuadSolProp R }

def MSSMACC.AnomalyFreePerp.InQuadSol : Type

Those solutions which satisfy the condition lineEqPropSol and inQuadSolProp but not inCubeSolProp.

Equations

• MSSMACC.AnomalyFreePerp.InQuadSol = { R : MSSMACC.Sols // MSSMACC.AnomalyFreePerp.LineEqPropSol R ∧ MSSMACC.AnomalyFreePerp.InQuadSolProp R ∧ ¬MSSMACC.AnomalyFreePerp.InCubeSolProp R }

def MSSMACC.AnomalyFreePerp.InQuadCubeSol : Type

Those solutions which satisfy the conditions lineEqPropSol, inQuadSolProp and inCubeSolProp.

Equations

• MSSMACC.AnomalyFreePerp.InQuadCubeSol = { R : MSSMACC.Sols // MSSMACC.AnomalyFreePerp.LineEqPropSol R ∧ MSSMACC.AnomalyFreePerp.InQuadSolProp R ∧ MSSMACC.AnomalyFreePerp.InCubeSolProp R }

def MSSMACC.AnomalyFreePerp.toSolNSQuad (R : AnomalyFreePerp) : MSSMACC.QuadSols

Given an R perpendicular to Y₃ and B₃ a quadratic solution.

Equations

• R.toSolNSQuad = MSSMACC.lineQuad R (3 * ((MSSMACCs.cubeTriLin R.val) R.val) MSSMACC.Y₃.val) (3 * ((MSSMACCs.cubeTriLin R.val) R.val) MSSMACC.B₃.val) (((MSSMACCs.cubeTriLin R.val) R.val) R.val)

theorem MSSMACC.AnomalyFreePerp.toSolNSQuad_cube (R : AnomalyFreePerp) : MSSMACCs.accCube R.toSolNSQuad.val = 0

theorem MSSMACC.AnomalyFreePerp.toSolNSQuad_eq_planeY₃B₃_on_α (R : AnomalyFreePerp) : R.toSolNSQuad.toLinSols = planeY₃B₃ R (α₁ R) (α₂ R) (α₃ R)

def MSSMACC.AnomalyFreePerp.toSolNS : AnomalyFreePerp × ℚ × ℚ × ℚ → MSSMACC.Sols

Given an R perpendicular to Y₃ and B₃, an element of Sols. This map is not surjective.

Equations

• MSSMACC.AnomalyFreePerp.toSolNS (R, a, fst, snd) = a • MSSMACC.AnomalyFreeMk'' R.toSolNSQuad ⋯

def MSSMACC.AnomalyFreePerp.toSolNSProj (T : MSSMACC.Sols) : AnomalyFreePerp × ℚ × ℚ × ℚ

A map from Sols to MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ which on elements of notInLineEqSol will produce a right inverse to toSolNS.

Equations

• MSSMACC.AnomalyFreePerp.toSolNSProj T = (MSSMACC.proj T.toLinSols, (MSSMACC.AnomalyFreePerp.lineEqCoeff T)⁻¹, 0, 0)

theorem MSSMACC.AnomalyFreePerp.toSolNS_proj (T : NotInLineEqSol) : toSolNS (toSolNSProj ↑T) = ↑T

def MSSMACC.AnomalyFreePerp.inLineEqToSol : InLineEq × ℚ × ℚ × ℚ → MSSMACC.Sols

A solution to the ACCs, given an element of inLineEq × ℚ × ℚ × ℚ.

Equations

• MSSMACC.AnomalyFreePerp.inLineEqToSol (R, c₁, c₂, c₃) = MSSMACC.AnomalyFreeMk'' (MSSMACC.lineQuad (↑R) c₁ c₂ c₃) ⋯

def MSSMACC.AnomalyFreePerp.inLineEqProj (T : InLineEqSol) : InLineEq × ℚ × ℚ × ℚ

On elements of inLineEqSol a right-inverse to inLineEqSol.

Equations

• One or more equations did not get rendered due to their size.

theorem MSSMACC.AnomalyFreePerp.inLineEqTo_smul (R : InLineEq) (c₁ c₂ c₃ d : ℚ) : inLineEqToSol (R, d * c₁, d * c₂, d * c₃) = d • inLineEqToSol (R, c₁, c₂, c₃)

theorem MSSMACC.AnomalyFreePerp.inLineEqToSol_proj (T : InLineEqSol) : inLineEqToSol (inLineEqProj T) = ↑T

def MSSMACC.AnomalyFreePerp.inQuadToSol : InQuad × ℚ × ℚ × ℚ → MSSMACC.Sols

Given an element of inQuad × ℚ × ℚ × ℚ, a solution to the ACCs.

Equations

• MSSMACC.AnomalyFreePerp.inQuadToSol (R, a₁, a₂, a₃) = MSSMACC.AnomalyFreeMk' (MSSMACC.lineCube (↑↑R) a₁ a₂ a₃) ⋯ ⋯

theorem MSSMACC.AnomalyFreePerp.inQuadToSol_smul (R : InQuad) (c₁ c₂ c₃ d : ℚ) : inQuadToSol (R, d * c₁, d * c₂, d * c₃) = d • inQuadToSol (R, c₁, c₂, c₃)

def MSSMACC.AnomalyFreePerp.inQuadProj (T : InQuadSol) : InQuad × ℚ × ℚ × ℚ

On elements of inQuadSol a right-inverse to inQuadToSol.

Equations

• One or more equations did not get rendered due to their size.

theorem MSSMACC.AnomalyFreePerp.inQuadToSol_proj (T : InQuadSol) : inQuadToSol (inQuadProj T) = ↑T

def MSSMACC.AnomalyFreePerp.inQuadCubeToSol : InQuadCube × ℚ × ℚ × ℚ → MSSMACC.Sols

Given a element of inQuadCube × ℚ × ℚ × ℚ, a solution to the ACCs.

Equations

• MSSMACC.AnomalyFreePerp.inQuadCubeToSol (R, b₁, b₂, b₃) = MSSMACC.AnomalyFreeMk' (MSSMACC.planeY₃B₃ (↑↑↑R) b₁ b₂ b₃) ⋯ ⋯

theorem MSSMACC.AnomalyFreePerp.inQuadCubeToSol_smul (R : InQuadCube) (c₁ c₂ c₃ d : ℚ) : inQuadCubeToSol (R, d * c₁, d * c₂, d * c₃) = d • inQuadCubeToSol (R, c₁, c₂, c₃)

def MSSMACC.AnomalyFreePerp.inQuadCubeProj (T : InQuadCubeSol) : InQuadCube × ℚ × ℚ × ℚ

On elements of inQuadCubeSol a right-inverse to inQuadCubeToSol.

Equations

• One or more equations did not get rendered due to their size.

theorem MSSMACC.AnomalyFreePerp.inQuadCubeToSol_proj (T : InQuadCubeSol) : inQuadCubeToSol (inQuadCubeProj T) = ↑T

def MSSMACC.AnomalyFreePerp.toSol : AnomalyFreePerp × ℚ × ℚ × ℚ → MSSMACC.Sols

A solution from an element of MSSMACC.AnomalyFreePerp × ℚ × ℚ × ℚ. We will show that this map is a surjection.

Equations

• One or more equations did not get rendered due to their size.

theorem MSSMACC.AnomalyFreePerp.toSol_toSolNSProj (T : NotInLineEqSol) : ∃ (X : AnomalyFreePerp × ℚ × ℚ × ℚ), toSol X = ↑T

theorem MSSMACC.AnomalyFreePerp.toSol_inLineEq (T : InLineEqSol) : ∃ (X : AnomalyFreePerp × ℚ × ℚ × ℚ), toSol X = ↑T

theorem MSSMACC.AnomalyFreePerp.toSol_inQuad (T : InQuadSol) : ∃ (X : AnomalyFreePerp × ℚ × ℚ × ℚ), toSol X = ↑T

theorem MSSMACC.AnomalyFreePerp.toSol_inQuadCube (T : InQuadCubeSol) : ∃ (X : AnomalyFreePerp × ℚ × ℚ × ℚ), toSol X = ↑T

theorem MSSMACC.AnomalyFreePerp.toSol_surjective : Function.Surjective toSol