Parameterizations for solutions to the linear ACCs for 1 family

In this file we give two parameterizations

• linearParameters of solutions to the linear ACCs for 1 family
• linearParametersQENeqZero of solutions to the linear ACCs for 1 family with Q and E non-zero

These parameterizations are based on: https://arxiv.org/abs/1907.00514

structure SM.SMNoGrav.One.linearParameters : Type

The parameters for a linear parameterization to the solution of the linear ACCs.

• Q' : ℚ

  The parameter Q'.

• Y : ℚ

  The parameter Y.

• E' : ℚ

  The parameter E'.

theorem SM.SMNoGrav.One.linearParameters.ext {S T : linearParameters} (hQ : S.Q' = T.Q') (hY : S.Y = T.Y) (hE : S.E' = T.E') : S = T

theorem SM.SMNoGrav.One.linearParameters.ext_iff {S T : linearParameters} : S = T ↔ S.Q' = T.Q' ∧ S.Y = T.Y ∧ S.E' = T.E'

def SM.SMNoGrav.One.linearParameters.asCharges (S : linearParameters) : (SMNoGrav 1).Charges

The map from the linear parameters to elements of (SMNoGrav 1).charges.

Equations

• S.asCharges 0 = S.Q'
• S.asCharges 1 = S.Y - S.Q'
• S.asCharges 2 = -(S.Y + S.Q')
• S.asCharges 3 = -3 * S.Q'
• S.asCharges 4 = S.E'

theorem SM.SMNoGrav.One.linearParameters.speciesVal {i : Fin 5} (S : linearParameters) : (SMCharges.toSpecies i) S.asCharges 0 = S.asCharges i

def SM.SMNoGrav.One.linearParameters.asLinear (S : linearParameters) : (SMNoGrav 1).LinSols

The map from the linear parameters to elements of (SMNoGrav 1).LinSols.

Equations

• S.asLinear = SM.SMNoGrav.chargeToLinear S.asCharges ⋯ ⋯

theorem SM.SMNoGrav.One.linearParameters.asLinear_val (S : linearParameters) : S.asLinear.val = S.asCharges

theorem SM.SMNoGrav.One.linearParameters.cubic (S : linearParameters) : SMACCs.accCube S.asCharges = -54 * S.Q' ^ 3 - 18 * S.Q' * S.Y ^ 2 + S.E' ^ 3

theorem SM.SMNoGrav.One.linearParameters.cubic_zero_Q'_zero (S : linearParameters) (hc : SMACCs.accCube S.asCharges = 0) (h : S.Q' = 0) : S.E' = 0

theorem SM.SMNoGrav.One.linearParameters.cubic_zero_E'_zero (S : linearParameters) (hc : SMACCs.accCube S.asCharges = 0) (h : S.E' = 0) : S.Q' = 0

def SM.SMNoGrav.One.linearParameters.bijection : linearParameters ≃ (SMNoGrav 1).LinSols

The bijection between the type of linear parameters and (SMNoGrav 1).LinSols.

Equations

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

