Plane of non-solutions

Working in the three family case, we show that there exists an eleven dimensional plane in the vector space of charges on which there are no solutions.

The main result of this file is eleven_dim_plane_of_no_sols_exists, which states that an 11 dimensional plane of charges exists on which there are no solutions except the origin.

def SMRHN.PlusU1.ElevenPlane.B₀ : (PlusU1 3).Charges

A charge assignment forming one of the basis elements of the plane.

Equations

• SMRHN.PlusU1.ElevenPlane.B₀ = ![1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]

def SMRHN.PlusU1.ElevenPlane.B₁ : (PlusU1 3).Charges

A charge assignment forming one of the basis elements of the plane.

Equations

• SMRHN.PlusU1.ElevenPlane.B₁ = ![0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]

def SMRHN.PlusU1.ElevenPlane.B₂ : (PlusU1 3).Charges

A charge assignment forming one of the basis elements of the plane.

Equations

• SMRHN.PlusU1.ElevenPlane.B₂ = ![0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]

def SMRHN.PlusU1.ElevenPlane.B₃ : (PlusU1 3).Charges

A charge assignment forming one of the basis elements of the plane.

Equations

• SMRHN.PlusU1.ElevenPlane.B₃ = ![0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]

def SMRHN.PlusU1.ElevenPlane.B₄ : (PlusU1 3).Charges

A charge assignment forming one of the basis elements of the plane.

Equations

• SMRHN.PlusU1.ElevenPlane.B₄ = ![0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]

def SMRHN.PlusU1.ElevenPlane.B₅ : (PlusU1 3).Charges

A charge assignment forming one of the basis elements of the plane.

Equations

• SMRHN.PlusU1.ElevenPlane.B₅ = ![0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0]

def SMRHN.PlusU1.ElevenPlane.B₆ : (PlusU1 3).Charges

A charge assignment forming one of the basis elements of the plane.

Equations

• SMRHN.PlusU1.ElevenPlane.B₆ = ![0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0]

def SMRHN.PlusU1.ElevenPlane.B₇ : (PlusU1 3).Charges

A charge assignment forming one of the basis elements of the plane.

Equations

• SMRHN.PlusU1.ElevenPlane.B₇ = ![0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0]

def SMRHN.PlusU1.ElevenPlane.B₈ : (PlusU1 3).Charges

A charge assignment forming one of the basis elements of the plane.

Equations

• SMRHN.PlusU1.ElevenPlane.B₈ = ![0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0]

def SMRHN.PlusU1.ElevenPlane.B₉ : (PlusU1 3).Charges

A charge assignment forming one of the basis elements of the plane.

Equations

• SMRHN.PlusU1.ElevenPlane.B₉ = ![0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 2, 0]

def SMRHN.PlusU1.ElevenPlane.B₁₀ : (PlusU1 3).Charges

A charge assignment forming one of the basis elements of the plane.

Equations

• SMRHN.PlusU1.ElevenPlane.B₁₀ = ![0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1]

def SMRHN.PlusU1.ElevenPlane.B : Fin 11 → (PlusU1 3).Charges

The charge assignment forming a basis of the plane.

Equations

• SMRHN.PlusU1.ElevenPlane.B 0 = SMRHN.PlusU1.ElevenPlane.B₀
• SMRHN.PlusU1.ElevenPlane.B 1 = SMRHN.PlusU1.ElevenPlane.B₁
• SMRHN.PlusU1.ElevenPlane.B 2 = SMRHN.PlusU1.ElevenPlane.B₂
• SMRHN.PlusU1.ElevenPlane.B 3 = SMRHN.PlusU1.ElevenPlane.B₃
• SMRHN.PlusU1.ElevenPlane.B 4 = SMRHN.PlusU1.ElevenPlane.B₄
• SMRHN.PlusU1.ElevenPlane.B 5 = SMRHN.PlusU1.ElevenPlane.B₅
• SMRHN.PlusU1.ElevenPlane.B 6 = SMRHN.PlusU1.ElevenPlane.B₆
• SMRHN.PlusU1.ElevenPlane.B 7 = SMRHN.PlusU1.ElevenPlane.B₇
• SMRHN.PlusU1.ElevenPlane.B 8 = SMRHN.PlusU1.ElevenPlane.B₈
• SMRHN.PlusU1.ElevenPlane.B 9 = SMRHN.PlusU1.ElevenPlane.B₉
• SMRHN.PlusU1.ElevenPlane.B 10 = SMRHN.PlusU1.ElevenPlane.B₁₀

