Dimension 7 plane

We work here in the three family case. We give an example of a 7 dimensional plane on which every point satisfies the ACCs.

The main result of this file is seven_dim_plane_exists which states that there exists a 7 dimensional plane of charges on which every point satisfies the ACCs.

def SMRHN.SM.PlaneSeven.B₀ : (SM 3).Charges

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

Equations

• SMRHN.SM.PlaneSeven.B₀ = SMνCharges.toSpeciesEquiv.invFun fun (s : Fin 6) (i : Fin 3) => match s, i with | 0, 0 => 1 | 0, 1 => -1 | x, x_1 => 0

theorem SMRHN.SM.PlaneSeven.B₀_cubic (S T : (SM 3).Charges) : ((SMνACCs.cubeTriLin B₀) S) T = 6 * (S 0 * T 0 - S 1 * T 1)

def SMRHN.SM.PlaneSeven.B₁ : (SM 3).Charges

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

Equations

• SMRHN.SM.PlaneSeven.B₁ = SMνCharges.toSpeciesEquiv.invFun fun (s : Fin 6) (i : Fin 3) => match s, i with | 1, 0 => 1 | 1, 1 => -1 | x, x_1 => 0

theorem SMRHN.SM.PlaneSeven.B₁_cubic (S T : (SM 3).Charges) : ((SMνACCs.cubeTriLin B₁) S) T = 3 * (S 3 * T 3 - S 4 * T 4)

def SMRHN.SM.PlaneSeven.B₂ : (SM 3).Charges

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

Equations

• SMRHN.SM.PlaneSeven.B₂ = SMνCharges.toSpeciesEquiv.invFun fun (s : Fin 6) (i : Fin 3) => match s, i with | 2, 0 => 1 | 2, 1 => -1 | x, x_1 => 0

theorem SMRHN.SM.PlaneSeven.B₂_cubic (S T : (SM 3).Charges) : ((SMνACCs.cubeTriLin B₂) S) T = 3 * (S 6 * T 6 - S 7 * T 7)

def SMRHN.SM.PlaneSeven.B₃ : (SM 3).Charges

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

Equations

• SMRHN.SM.PlaneSeven.B₃ = SMνCharges.toSpeciesEquiv.invFun fun (s : Fin 6) (i : Fin 3) => match s, i with | 3, 0 => 1 | 3, 1 => -1 | x, x_1 => 0

theorem SMRHN.SM.PlaneSeven.B₃_cubic (S T : (SM 3).Charges) : ((SMνACCs.cubeTriLin B₃) S) T = 2 * (S 9 * T 9 - S 10 * T 10)

def SMRHN.SM.PlaneSeven.B₄ : (SM 3).Charges

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

Equations

• SMRHN.SM.PlaneSeven.B₄ = SMνCharges.toSpeciesEquiv.invFun fun (s : Fin 6) (i : Fin 3) => match s, i with | 4, 0 => 1 | 4, 1 => -1 | x, x_1 => 0

theorem SMRHN.SM.PlaneSeven.B₄_cubic (S T : (SM 3).Charges) : ((SMνACCs.cubeTriLin B₄) S) T = S 12 * T 12 - S 13 * T 13

def SMRHN.SM.PlaneSeven.B₅ : (SM 3).Charges

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

Equations

• SMRHN.SM.PlaneSeven.B₅ = SMνCharges.toSpeciesEquiv.invFun fun (s : Fin 6) (i : Fin 3) => match s, i with | 5, 0 => 1 | 5, 1 => -1 | x, x_1 => 0

theorem SMRHN.SM.PlaneSeven.B₅_cubic (S T : (SM 3).Charges) : ((SMνACCs.cubeTriLin B₅) S) T = S 15 * T 15 - S 16 * T 16

def SMRHN.SM.PlaneSeven.B₆ : (SM 3).Charges

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

Equations

• SMRHN.SM.PlaneSeven.B₆ = SMνCharges.toSpeciesEquiv.invFun fun (s : Fin 6) (i : Fin 3) => match s, i with | 1, 2 => 1 | 2, 2 => -1 | x, x_1 => 0

theorem SMRHN.SM.PlaneSeven.B₆_cubic (S T : (SM 3).Charges) : ((SMνACCs.cubeTriLin B₆) S) T = 3 * (S 5 * T 5 - S 8 * T 8)

def SMRHN.SM.PlaneSeven.B : Fin 7 → (SM 3).Charges

The charge assignments forming a basis of the plane.

Equations

• SMRHN.SM.PlaneSeven.B 0 = SMRHN.SM.PlaneSeven.B₀
• SMRHN.SM.PlaneSeven.B 1 = SMRHN.SM.PlaneSeven.B₁
• SMRHN.SM.PlaneSeven.B 2 = SMRHN.SM.PlaneSeven.B₂
• SMRHN.SM.PlaneSeven.B 3 = SMRHN.SM.PlaneSeven.B₃
• SMRHN.SM.PlaneSeven.B 4 = SMRHN.SM.PlaneSeven.B₄
• SMRHN.SM.PlaneSeven.B 5 = SMRHN.SM.PlaneSeven.B₅
• SMRHN.SM.PlaneSeven.B 6 = SMRHN.SM.PlaneSeven.B₆