def SM.SMNoGrav.One.linearParameters.bijectionQEZero : { S : linearParameters // S.Q' ≠ 0 ∧ S.E' ≠ 0 } ≃ { S : (SMNoGrav 1).LinSols // SMCharges.Q S.val 0 ≠ 0 ∧ SMCharges.E S.val 0 ≠ 0 }

The bijection between the linear parameters and (SMNoGrav 1).LinSols in the special case when Q and E are both not zero.

Equations

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

theorem SM.SMNoGrav.One.linearParameters.grav (S : linearParameters) : SMACCs.accGrav S.asCharges = 0 ↔ S.E' = 6 * S.Q'

structure SM.SMNoGrav.One.linearParametersQENeqZero : Type

The parameters for solutions to the linear ACCs with the condition that Q and E are non-zero.

• x : ℚ

  The parameter x.

• v : ℚ

  The parameter v.

• w : ℚ

  The parameter w.

• hx : self.x ≠ 0
• hvw : self.v + self.w ≠ 0

theorem SM.SMNoGrav.One.linearParametersQENeqZero.ext {S T : linearParametersQENeqZero} (hx : S.x = T.x) (hv : S.v = T.v) (hw : S.w = T.w) : S = T

theorem SM.SMNoGrav.One.linearParametersQENeqZero.ext_iff {S T : linearParametersQENeqZero} : S = T ↔ S.x = T.x ∧ S.v = T.v ∧ S.w = T.w

def SM.SMNoGrav.One.linearParametersQENeqZero.toLinearParameters (S : linearParametersQENeqZero) : { S : linearParameters // S.Q' ≠ 0 ∧ S.E' ≠ 0 }

A map from linearParametersQENeqZero to linearParameters.

Equations

• S.toLinearParameters = ⟨{ Q' := S.x, Y := 3 * S.x * (S.v - S.w) / (S.v + S.w), E' := -6 * S.x / (S.v + S.w) }, ⋯⟩

@[simp]

theorem SM.SMNoGrav.One.linearParametersQENeqZero.toLinearParameters_coe_E' (S : linearParametersQENeqZero) : (↑S.toLinearParameters).E' = -(6 * S.x) / (S.v + S.w)

@[simp]

theorem SM.SMNoGrav.One.linearParametersQENeqZero.toLinearParameters_coe_Y (S : linearParametersQENeqZero) : (↑S.toLinearParameters).Y = 3 * S.x * (S.v - S.w) / (S.v + S.w)

@[simp]

theorem SM.SMNoGrav.One.linearParametersQENeqZero.toLinearParameters_coe_Q' (S : linearParametersQENeqZero) : (↑S.toLinearParameters).Q' = S.x

def SM.SMNoGrav.One.linearParametersQENeqZero.tolinearParametersQNeqZero (S : { S : linearParameters // S.Q' ≠ 0 ∧ S.E' ≠ 0 }) : linearParametersQENeqZero

A map from linearParameters to linearParametersQENeqZero in the special case when Q' and E' of the linear parameters are non-zero.

Equations

• SM.SMNoGrav.One.linearParametersQENeqZero.tolinearParametersQNeqZero S = { x := (↑S).Q', v := -(3 * (↑S).Q' + (↑S).Y) / (↑S).E', w := -(3 * (↑S).Q' - (↑S).Y) / (↑S).E', hx := ⋯, hvw := ⋯ }

@[simp]

theorem SM.SMNoGrav.One.linearParametersQENeqZero.tolinearParametersQNeqZero_v (S : { S : linearParameters // S.Q' ≠ 0 ∧ S.E' ≠ 0 }) : (tolinearParametersQNeqZero S).v = (-(↑S).Y + -(3 * (↑S).Q')) / (↑S).E'

@[simp]

theorem SM.SMNoGrav.One.linearParametersQENeqZero.tolinearParametersQNeqZero_w (S : { S : linearParameters // S.Q' ≠ 0 ∧ S.E' ≠ 0 }) : (tolinearParametersQNeqZero S).w = ((↑S).Y - 3 * (↑S).Q') / (↑S).E'

@[simp]

theorem SM.SMNoGrav.One.linearParametersQENeqZero.tolinearParametersQNeqZero_x (S : { S : linearParameters // S.Q' ≠ 0 ∧ S.E' ≠ 0 }) : (tolinearParametersQNeqZero S).x = (↑S).Q'

def SM.SMNoGrav.One.linearParametersQENeqZero.bijectionLinearParameters : linearParametersQENeqZero ≃ { S : linearParameters // S.Q' ≠ 0 ∧ S.E' ≠ 0 }

A bijection between the type linearParametersQENeqZero and linear parameters with Q' and E' non-zero.

Equations

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

@[simp]

theorem SM.SMNoGrav.One.linearParametersQENeqZero.bijectionLinearParameters_apply_coe_Y (S : linearParametersQENeqZero) : (↑(bijectionLinearParameters S)).Y = 3 * S.x * (S.v - S.w) / (S.v + S.w)

@[simp]

theorem SM.SMNoGrav.One.linearParametersQENeqZero.bijectionLinearParameters_apply_coe_Q' (S : linearParametersQENeqZero) : (↑(bijectionLinearParameters S)).Q' = S.x

@[simp]

theorem SM.SMNoGrav.One.linearParametersQENeqZero.bijectionLinearParameters_symm_apply_w (S : { S : linearParameters // S.Q' ≠ 0 ∧ S.E' ≠ 0 }) : (bijectionLinearParameters.symm S).w = ((↑S).Y - 3 * (↑S).Q') / (↑S).E'

@[simp]

theorem SM.SMNoGrav.One.linearParametersQENeqZero.bijectionLinearParameters_apply_coe_E' (S : linearParametersQENeqZero) : (↑(bijectionLinearParameters S)).E' = -(6 * S.x) / (S.v + S.w)

@[simp]

theorem SM.SMNoGrav.One.linearParametersQENeqZero.bijectionLinearParameters_symm_apply_x (S : { S : linearParameters // S.Q' ≠ 0 ∧ S.E' ≠ 0 }) : (bijectionLinearParameters.symm S).x = (↑S).Q'

@[simp]

theorem SM.SMNoGrav.One.linearParametersQENeqZero.bijectionLinearParameters_symm_apply_v (S : { S : linearParameters // S.Q' ≠ 0 ∧ S.E' ≠ 0 }) : (bijectionLinearParameters.symm S).v = (-(↑S).Y + -(3 * (↑S).Q')) / (↑S).E'

def SM.SMNoGrav.One.linearParametersQENeqZero.bijection : linearParametersQENeqZero ≃ { S : (SMNoGrav 1).LinSols // SMCharges.Q S.val 0 ≠ 0 ∧ SMCharges.E S.val 0 ≠ 0 }

The bijection between linearParametersQENeqZero and LinSols with Q and E non-zero.

Equations

• SM.SMNoGrav.One.linearParametersQENeqZero.bijection = SM.SMNoGrav.One.linearParametersQENeqZero.bijectionLinearParameters.trans SM.SMNoGrav.One.linearParameters.bijectionQEZero

theorem SM.SMNoGrav.One.linearParametersQENeqZero.cubic (S : linearParametersQENeqZero) : SMACCs.accCube (↑(bijection S)).val = 0 ↔ S.v ^ 3 + S.w ^ 3 = -1

theorem SM.SMNoGrav.One.linearParametersQENeqZero.cubic_v_or_w_zero (S : linearParametersQENeqZero) (h : SMACCs.accCube (↑(bijection S)).val = 0) : S.v = 0 ∨ S.w = 0

theorem SM.SMNoGrav.One.linearParametersQENeqZero.cubic_v_zero (S : linearParametersQENeqZero) (h : SMACCs.accCube (↑(bijection S)).val = 0) (hv : S.v = 0) : S.w = -1

theorem SM.SMNoGrav.One.linearParametersQENeqZero.cube_w_zero (S : linearParametersQENeqZero) (h : SMACCs.accCube (↑(bijection S)).val = 0) (hw : S.w = 0) : S.v = -1

theorem SM.SMNoGrav.One.linearParametersQENeqZero.cube_w_v (S : linearParametersQENeqZero) (h : SMACCs.accCube (↑(bijection S)).val = 0) : S.v = -1 ∧ S.w = 0 ∨ S.v = 0 ∧ S.w = -1

theorem SM.SMNoGrav.One.linearParametersQENeqZero.grav (S : linearParametersQENeqZero) : SMACCs.accGrav (↑(bijection S)).val = 0 ↔ S.v + S.w = -1

theorem SM.SMNoGrav.One.linearParametersQENeqZero.grav_of_cubic (S : linearParametersQENeqZero) (h : SMACCs.accCube (↑(bijection S)).val = 0) : SMACCs.accGrav (↑(bijection S)).val = 0