theorem SMRHN.PlusU1.ElevenPlane.Bi_Bj_quad {i j : Fin 11} (hi : i ≠ j) : (SMνACCs.quadBiLin (B i)) (B j) = 0

theorem SMRHN.PlusU1.ElevenPlane.Bi_sum_quad (i : Fin 11) (f : Fin 11 → ℚ) : (SMνACCs.quadBiLin (B i)) (∑ k : Fin 11, f k • B k) = f i * (SMνACCs.quadBiLin (B i)) (B i)

def SMRHN.PlusU1.ElevenPlane.quadCoeff : Fin 11 → ℚ

The coefficients of the quadratic equation in our basis.

Equations

• SMRHN.PlusU1.ElevenPlane.quadCoeff = ![1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0]

theorem SMRHN.PlusU1.ElevenPlane.quadCoeff_eq_bilinear (i : Fin 11) : quadCoeff i = (SMνACCs.quadBiLin (B i)) (B i)

theorem SMRHN.PlusU1.ElevenPlane.on_accQuad (f : Fin 11 → ℚ) : SMνACCs.accQuad (∑ i : Fin 11, f i • B i) = ∑ i : Fin 11, quadCoeff i * f i ^ 2

theorem SMRHN.PlusU1.ElevenPlane.isSolution_quadCoeff_f_sq_zero (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i : Fin 11, f i • B i)) (k : Fin 11) : quadCoeff k * f k ^ 2 = 0

theorem SMRHN.PlusU1.ElevenPlane.isSolution_f0 (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i : Fin 11, f i • B i)) : f 0 = 0

theorem SMRHN.PlusU1.ElevenPlane.isSolution_f1 (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i : Fin 11, f i • B i)) : f 1 = 0

theorem SMRHN.PlusU1.ElevenPlane.isSolution_f2 (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i : Fin 11, f i • B i)) : f 2 = 0

theorem SMRHN.PlusU1.ElevenPlane.isSolution_f3 (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i : Fin 11, f i • B i)) : f 3 = 0

theorem SMRHN.PlusU1.ElevenPlane.isSolution_f4 (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i : Fin 11, f i • B i)) : f 4 = 0

theorem SMRHN.PlusU1.ElevenPlane.isSolution_f5 (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i : Fin 11, f i • B i)) : f 5 = 0

theorem SMRHN.PlusU1.ElevenPlane.isSolution_f6 (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i : Fin 11, f i • B i)) : f 6 = 0

theorem SMRHN.PlusU1.ElevenPlane.isSolution_f7 (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i : Fin 11, f i • B i)) : f 7 = 0

theorem SMRHN.PlusU1.ElevenPlane.isSolution_f8 (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i : Fin 11, f i • B i)) : f 8 = 0

theorem SMRHN.PlusU1.ElevenPlane.isSolution_sum_part (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i : Fin 11, f i • B i)) : ∑ i : Fin 11, f i • B i = f 9 • B₉ + f 10 • B₁₀

theorem SMRHN.PlusU1.ElevenPlane.isSolution_grav (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i : Fin 11, f i • B i)) : f 10 = -3 * f 9

theorem SMRHN.PlusU1.ElevenPlane.isSolution_sum_part' (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i : Fin 11, f i • B i)) : ∑ i : Fin 11, f i • B i = f 9 • B₉ + (-3 * f 9) • B₁₀

theorem SMRHN.PlusU1.ElevenPlane.isSolution_f9 (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i : Fin 11, f i • B i)) : f 9 = 0

theorem SMRHN.PlusU1.ElevenPlane.isSolution_f10 (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i : Fin 11, f i • B i)) : f 10 = 0

theorem SMRHN.PlusU1.ElevenPlane.isSolution_f_zero (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i : Fin 11, f i • B i)) (k : Fin 11) : f k = 0

theorem SMRHN.PlusU1.ElevenPlane.isSolution_only_if_zero (f : Fin 11 → ℚ) (hS : (PlusU1 3).IsSolution (∑ i : Fin 11, f i • B i)) : ∑ i : Fin 11, f i • B i = 0

theorem SMRHN.PlusU1.ElevenPlane.basis_linear_independent : LinearIndependent ℚ B

theorem SMRHN.PlusU1.eleven_dim_plane_of_no_sols_exists : ∃ (B : Fin 11 → (PlusU1 3).Charges), LinearIndependent ℚ B ∧ ∀ (f : Fin 11 → ℚ), (PlusU1 3).IsSolution (∑ i : Fin 11, f i • B i) → ∑ i : Fin 11, f i • B i = 0