theorem SMRHN.SM.PlaneSeven.B₀_Bi_cubic {i : Fin 7} (hi : 0 ≠ i) (S : (SM 3).Charges) : ((SMνACCs.cubeTriLin (B 0)) (B i)) S = 0

theorem SMRHN.SM.PlaneSeven.B₁_Bi_cubic {i : Fin 7} (hi : 1 ≠ i) (S : (SM 3).Charges) : ((SMνACCs.cubeTriLin (B 1)) (B i)) S = 0

theorem SMRHN.SM.PlaneSeven.B₂_Bi_cubic {i : Fin 7} (hi : 2 ≠ i) (S : (SM 3).Charges) : ((SMνACCs.cubeTriLin (B 2)) (B i)) S = 0

theorem SMRHN.SM.PlaneSeven.B₃_Bi_cubic {i : Fin 7} (hi : 3 ≠ i) (S : (SM 3).Charges) : ((SMνACCs.cubeTriLin (B 3)) (B i)) S = 0

theorem SMRHN.SM.PlaneSeven.B₄_Bi_cubic {i : Fin 7} (hi : 4 ≠ i) (S : (SM 3).Charges) : ((SMνACCs.cubeTriLin (B 4)) (B i)) S = 0

theorem SMRHN.SM.PlaneSeven.B₅_Bi_cubic {i : Fin 7} (hi : 5 ≠ i) (S : (SM 3).Charges) : ((SMνACCs.cubeTriLin (B 5)) (B i)) S = 0

theorem SMRHN.SM.PlaneSeven.B₆_Bi_cubic {i : Fin 7} (hi : 6 ≠ i) (S : (SM 3).Charges) : ((SMνACCs.cubeTriLin (B 6)) (B i)) S = 0

theorem SMRHN.SM.PlaneSeven.Bi_Bj_ne_cubic {i j : Fin 7} (h : i ≠ j) (S : (SM 3).Charges) : ((SMνACCs.cubeTriLin (B i)) (B j)) S = 0

theorem SMRHN.SM.PlaneSeven.B₀_B₀_Bi_cubic {i : Fin 7} : ((SMνACCs.cubeTriLin (B 0)) (B 0)) (B i) = 0

theorem SMRHN.SM.PlaneSeven.B₁_B₁_Bi_cubic {i : Fin 7} : ((SMνACCs.cubeTriLin (B 1)) (B 1)) (B i) = 0

theorem SMRHN.SM.PlaneSeven.B₂_B₂_Bi_cubic {i : Fin 7} : ((SMνACCs.cubeTriLin (B 2)) (B 2)) (B i) = 0

theorem SMRHN.SM.PlaneSeven.B₃_B₃_Bi_cubic {i : Fin 7} : ((SMνACCs.cubeTriLin (B 3)) (B 3)) (B i) = 0

theorem SMRHN.SM.PlaneSeven.B₄_B₄_Bi_cubic {i : Fin 7} : ((SMνACCs.cubeTriLin (B 4)) (B 4)) (B i) = 0

theorem SMRHN.SM.PlaneSeven.B₅_B₅_Bi_cubic {i : Fin 7} : ((SMνACCs.cubeTriLin (B 5)) (B 5)) (B i) = 0

theorem SMRHN.SM.PlaneSeven.B₆_B₆_Bi_cubic {i : Fin 7} : ((SMνACCs.cubeTriLin (B 6)) (B 6)) (B i) = 0

theorem SMRHN.SM.PlaneSeven.Bi_Bi_Bj_cubic (i j : Fin 7) : ((SMνACCs.cubeTriLin (B i)) (B i)) (B j) = 0

theorem SMRHN.SM.PlaneSeven.Bi_Bj_Bk_cubic (i j k : Fin 7) : ((SMνACCs.cubeTriLin (B i)) (B j)) (B k) = 0

theorem SMRHN.SM.PlaneSeven.B_in_accCube (f : Fin 7 → ℚ) : SMνACCs.accCube (∑ i : Fin 7, f i • B i) = 0

theorem SMRHN.SM.PlaneSeven.B_sum_is_sol (f : Fin 7 → ℚ) : (SM 3).IsSolution (∑ i : Fin 7, f i • B i)

theorem SMRHN.SM.PlaneSeven.basis_linear_independent : LinearIndependent ℚ B

theorem SMRHN.SM.seven_dim_plane_exists : ∃ (B : Fin 7 → (SM 3).Charges), LinearIndependent ℚ B ∧ ∀ (f : Fin 7 → ℚ), (SM 3).IsSolution (∑ i : Fin 7, f i • B i)