94 lines
3.5 KiB
Text
94 lines
3.5 KiB
Text
/-
|
||
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
|
||
Released under Apache 2.0 license.
|
||
Authors: Joseph Tooby-Smith
|
||
-/
|
||
import HepLean.AnomalyCancellation.MSSMNu.Basic
|
||
import HepLean.AnomalyCancellation.MSSMNu.Y3
|
||
import HepLean.AnomalyCancellation.MSSMNu.B3
|
||
import Mathlib.Tactic.Polyrith
|
||
/-!
|
||
# The line through B₃ and Y₃
|
||
|
||
We give properties of lines through `B₃` and `Y₃`. We show that every point on this line
|
||
is a solution to the quadratic `lineY₃B₃Charges_quad` and a double point of the cubic
|
||
`lineY₃B₃_doublePoint`.
|
||
|
||
# References
|
||
|
||
The main reference for the material in this file is:
|
||
|
||
- https://arxiv.org/pdf/2107.07926.pdf
|
||
|
||
-/
|
||
|
||
universe v u
|
||
|
||
namespace MSSMACC
|
||
open MSSMCharges
|
||
open MSSMACCs
|
||
open BigOperators
|
||
|
||
/-- The line through $Y_3$ and $B_3$ as `LinSols`. -/
|
||
def lineY₃B₃Charges (a b : ℚ) : MSSMACC.LinSols := a • Y₃.1.1 + b • B₃.1.1
|
||
|
||
lemma lineY₃B₃Charges_quad (a b : ℚ) : accQuad (lineY₃B₃Charges a b).val = 0 := by
|
||
change accQuad (a • Y₃.val + b • B₃.val) = 0
|
||
rw [accQuad]
|
||
rw [quadBiLin.toHomogeneousQuad_add]
|
||
rw [quadBiLin.toHomogeneousQuad.map_smul]
|
||
rw [quadBiLin.toHomogeneousQuad.map_smul]
|
||
rw [quadBiLin.map_smul₁, quadBiLin.map_smul₂]
|
||
erw [quadSol Y₃.1, quadSol B₃.1]
|
||
simp only [mul_zero, add_zero, Fin.isValue, Fin.reduceFinMk, zero_add,
|
||
mul_eq_zero, OfNat.ofNat_ne_zero, false_or]
|
||
apply Or.inr ∘ Or.inr
|
||
rfl
|
||
|
||
lemma lineY₃B₃Charges_cubic (a b : ℚ) : accCube (lineY₃B₃Charges a b).val = 0 := by
|
||
change accCube (a • Y₃.val + b • B₃.val) = 0
|
||
rw [accCube]
|
||
rw [cubeTriLin.toCubic_add]
|
||
rw [cubeTriLin.toCubic.map_smul]
|
||
rw [cubeTriLin.toCubic.map_smul]
|
||
rw [cubeTriLin.map_smul₁, cubeTriLin.map_smul₂, cubeTriLin.map_smul₃]
|
||
rw [cubeTriLin.map_smul₁, cubeTriLin.map_smul₂, cubeTriLin.map_smul₃]
|
||
erw [Y₃.cubicSol, B₃.cubicSol]
|
||
rw [show cubeTriLin Y₃.val Y₃.val B₃.val = 0 by rfl]
|
||
rw [show cubeTriLin B₃.val B₃.val Y₃.val = 0 by rfl]
|
||
simp
|
||
|
||
/-- The line through $Y_3$ and $B_3$ as `Sols`. -/
|
||
def lineY₃B₃ (a b : ℚ) : MSSMACC.Sols :=
|
||
AnomalyFreeMk' (lineY₃B₃Charges a b) (lineY₃B₃Charges_quad a b) (lineY₃B₃Charges_cubic a b)
|
||
|
||
lemma doublePoint_Y₃_B₃ (R : MSSMACC.LinSols) :
|
||
cubeTriLin Y₃.val B₃.val R.val = 0 := by
|
||
simp only [cubeTriLin, TriLinearSymm.mk₃_toFun_apply_apply, cubeTriLinToFun,
|
||
MSSMSpecies_numberCharges, Fin.isValue, Fin.reduceFinMk]
|
||
rw [Fin.sum_univ_three]
|
||
rw [B₃_val, Y₃_val]
|
||
rw [B₃AsCharge, Y₃AsCharge]
|
||
repeat rw [toSMSpecies_toSpecies_inv]
|
||
rw [Hd_toSpecies_inv, Hu_toSpecies_inv]
|
||
rw [Hd_toSpecies_inv, Hu_toSpecies_inv]
|
||
simp only [mul_one, Fin.isValue, toSMSpecies_apply, one_mul, mul_neg, neg_neg, neg_mul, zero_mul,
|
||
add_zero, neg_zero, Hd_apply, Fin.reduceFinMk, Hu_apply]
|
||
have hLin := R.linearSol
|
||
simp at hLin
|
||
have h1 := hLin 1
|
||
have h2 := hLin 2
|
||
have h3 := hLin 3
|
||
simp [Fin.sum_univ_three] at h1 h2 h3
|
||
linear_combination -(12 * h2) + 9 * h1 + 3 * h3
|
||
|
||
lemma lineY₃B₃_doublePoint (R : MSSMACC.LinSols) (a b : ℚ) :
|
||
cubeTriLin (lineY₃B₃ a b).val (lineY₃B₃ a b).val R.val = 0 := by
|
||
change cubeTriLin (a • Y₃.val + b • B₃.val) (a • Y₃.val + b • B₃.val) R.val = 0
|
||
rw [cubeTriLin.map_add₂, cubeTriLin.map_add₁, cubeTriLin.map_add₁]
|
||
repeat rw [cubeTriLin.map_smul₂, cubeTriLin.map_smul₁]
|
||
rw [doublePoint_B₃_B₃, doublePoint_Y₃_Y₃, doublePoint_Y₃_B₃]
|
||
rw [cubeTriLin.swap₁, doublePoint_Y₃_B₃]
|
||
simp
|
||
|
||
end MSSMACC
|