Physlib.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Ordinary.DimSevenPlane — Physlib

Imports

/-
Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.Particles.BeyondTheStandardModel.RHN.AnomalyCancellation.Ordinary.Basic

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.

@[expose] public section

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

def B₀ : (SM 3).Charges := toSpeciesEquiv.invFun (fun s => fun i =>
  match s, i with
  | 0, 0 => 1
  | 0, 1 => - 1
  | _, _ => 0)

set_option backward.isDefEq.respectTransparency false in
lemma B₀_cubic (S T : (SM 3).Charges) : cubeTriLin B₀ S T =
    6 * (S (0 : Fin 18) * T (0 : Fin 18) - S (1 : Fin 18) * T (1 : Fin 18)) := byS:(SM 3).ChargesT:(SM 3).Charges⊢ ((cubeTriLin B₀) S) T = 6 * (S 0 * T 0 - S 1 * T 1)
  simp [B₀, cubeTriLin_toFun_apply_apply, finProdFinEquiv, Fin.divNat, Fin.modNat,
    Fin.sum_univ_three]S:(SM 3).ChargesT:(SM 3).Charges⊢ 6 * (S 0 * T 0) + -(6 * (S 1 * T 1)) = 6 * (S 0 * T 0 - S 1 * T 1)
  ringAll goals completed! 🐙

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

def B₁ : (SM 3).Charges := toSpeciesEquiv.invFun (fun s => fun i =>
  match s, i with
  | 1, 0 => 1
  | 1, 1 => - 1
  | _, _ => 0)

set_option backward.isDefEq.respectTransparency false in
lemma B₁_cubic (S T : (SM 3).Charges) : cubeTriLin B₁ S T =
    3 * (S (3 : Fin 18) * T (3 : Fin 18) - S (4 : Fin 18) * T (4 : Fin 18)) := byS:(SM 3).ChargesT:(SM 3).Charges⊢ ((cubeTriLin B₁) S) T = 3 * (S 3 * T 3 - S 4 * T 4)
  simp [B₁, cubeTriLin_toFun_apply_apply, finProdFinEquiv, Fin.divNat, Fin.modNat,
    Fin.sum_univ_three]S:(SM 3).ChargesT:(SM 3).Charges⊢ 3 * (S 3 * T 3) + -(3 * (S 4 * T 4)) = 3 * (S 3 * T 3 - S 4 * T 4)
  ringAll goals completed! 🐙

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

def B₂ : (SM 3).Charges := toSpeciesEquiv.invFun (fun s => fun i =>
  match s, i with
  | 2, 0 => 1
  | 2, 1 => - 1
  | _, _ => 0)

set_option backward.isDefEq.respectTransparency false in
lemma B₂_cubic (S T : (SM 3).Charges) : cubeTriLin B₂ S T =
    3 * (S (6 : Fin 18) * T (6 : Fin 18) - S (7 : Fin 18) * T (7 : Fin 18)) := byS:(SM 3).ChargesT:(SM 3).Charges⊢ ((cubeTriLin B₂) S) T = 3 * (S 6 * T 6 - S 7 * T 7)
  simp [B₂, cubeTriLin_toFun_apply_apply, finProdFinEquiv, Fin.divNat, Fin.modNat,
    Fin.sum_univ_three]S:(SM 3).ChargesT:(SM 3).Charges⊢ 3 * (S 6 * T 6) + -(3 * (S 7 * T 7)) = 3 * (S 6 * T 6 - S 7 * T 7)
  ringAll goals completed! 🐙

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

def B₃ : (SM 3).Charges := toSpeciesEquiv.invFun (fun s => fun i =>
  match s, i with
  | 3, 0 => 1
  | 3, 1 => - 1
  | _, _ => 0)

set_option backward.isDefEq.respectTransparency false in
lemma B₃_cubic (S T : (SM 3).Charges) : cubeTriLin B₃ S T =
    2 * (S (9 : Fin 18) * T (9 : Fin 18) - S (10 : Fin 18) * T (10 : Fin 18)) := byS:(SM 3).ChargesT:(SM 3).Charges⊢ ((cubeTriLin B₃) S) T = 2 * (S 9 * T 9 - S 10 * T 10)
  simp [B₃, cubeTriLin_toFun_apply_apply, finProdFinEquiv, Fin.divNat, Fin.modNat,
    Fin.sum_univ_three]S:(SM 3).ChargesT:(SM 3).Charges⊢ 2 * (S 9 * T 9) + -(2 * (S 10 * T 10)) = 2 * (S 9 * T 9 - S 10 * T 10)
  ringAll goals completed! 🐙

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

def B₄ : (SM 3).Charges := toSpeciesEquiv.invFun (fun s => fun i =>
  match s, i with
  | 4, 0 => 1
  | 4, 1 => - 1
  | _, _ => 0)

set_option backward.isDefEq.respectTransparency false in
lemma B₄_cubic (S T : (SM 3).Charges) : cubeTriLin B₄ S T =
    (S (12 : Fin 18) * T (12 : Fin 18) - S (13 : Fin 18) * T (13 : Fin 18)) := byS:(SM 3).ChargesT:(SM 3).Charges⊢ ((cubeTriLin B₄) S) T = S 12 * T 12 - S 13 * T 13
  simp [B₄, cubeTriLin_toFun_apply_apply, finProdFinEquiv, Fin.divNat, Fin.modNat,
    Fin.sum_univ_three]S:(SM 3).ChargesT:(SM 3).Charges⊢ S 12 * T 12 + -(S 13 * T 13) = S 12 * T 12 - S 13 * T 13
  ringAll goals completed! 🐙

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

def B₅ : (SM 3).Charges := toSpeciesEquiv.invFun (fun s => fun i =>
  match s, i with
  | 5, 0 => 1
  | 5, 1 => - 1
  | _, _ => 0)

set_option backward.isDefEq.respectTransparency false in
lemma B₅_cubic (S T : (SM 3).Charges) : cubeTriLin B₅ S T =
    (S (15 : Fin 18) * T (15 : Fin 18) - S (16 : Fin 18) * T (16 : Fin 18)) := byS:(SM 3).ChargesT:(SM 3).Charges⊢ ((cubeTriLin B₅) S) T = S 15 * T 15 - S 16 * T 16
  simp [B₅, cubeTriLin_toFun_apply_apply, finProdFinEquiv, Fin.divNat, Fin.modNat,
    Fin.sum_univ_three]S:(SM 3).ChargesT:(SM 3).Charges⊢ S 15 * T 15 + -(S 16 * T 16) = S 15 * T 15 - S 16 * T 16
  ringAll goals completed! 🐙

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

def B₆ : (SM 3).Charges := toSpeciesEquiv.invFun (fun s => fun i =>
  match s, i with
  | 1, 2 => 1
  | 2, 2 => -1
  | _, _ => 0)

set_option backward.isDefEq.respectTransparency false in
lemma B₆_cubic (S T : (SM 3).Charges) : cubeTriLin B₆ S T =
    3 * (S (5 : Fin 18) * T (5 : Fin 18) - S (8 : Fin 18) * T (8 : Fin 18)) := byS:(SM 3).ChargesT:(SM 3).Charges⊢ ((cubeTriLin B₆) S) T = 3 * (S 5 * T 5 - S 8 * T 8)
  simp [B₆, cubeTriLin_toFun_apply_apply, finProdFinEquiv, Fin.divNat, Fin.modNat,
    Fin.sum_univ_three]S:(SM 3).ChargesT:(SM 3).Charges⊢ 3 * (S 5 * T 5) + -(3 * (S 8 * T 8)) = 3 * (S 5 * T 5 - S 8 * T 8)
  ringAll goals completed! 🐙

TODO "Remove the definitions of elements `(SM 3).Charges` B₀, B₁ etc, here are
  use only `B : Fin 7 → (SM 3).Charges`. "

The charge assignments forming a basis of the plane.

@[simp]
abbrev B : Fin 7 → (SM 3).Charges := fun i =>
  match i with
  | 0 => B₀
  | 1 => B₁
  | 2 => B₂
  | 3 => B₃
  | 4 => B₄
  | 5 => B₅
  | 6 => B₆

              

lemma B₀_Bi_cubic {i : Fin 7} (hi : 0 ≠ i) (S : (SM 3).Charges) :
    cubeTriLin (B 0) (B i) S = 0 := byi:Fin 7hi:0 ≠ iS:(SM 3).Charges⊢ ((cubeTriLin (B 0)) (B i)) S = 0
  change cubeTriLin B₀ (B i) S = 0i:Fin 7hi:0 ≠ iS:(SM 3).Charges⊢ ((cubeTriLin B₀) (B i)) S = 0
  rw [B₀_cubici:Fin 7hi:0 ≠ iS:(SM 3).Charges⊢ 6 * (B i 0 * S 0 - B i 1 * S 1) = 0i:Fin 7hi:0 ≠ iS:(SM 3).Charges⊢ 6 * (B i 0 * S 0 - B i 1 * S 1) = 0]i:Fin 7hi:0 ≠ iS:(SM 3).Charges⊢ 6 * (B i 0 * S 0 - B i 1 * S 1) = 0
  fin_cases i«0»S:(SM 3).Chargeshi:0 ≠ (fun i => i) ⟨0, ⋯⟩⊢ 6 * (B ((fun i => i) ⟨0, ⋯⟩) 0 * S 0 - B ((fun i => i) ⟨0, ⋯⟩) 1 * S 1) = 0«1»S:(SM 3).Chargeshi:0 ≠ (fun i => i) ⟨1, ⋯⟩⊢ 6 * (B ((fun i => i) ⟨1, ⋯⟩) 0 * S 0 - B ((fun i => i) ⟨1, ⋯⟩) 1 * S 1) = 0«2»S:(SM 3).Chargeshi:0 ≠ (fun i => i) ⟨2, ⋯⟩⊢ 6 * (B ((fun i => i) ⟨2, ⋯⟩) 0 * S 0 - B ((fun i => i) ⟨2, ⋯⟩) 1 * S 1) = 0«3»S:(SM 3).Chargeshi:0 ≠ (fun i => i) ⟨3, ⋯⟩⊢ 6 * (B ((fun i => i) ⟨3, ⋯⟩) 0 * S 0 - B ((fun i => i) ⟨3, ⋯⟩) 1 * S 1) = 0«4»S:(SM 3).Chargeshi:0 ≠ (fun i => i) ⟨4, ⋯⟩⊢ 6 * (B ((fun i => i) ⟨4, ⋯⟩) 0 * S 0 - B ((fun i => i) ⟨4, ⋯⟩) 1 * S 1) = 0«5»S:(SM 3).Chargeshi:0 ≠ (fun i => i) ⟨5, ⋯⟩⊢ 6 * (B ((fun i => i) ⟨5, ⋯⟩) 0 * S 0 - B ((fun i => i) ⟨5, ⋯⟩) 1 * S 1) = 0«6»S:(SM 3).Chargeshi:0 ≠ (fun i => i) ⟨6, ⋯⟩⊢ 6 * (B ((fun i => i) ⟨6, ⋯⟩) 0 * S 0 - B ((fun i => i) ⟨6, ⋯⟩) 1 * S 1) = 0 <;>«0»S:(SM 3).Chargeshi:0 ≠ (fun i => i) ⟨0, ⋯⟩⊢ 6 * (B ((fun i => i) ⟨0, ⋯⟩) 0 * S 0 - B ((fun i => i) ⟨0, ⋯⟩) 1 * S 1) = 0«1»S:(SM 3).Chargeshi:0 ≠ (fun i => i) ⟨1, ⋯⟩⊢ 6 * (B ((fun i => i) ⟨1, ⋯⟩) 0 * S 0 - B ((fun i => i) ⟨1, ⋯⟩) 1 * S 1) = 0«2»S:(SM 3).Chargeshi:0 ≠ (fun i => i) ⟨2, ⋯⟩⊢ 6 * (B ((fun i => i) ⟨2, ⋯⟩) 0 * S 0 - B ((fun i => i) ⟨2, ⋯⟩) 1 * S 1) = 0«3»S:(SM 3).Chargeshi:0 ≠ (fun i => i) ⟨3, ⋯⟩⊢ 6 * (B ((fun i => i) ⟨3, ⋯⟩) 0 * S 0 - B ((fun i => i) ⟨3, ⋯⟩) 1 * S 1) = 0«4»S:(SM 3).Chargeshi:0 ≠ (fun i => i) ⟨4, ⋯⟩⊢ 6 * (B ((fun i => i) ⟨4, ⋯⟩) 0 * S 0 - B ((fun i => i) ⟨4, ⋯⟩) 1 * S 1) = 0«5»S:(SM 3).Chargeshi:0 ≠ (fun i => i) ⟨5, ⋯⟩⊢ 6 * (B ((fun i => i) ⟨5, ⋯⟩) 0 * S 0 - B ((fun i => i) ⟨5, ⋯⟩) 1 * S 1) = 0«6»S:(SM 3).Chargeshi:0 ≠ (fun i => i) ⟨6, ⋯⟩⊢ 6 * (B ((fun i => i) ⟨6, ⋯⟩) 0 * S 0 - B ((fun i => i) ⟨6, ⋯⟩) 1 * S 1) = 0
    first | exact absurd rfl hi«6»S:(SM 3).Chargeshi:0 ≠ (fun i => i) ⟨6, ⋯⟩⊢ 6 * (B ((fun i => i) ⟨6, ⋯⟩) 0 * S 0 - B ((fun i => i) ⟨6, ⋯⟩) 1 * S 1) = 0 | simp [B₁, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat]All goals completed! 🐙

lemma B₁_Bi_cubic {i : Fin 7} (hi : 1 ≠ i) (S : (SM 3).Charges) :
    cubeTriLin (B 1) (B i) S = 0 := byi:Fin 7hi:1 ≠ iS:(SM 3).Charges⊢ ((cubeTriLin (B 1)) (B i)) S = 0
  change cubeTriLin B₁ (B i) S = 0i:Fin 7hi:1 ≠ iS:(SM 3).Charges⊢ ((cubeTriLin B₁) (B i)) S = 0
  rw [B₁_cubici:Fin 7hi:1 ≠ iS:(SM 3).Charges⊢ 3 * (B i 3 * S 3 - B i 4 * S 4) = 0i:Fin 7hi:1 ≠ iS:(SM 3).Charges⊢ 3 * (B i 3 * S 3 - B i 4 * S 4) = 0]i:Fin 7hi:1 ≠ iS:(SM 3).Charges⊢ 3 * (B i 3 * S 3 - B i 4 * S 4) = 0
  fin_cases i«0»S:(SM 3).Chargeshi:1 ≠ (fun i => i) ⟨0, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨0, ⋯⟩) 3 * S 3 - B ((fun i => i) ⟨0, ⋯⟩) 4 * S 4) = 0«1»S:(SM 3).Chargeshi:1 ≠ (fun i => i) ⟨1, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨1, ⋯⟩) 3 * S 3 - B ((fun i => i) ⟨1, ⋯⟩) 4 * S 4) = 0«2»S:(SM 3).Chargeshi:1 ≠ (fun i => i) ⟨2, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨2, ⋯⟩) 3 * S 3 - B ((fun i => i) ⟨2, ⋯⟩) 4 * S 4) = 0«3»S:(SM 3).Chargeshi:1 ≠ (fun i => i) ⟨3, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨3, ⋯⟩) 3 * S 3 - B ((fun i => i) ⟨3, ⋯⟩) 4 * S 4) = 0«4»S:(SM 3).Chargeshi:1 ≠ (fun i => i) ⟨4, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨4, ⋯⟩) 3 * S 3 - B ((fun i => i) ⟨4, ⋯⟩) 4 * S 4) = 0«5»S:(SM 3).Chargeshi:1 ≠ (fun i => i) ⟨5, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨5, ⋯⟩) 3 * S 3 - B ((fun i => i) ⟨5, ⋯⟩) 4 * S 4) = 0«6»S:(SM 3).Chargeshi:1 ≠ (fun i => i) ⟨6, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨6, ⋯⟩) 3 * S 3 - B ((fun i => i) ⟨6, ⋯⟩) 4 * S 4) = 0 <;>«0»S:(SM 3).Chargeshi:1 ≠ (fun i => i) ⟨0, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨0, ⋯⟩) 3 * S 3 - B ((fun i => i) ⟨0, ⋯⟩) 4 * S 4) = 0«1»S:(SM 3).Chargeshi:1 ≠ (fun i => i) ⟨1, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨1, ⋯⟩) 3 * S 3 - B ((fun i => i) ⟨1, ⋯⟩) 4 * S 4) = 0«2»S:(SM 3).Chargeshi:1 ≠ (fun i => i) ⟨2, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨2, ⋯⟩) 3 * S 3 - B ((fun i => i) ⟨2, ⋯⟩) 4 * S 4) = 0«3»S:(SM 3).Chargeshi:1 ≠ (fun i => i) ⟨3, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨3, ⋯⟩) 3 * S 3 - B ((fun i => i) ⟨3, ⋯⟩) 4 * S 4) = 0«4»S:(SM 3).Chargeshi:1 ≠ (fun i => i) ⟨4, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨4, ⋯⟩) 3 * S 3 - B ((fun i => i) ⟨4, ⋯⟩) 4 * S 4) = 0«5»S:(SM 3).Chargeshi:1 ≠ (fun i => i) ⟨5, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨5, ⋯⟩) 3 * S 3 - B ((fun i => i) ⟨5, ⋯⟩) 4 * S 4) = 0«6»S:(SM 3).Chargeshi:1 ≠ (fun i => i) ⟨6, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨6, ⋯⟩) 3 * S 3 - B ((fun i => i) ⟨6, ⋯⟩) 4 * S 4) = 0
    first | exact absurd rfl hi«6»S:(SM 3).Chargeshi:1 ≠ (fun i => i) ⟨6, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨6, ⋯⟩) 3 * S 3 - B ((fun i => i) ⟨6, ⋯⟩) 4 * S 4) = 0 | simp [B₀, B₂, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat]All goals completed! 🐙

lemma B₂_Bi_cubic {i : Fin 7} (hi : 2 ≠ i) (S : (SM 3).Charges) :
    cubeTriLin (B 2) (B i) S = 0 := byi:Fin 7hi:2 ≠ iS:(SM 3).Charges⊢ ((cubeTriLin (B 2)) (B i)) S = 0
  change cubeTriLin B₂ (B i) S = 0i:Fin 7hi:2 ≠ iS:(SM 3).Charges⊢ ((cubeTriLin B₂) (B i)) S = 0
  rw [B₂_cubici:Fin 7hi:2 ≠ iS:(SM 3).Charges⊢ 3 * (B i 6 * S 6 - B i 7 * S 7) = 0i:Fin 7hi:2 ≠ iS:(SM 3).Charges⊢ 3 * (B i 6 * S 6 - B i 7 * S 7) = 0]i:Fin 7hi:2 ≠ iS:(SM 3).Charges⊢ 3 * (B i 6 * S 6 - B i 7 * S 7) = 0
  fin_cases i«0»S:(SM 3).Chargeshi:2 ≠ (fun i => i) ⟨0, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨0, ⋯⟩) 6 * S 6 - B ((fun i => i) ⟨0, ⋯⟩) 7 * S 7) = 0«1»S:(SM 3).Chargeshi:2 ≠ (fun i => i) ⟨1, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨1, ⋯⟩) 6 * S 6 - B ((fun i => i) ⟨1, ⋯⟩) 7 * S 7) = 0«2»S:(SM 3).Chargeshi:2 ≠ (fun i => i) ⟨2, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨2, ⋯⟩) 6 * S 6 - B ((fun i => i) ⟨2, ⋯⟩) 7 * S 7) = 0«3»S:(SM 3).Chargeshi:2 ≠ (fun i => i) ⟨3, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨3, ⋯⟩) 6 * S 6 - B ((fun i => i) ⟨3, ⋯⟩) 7 * S 7) = 0«4»S:(SM 3).Chargeshi:2 ≠ (fun i => i) ⟨4, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨4, ⋯⟩) 6 * S 6 - B ((fun i => i) ⟨4, ⋯⟩) 7 * S 7) = 0«5»S:(SM 3).Chargeshi:2 ≠ (fun i => i) ⟨5, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨5, ⋯⟩) 6 * S 6 - B ((fun i => i) ⟨5, ⋯⟩) 7 * S 7) = 0«6»S:(SM 3).Chargeshi:2 ≠ (fun i => i) ⟨6, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨6, ⋯⟩) 6 * S 6 - B ((fun i => i) ⟨6, ⋯⟩) 7 * S 7) = 0 <;>«0»S:(SM 3).Chargeshi:2 ≠ (fun i => i) ⟨0, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨0, ⋯⟩) 6 * S 6 - B ((fun i => i) ⟨0, ⋯⟩) 7 * S 7) = 0«1»S:(SM 3).Chargeshi:2 ≠ (fun i => i) ⟨1, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨1, ⋯⟩) 6 * S 6 - B ((fun i => i) ⟨1, ⋯⟩) 7 * S 7) = 0«2»S:(SM 3).Chargeshi:2 ≠ (fun i => i) ⟨2, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨2, ⋯⟩) 6 * S 6 - B ((fun i => i) ⟨2, ⋯⟩) 7 * S 7) = 0«3»S:(SM 3).Chargeshi:2 ≠ (fun i => i) ⟨3, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨3, ⋯⟩) 6 * S 6 - B ((fun i => i) ⟨3, ⋯⟩) 7 * S 7) = 0«4»S:(SM 3).Chargeshi:2 ≠ (fun i => i) ⟨4, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨4, ⋯⟩) 6 * S 6 - B ((fun i => i) ⟨4, ⋯⟩) 7 * S 7) = 0«5»S:(SM 3).Chargeshi:2 ≠ (fun i => i) ⟨5, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨5, ⋯⟩) 6 * S 6 - B ((fun i => i) ⟨5, ⋯⟩) 7 * S 7) = 0«6»S:(SM 3).Chargeshi:2 ≠ (fun i => i) ⟨6, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨6, ⋯⟩) 6 * S 6 - B ((fun i => i) ⟨6, ⋯⟩) 7 * S 7) = 0
    first | exact absurd rfl hi«6»S:(SM 3).Chargeshi:2 ≠ (fun i => i) ⟨6, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨6, ⋯⟩) 6 * S 6 - B ((fun i => i) ⟨6, ⋯⟩) 7 * S 7) = 0 | simp [B₀, B₁, B₃, B₄, B₅, B₆, Fin.divNat, Fin.modNat]All goals completed! 🐙

lemma B₃_Bi_cubic {i : Fin 7} (hi : 3 ≠ i) (S : (SM 3).Charges) :
    cubeTriLin (B 3) (B i) S = 0 := byi:Fin 7hi:3 ≠ iS:(SM 3).Charges⊢ ((cubeTriLin (B 3)) (B i)) S = 0
  change cubeTriLin (B₃) (B i) S = 0i:Fin 7hi:3 ≠ iS:(SM 3).Charges⊢ ((cubeTriLin B₃) (B i)) S = 0
  rw [B₃_cubici:Fin 7hi:3 ≠ iS:(SM 3).Charges⊢ 2 * (B i 9 * S 9 - B i 10 * S 10) = 0i:Fin 7hi:3 ≠ iS:(SM 3).Charges⊢ 2 * (B i 9 * S 9 - B i 10 * S 10) = 0]i:Fin 7hi:3 ≠ iS:(SM 3).Charges⊢ 2 * (B i 9 * S 9 - B i 10 * S 10) = 0
  fin_cases i«0»S:(SM 3).Chargeshi:3 ≠ (fun i => i) ⟨0, ⋯⟩⊢ 2 * (B ((fun i => i) ⟨0, ⋯⟩) 9 * S 9 - B ((fun i => i) ⟨0, ⋯⟩) 10 * S 10) = 0«1»S:(SM 3).Chargeshi:3 ≠ (fun i => i) ⟨1, ⋯⟩⊢ 2 * (B ((fun i => i) ⟨1, ⋯⟩) 9 * S 9 - B ((fun i => i) ⟨1, ⋯⟩) 10 * S 10) = 0«2»S:(SM 3).Chargeshi:3 ≠ (fun i => i) ⟨2, ⋯⟩⊢ 2 * (B ((fun i => i) ⟨2, ⋯⟩) 9 * S 9 - B ((fun i => i) ⟨2, ⋯⟩) 10 * S 10) = 0«3»S:(SM 3).Chargeshi:3 ≠ (fun i => i) ⟨3, ⋯⟩⊢ 2 * (B ((fun i => i) ⟨3, ⋯⟩) 9 * S 9 - B ((fun i => i) ⟨3, ⋯⟩) 10 * S 10) = 0«4»S:(SM 3).Chargeshi:3 ≠ (fun i => i) ⟨4, ⋯⟩⊢ 2 * (B ((fun i => i) ⟨4, ⋯⟩) 9 * S 9 - B ((fun i => i) ⟨4, ⋯⟩) 10 * S 10) = 0«5»S:(SM 3).Chargeshi:3 ≠ (fun i => i) ⟨5, ⋯⟩⊢ 2 * (B ((fun i => i) ⟨5, ⋯⟩) 9 * S 9 - B ((fun i => i) ⟨5, ⋯⟩) 10 * S 10) = 0«6»S:(SM 3).Chargeshi:3 ≠ (fun i => i) ⟨6, ⋯⟩⊢ 2 * (B ((fun i => i) ⟨6, ⋯⟩) 9 * S 9 - B ((fun i => i) ⟨6, ⋯⟩) 10 * S 10) = 0 <;>«0»S:(SM 3).Chargeshi:3 ≠ (fun i => i) ⟨0, ⋯⟩⊢ 2 * (B ((fun i => i) ⟨0, ⋯⟩) 9 * S 9 - B ((fun i => i) ⟨0, ⋯⟩) 10 * S 10) = 0«1»S:(SM 3).Chargeshi:3 ≠ (fun i => i) ⟨1, ⋯⟩⊢ 2 * (B ((fun i => i) ⟨1, ⋯⟩) 9 * S 9 - B ((fun i => i) ⟨1, ⋯⟩) 10 * S 10) = 0«2»S:(SM 3).Chargeshi:3 ≠ (fun i => i) ⟨2, ⋯⟩⊢ 2 * (B ((fun i => i) ⟨2, ⋯⟩) 9 * S 9 - B ((fun i => i) ⟨2, ⋯⟩) 10 * S 10) = 0«3»S:(SM 3).Chargeshi:3 ≠ (fun i => i) ⟨3, ⋯⟩⊢ 2 * (B ((fun i => i) ⟨3, ⋯⟩) 9 * S 9 - B ((fun i => i) ⟨3, ⋯⟩) 10 * S 10) = 0«4»S:(SM 3).Chargeshi:3 ≠ (fun i => i) ⟨4, ⋯⟩⊢ 2 * (B ((fun i => i) ⟨4, ⋯⟩) 9 * S 9 - B ((fun i => i) ⟨4, ⋯⟩) 10 * S 10) = 0«5»S:(SM 3).Chargeshi:3 ≠ (fun i => i) ⟨5, ⋯⟩⊢ 2 * (B ((fun i => i) ⟨5, ⋯⟩) 9 * S 9 - B ((fun i => i) ⟨5, ⋯⟩) 10 * S 10) = 0«6»S:(SM 3).Chargeshi:3 ≠ (fun i => i) ⟨6, ⋯⟩⊢ 2 * (B ((fun i => i) ⟨6, ⋯⟩) 9 * S 9 - B ((fun i => i) ⟨6, ⋯⟩) 10 * S 10) = 0
    first | exact absurd rfl hi«6»S:(SM 3).Chargeshi:3 ≠ (fun i => i) ⟨6, ⋯⟩⊢ 2 * (B ((fun i => i) ⟨6, ⋯⟩) 9 * S 9 - B ((fun i => i) ⟨6, ⋯⟩) 10 * S 10) = 0 | simp [B₀, B₁, B₂, B₄, B₅, B₆, Fin.divNat, Fin.modNat]All goals completed! 🐙

lemma B₄_Bi_cubic {i : Fin 7} (hi : 4 ≠ i) (S : (SM 3).Charges) :
    cubeTriLin (B 4) (B i) S = 0 := byi:Fin 7hi:4 ≠ iS:(SM 3).Charges⊢ ((cubeTriLin (B 4)) (B i)) S = 0
  change cubeTriLin (B₄) (B i) S = 0i:Fin 7hi:4 ≠ iS:(SM 3).Charges⊢ ((cubeTriLin B₄) (B i)) S = 0
  rw [B₄_cubici:Fin 7hi:4 ≠ iS:(SM 3).Charges⊢ B i 12 * S 12 - B i 13 * S 13 = 0i:Fin 7hi:4 ≠ iS:(SM 3).Charges⊢ B i 12 * S 12 - B i 13 * S 13 = 0]i:Fin 7hi:4 ≠ iS:(SM 3).Charges⊢ B i 12 * S 12 - B i 13 * S 13 = 0
  fin_cases i«0»S:(SM 3).Chargeshi:4 ≠ (fun i => i) ⟨0, ⋯⟩⊢ B ((fun i => i) ⟨0, ⋯⟩) 12 * S 12 - B ((fun i => i) ⟨0, ⋯⟩) 13 * S 13 = 0«1»S:(SM 3).Chargeshi:4 ≠ (fun i => i) ⟨1, ⋯⟩⊢ B ((fun i => i) ⟨1, ⋯⟩) 12 * S 12 - B ((fun i => i) ⟨1, ⋯⟩) 13 * S 13 = 0«2»S:(SM 3).Chargeshi:4 ≠ (fun i => i) ⟨2, ⋯⟩⊢ B ((fun i => i) ⟨2, ⋯⟩) 12 * S 12 - B ((fun i => i) ⟨2, ⋯⟩) 13 * S 13 = 0«3»S:(SM 3).Chargeshi:4 ≠ (fun i => i) ⟨3, ⋯⟩⊢ B ((fun i => i) ⟨3, ⋯⟩) 12 * S 12 - B ((fun i => i) ⟨3, ⋯⟩) 13 * S 13 = 0«4»S:(SM 3).Chargeshi:4 ≠ (fun i => i) ⟨4, ⋯⟩⊢ B ((fun i => i) ⟨4, ⋯⟩) 12 * S 12 - B ((fun i => i) ⟨4, ⋯⟩) 13 * S 13 = 0«5»S:(SM 3).Chargeshi:4 ≠ (fun i => i) ⟨5, ⋯⟩⊢ B ((fun i => i) ⟨5, ⋯⟩) 12 * S 12 - B ((fun i => i) ⟨5, ⋯⟩) 13 * S 13 = 0«6»S:(SM 3).Chargeshi:4 ≠ (fun i => i) ⟨6, ⋯⟩⊢ B ((fun i => i) ⟨6, ⋯⟩) 12 * S 12 - B ((fun i => i) ⟨6, ⋯⟩) 13 * S 13 = 0 <;>«0»S:(SM 3).Chargeshi:4 ≠ (fun i => i) ⟨0, ⋯⟩⊢ B ((fun i => i) ⟨0, ⋯⟩) 12 * S 12 - B ((fun i => i) ⟨0, ⋯⟩) 13 * S 13 = 0«1»S:(SM 3).Chargeshi:4 ≠ (fun i => i) ⟨1, ⋯⟩⊢ B ((fun i => i) ⟨1, ⋯⟩) 12 * S 12 - B ((fun i => i) ⟨1, ⋯⟩) 13 * S 13 = 0«2»S:(SM 3).Chargeshi:4 ≠ (fun i => i) ⟨2, ⋯⟩⊢ B ((fun i => i) ⟨2, ⋯⟩) 12 * S 12 - B ((fun i => i) ⟨2, ⋯⟩) 13 * S 13 = 0«3»S:(SM 3).Chargeshi:4 ≠ (fun i => i) ⟨3, ⋯⟩⊢ B ((fun i => i) ⟨3, ⋯⟩) 12 * S 12 - B ((fun i => i) ⟨3, ⋯⟩) 13 * S 13 = 0«4»S:(SM 3).Chargeshi:4 ≠ (fun i => i) ⟨4, ⋯⟩⊢ B ((fun i => i) ⟨4, ⋯⟩) 12 * S 12 - B ((fun i => i) ⟨4, ⋯⟩) 13 * S 13 = 0«5»S:(SM 3).Chargeshi:4 ≠ (fun i => i) ⟨5, ⋯⟩⊢ B ((fun i => i) ⟨5, ⋯⟩) 12 * S 12 - B ((fun i => i) ⟨5, ⋯⟩) 13 * S 13 = 0«6»S:(SM 3).Chargeshi:4 ≠ (fun i => i) ⟨6, ⋯⟩⊢ B ((fun i => i) ⟨6, ⋯⟩) 12 * S 12 - B ((fun i => i) ⟨6, ⋯⟩) 13 * S 13 = 0
    first | exact absurd rfl hi«6»S:(SM 3).Chargeshi:4 ≠ (fun i => i) ⟨6, ⋯⟩⊢ B ((fun i => i) ⟨6, ⋯⟩) 12 * S 12 - B ((fun i => i) ⟨6, ⋯⟩) 13 * S 13 = 0 | simp [B₀, B₁, B₂, B₃, B₅, B₆, Fin.divNat, Fin.modNat]All goals completed! 🐙

lemma B₅_Bi_cubic {i : Fin 7} (hi : 5 ≠ i) (S : (SM 3).Charges) :
    cubeTriLin (B 5) (B i) S = 0 := byi:Fin 7hi:5 ≠ iS:(SM 3).Charges⊢ ((cubeTriLin (B 5)) (B i)) S = 0
  change cubeTriLin (B₅) (B i) S = 0i:Fin 7hi:5 ≠ iS:(SM 3).Charges⊢ ((cubeTriLin B₅) (B i)) S = 0
  rw [B₅_cubici:Fin 7hi:5 ≠ iS:(SM 3).Charges⊢ B i 15 * S 15 - B i 16 * S 16 = 0i:Fin 7hi:5 ≠ iS:(SM 3).Charges⊢ B i 15 * S 15 - B i 16 * S 16 = 0]i:Fin 7hi:5 ≠ iS:(SM 3).Charges⊢ B i 15 * S 15 - B i 16 * S 16 = 0
  fin_cases i«0»S:(SM 3).Chargeshi:5 ≠ (fun i => i) ⟨0, ⋯⟩⊢ B ((fun i => i) ⟨0, ⋯⟩) 15 * S 15 - B ((fun i => i) ⟨0, ⋯⟩) 16 * S 16 = 0«1»S:(SM 3).Chargeshi:5 ≠ (fun i => i) ⟨1, ⋯⟩⊢ B ((fun i => i) ⟨1, ⋯⟩) 15 * S 15 - B ((fun i => i) ⟨1, ⋯⟩) 16 * S 16 = 0«2»S:(SM 3).Chargeshi:5 ≠ (fun i => i) ⟨2, ⋯⟩⊢ B ((fun i => i) ⟨2, ⋯⟩) 15 * S 15 - B ((fun i => i) ⟨2, ⋯⟩) 16 * S 16 = 0«3»S:(SM 3).Chargeshi:5 ≠ (fun i => i) ⟨3, ⋯⟩⊢ B ((fun i => i) ⟨3, ⋯⟩) 15 * S 15 - B ((fun i => i) ⟨3, ⋯⟩) 16 * S 16 = 0«4»S:(SM 3).Chargeshi:5 ≠ (fun i => i) ⟨4, ⋯⟩⊢ B ((fun i => i) ⟨4, ⋯⟩) 15 * S 15 - B ((fun i => i) ⟨4, ⋯⟩) 16 * S 16 = 0«5»S:(SM 3).Chargeshi:5 ≠ (fun i => i) ⟨5, ⋯⟩⊢ B ((fun i => i) ⟨5, ⋯⟩) 15 * S 15 - B ((fun i => i) ⟨5, ⋯⟩) 16 * S 16 = 0«6»S:(SM 3).Chargeshi:5 ≠ (fun i => i) ⟨6, ⋯⟩⊢ B ((fun i => i) ⟨6, ⋯⟩) 15 * S 15 - B ((fun i => i) ⟨6, ⋯⟩) 16 * S 16 = 0 <;>«0»S:(SM 3).Chargeshi:5 ≠ (fun i => i) ⟨0, ⋯⟩⊢ B ((fun i => i) ⟨0, ⋯⟩) 15 * S 15 - B ((fun i => i) ⟨0, ⋯⟩) 16 * S 16 = 0«1»S:(SM 3).Chargeshi:5 ≠ (fun i => i) ⟨1, ⋯⟩⊢ B ((fun i => i) ⟨1, ⋯⟩) 15 * S 15 - B ((fun i => i) ⟨1, ⋯⟩) 16 * S 16 = 0«2»S:(SM 3).Chargeshi:5 ≠ (fun i => i) ⟨2, ⋯⟩⊢ B ((fun i => i) ⟨2, ⋯⟩) 15 * S 15 - B ((fun i => i) ⟨2, ⋯⟩) 16 * S 16 = 0«3»S:(SM 3).Chargeshi:5 ≠ (fun i => i) ⟨3, ⋯⟩⊢ B ((fun i => i) ⟨3, ⋯⟩) 15 * S 15 - B ((fun i => i) ⟨3, ⋯⟩) 16 * S 16 = 0«4»S:(SM 3).Chargeshi:5 ≠ (fun i => i) ⟨4, ⋯⟩⊢ B ((fun i => i) ⟨4, ⋯⟩) 15 * S 15 - B ((fun i => i) ⟨4, ⋯⟩) 16 * S 16 = 0«5»S:(SM 3).Chargeshi:5 ≠ (fun i => i) ⟨5, ⋯⟩⊢ B ((fun i => i) ⟨5, ⋯⟩) 15 * S 15 - B ((fun i => i) ⟨5, ⋯⟩) 16 * S 16 = 0«6»S:(SM 3).Chargeshi:5 ≠ (fun i => i) ⟨6, ⋯⟩⊢ B ((fun i => i) ⟨6, ⋯⟩) 15 * S 15 - B ((fun i => i) ⟨6, ⋯⟩) 16 * S 16 = 0
    first | exact absurd rfl hi«6»S:(SM 3).Chargeshi:5 ≠ (fun i => i) ⟨6, ⋯⟩⊢ B ((fun i => i) ⟨6, ⋯⟩) 15 * S 15 - B ((fun i => i) ⟨6, ⋯⟩) 16 * S 16 = 0 | simp [B₀, B₁, B₂, B₃, B₄, B₆, Fin.divNat, Fin.modNat]All goals completed! 🐙

lemma B₆_Bi_cubic {i : Fin 7} (hi : 6 ≠ i) (S : (SM 3).Charges) :
    cubeTriLin (B 6) (B i) S = 0 := byi:Fin 7hi:6 ≠ iS:(SM 3).Charges⊢ ((cubeTriLin (B 6)) (B i)) S = 0
  change cubeTriLin (B₆) (B i) S = 0i:Fin 7hi:6 ≠ iS:(SM 3).Charges⊢ ((cubeTriLin B₆) (B i)) S = 0
  rw [B₆_cubici:Fin 7hi:6 ≠ iS:(SM 3).Charges⊢ 3 * (B i 5 * S 5 - B i 8 * S 8) = 0i:Fin 7hi:6 ≠ iS:(SM 3).Charges⊢ 3 * (B i 5 * S 5 - B i 8 * S 8) = 0]i:Fin 7hi:6 ≠ iS:(SM 3).Charges⊢ 3 * (B i 5 * S 5 - B i 8 * S 8) = 0
  fin_cases i«0»S:(SM 3).Chargeshi:6 ≠ (fun i => i) ⟨0, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨0, ⋯⟩) 5 * S 5 - B ((fun i => i) ⟨0, ⋯⟩) 8 * S 8) = 0«1»S:(SM 3).Chargeshi:6 ≠ (fun i => i) ⟨1, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨1, ⋯⟩) 5 * S 5 - B ((fun i => i) ⟨1, ⋯⟩) 8 * S 8) = 0«2»S:(SM 3).Chargeshi:6 ≠ (fun i => i) ⟨2, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨2, ⋯⟩) 5 * S 5 - B ((fun i => i) ⟨2, ⋯⟩) 8 * S 8) = 0«3»S:(SM 3).Chargeshi:6 ≠ (fun i => i) ⟨3, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨3, ⋯⟩) 5 * S 5 - B ((fun i => i) ⟨3, ⋯⟩) 8 * S 8) = 0«4»S:(SM 3).Chargeshi:6 ≠ (fun i => i) ⟨4, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨4, ⋯⟩) 5 * S 5 - B ((fun i => i) ⟨4, ⋯⟩) 8 * S 8) = 0«5»S:(SM 3).Chargeshi:6 ≠ (fun i => i) ⟨5, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨5, ⋯⟩) 5 * S 5 - B ((fun i => i) ⟨5, ⋯⟩) 8 * S 8) = 0«6»S:(SM 3).Chargeshi:6 ≠ (fun i => i) ⟨6, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨6, ⋯⟩) 5 * S 5 - B ((fun i => i) ⟨6, ⋯⟩) 8 * S 8) = 0 <;>«0»S:(SM 3).Chargeshi:6 ≠ (fun i => i) ⟨0, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨0, ⋯⟩) 5 * S 5 - B ((fun i => i) ⟨0, ⋯⟩) 8 * S 8) = 0«1»S:(SM 3).Chargeshi:6 ≠ (fun i => i) ⟨1, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨1, ⋯⟩) 5 * S 5 - B ((fun i => i) ⟨1, ⋯⟩) 8 * S 8) = 0«2»S:(SM 3).Chargeshi:6 ≠ (fun i => i) ⟨2, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨2, ⋯⟩) 5 * S 5 - B ((fun i => i) ⟨2, ⋯⟩) 8 * S 8) = 0«3»S:(SM 3).Chargeshi:6 ≠ (fun i => i) ⟨3, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨3, ⋯⟩) 5 * S 5 - B ((fun i => i) ⟨3, ⋯⟩) 8 * S 8) = 0«4»S:(SM 3).Chargeshi:6 ≠ (fun i => i) ⟨4, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨4, ⋯⟩) 5 * S 5 - B ((fun i => i) ⟨4, ⋯⟩) 8 * S 8) = 0«5»S:(SM 3).Chargeshi:6 ≠ (fun i => i) ⟨5, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨5, ⋯⟩) 5 * S 5 - B ((fun i => i) ⟨5, ⋯⟩) 8 * S 8) = 0«6»S:(SM 3).Chargeshi:6 ≠ (fun i => i) ⟨6, ⋯⟩⊢ 3 * (B ((fun i => i) ⟨6, ⋯⟩) 5 * S 5 - B ((fun i => i) ⟨6, ⋯⟩) 8 * S 8) = 0
    first | exact absurd rfl hiAll goals completed! 🐙 | simp [B₀, B₁, B₂, B₃, B₄, B₅, Fin.divNat, Fin.modNat]All goals completed! 🐙lemma Bi_Bj_ne_cubic {i j : Fin 7} (h : i ≠ j) (S : (SM 3).Charges) :
    cubeTriLin (B i) (B j) S = 0 := byi:Fin 7j:Fin 7h:i ≠ jS:(SM 3).Charges⊢ ((cubeTriLin (B i)) (B j)) S = 0
  fin_cases i«0»j:Fin 7S:(SM 3).Chargesh:(fun i => i) ⟨0, ⋯⟩ ≠ j⊢ ((cubeTriLin (B ((fun i => i) ⟨0, ⋯⟩))) (B j)) S = 0«1»j:Fin 7S:(SM 3).Chargesh:(fun i => i) ⟨1, ⋯⟩ ≠ j⊢ ((cubeTriLin (B ((fun i => i) ⟨1, ⋯⟩))) (B j)) S = 0«2»j:Fin 7S:(SM 3).Chargesh:(fun i => i) ⟨2, ⋯⟩ ≠ j⊢ ((cubeTriLin (B ((fun i => i) ⟨2, ⋯⟩))) (B j)) S = 0«3»j:Fin 7S:(SM 3).Chargesh:(fun i => i) ⟨3, ⋯⟩ ≠ j⊢ ((cubeTriLin (B ((fun i => i) ⟨3, ⋯⟩))) (B j)) S = 0«4»j:Fin 7S:(SM 3).Chargesh:(fun i => i) ⟨4, ⋯⟩ ≠ j⊢ ((cubeTriLin (B ((fun i => i) ⟨4, ⋯⟩))) (B j)) S = 0«5»j:Fin 7S:(SM 3).Chargesh:(fun i => i) ⟨5, ⋯⟩ ≠ j⊢ ((cubeTriLin (B ((fun i => i) ⟨5, ⋯⟩))) (B j)) S = 0«6»j:Fin 7S:(SM 3).Chargesh:(fun i => i) ⟨6, ⋯⟩ ≠ j⊢ ((cubeTriLin (B ((fun i => i) ⟨6, ⋯⟩))) (B j)) S = 0
  ·«0»j:Fin 7S:(SM 3).Chargesh:(fun i => i) ⟨0, ⋯⟩ ≠ j⊢ ((cubeTriLin (B ((fun i => i) ⟨0, ⋯⟩))) (B j)) S = 0 exact B₀_Bi_cubic h SAll goals completed! 🐙
  ·«1»j:Fin 7S:(SM 3).Chargesh:(fun i => i) ⟨1, ⋯⟩ ≠ j⊢ ((cubeTriLin (B ((fun i => i) ⟨1, ⋯⟩))) (B j)) S = 0 exact B₁_Bi_cubic h SAll goals completed! 🐙
  ·«2»j:Fin 7S:(SM 3).Chargesh:(fun i => i) ⟨2, ⋯⟩ ≠ j⊢ ((cubeTriLin (B ((fun i => i) ⟨2, ⋯⟩))) (B j)) S = 0 exact B₂_Bi_cubic h SAll goals completed! 🐙
  ·«3»j:Fin 7S:(SM 3).Chargesh:(fun i => i) ⟨3, ⋯⟩ ≠ j⊢ ((cubeTriLin (B ((fun i => i) ⟨3, ⋯⟩))) (B j)) S = 0 exact B₃_Bi_cubic h SAll goals completed! 🐙
  ·«4»j:Fin 7S:(SM 3).Chargesh:(fun i => i) ⟨4, ⋯⟩ ≠ j⊢ ((cubeTriLin (B ((fun i => i) ⟨4, ⋯⟩))) (B j)) S = 0 exact B₄_Bi_cubic h SAll goals completed! 🐙
  ·«5»j:Fin 7S:(SM 3).Chargesh:(fun i => i) ⟨5, ⋯⟩ ≠ j⊢ ((cubeTriLin (B ((fun i => i) ⟨5, ⋯⟩))) (B j)) S = 0 exact B₅_Bi_cubic h SAll goals completed! 🐙
  ·«6»j:Fin 7S:(SM 3).Chargesh:(fun i => i) ⟨6, ⋯⟩ ≠ j⊢ ((cubeTriLin (B ((fun i => i) ⟨6, ⋯⟩))) (B j)) S = 0 exact B₆_Bi_cubic h SAll goals completed! 🐙

lemma Bi_Bi_Bj_cubic (i j : Fin 7) :
    cubeTriLin (B i) (B i) (B j) = 0 := byi:Fin 7j:Fin 7⊢ ((cubeTriLin (B i)) (B i)) (B j) = 0
  rcases eq_or_ne i j with rfl | hijinli:Fin 7⊢ ((cubeTriLin (B i)) (B i)) (B i) = 0inri:Fin 7j:Fin 7hij:i ≠ j⊢ ((cubeTriLin (B i)) (B i)) (B j) = 0
  ·inli:Fin 7⊢ ((cubeTriLin (B i)) (B i)) (B i) = 0 with_unfolding_all decide +revertAll goals completed! 🐙
  ·inri:Fin 7j:Fin 7hij:i ≠ j⊢ ((cubeTriLin (B i)) (B i)) (B j) = 0 rw [cubeTriLin.swap₂inri:Fin 7j:Fin 7hij:i ≠ j⊢ ((cubeTriLin (B i)) (B j)) (B i) = 0inri:Fin 7j:Fin 7hij:i ≠ j⊢ ((cubeTriLin (B i)) (B j)) (B i) = 0]inri:Fin 7j:Fin 7hij:i ≠ j⊢ ((cubeTriLin (B i)) (B j)) (B i) = 0
    exact Bi_Bj_ne_cubic hij (B i)All goals completed! 🐙lemma Bi_Bj_Bk_cubic (i j k : Fin 7) :
    cubeTriLin (B i) (B j) (B k) = 0 := byi:Fin 7j:Fin 7k:Fin 7⊢ ((cubeTriLin (B i)) (B j)) (B k) = 0
  rcases eq_or_ne i j with rfl | hijinli:Fin 7k:Fin 7⊢ ((cubeTriLin (B i)) (B i)) (B k) = 0inri:Fin 7j:Fin 7k:Fin 7hij:i ≠ j⊢ ((cubeTriLin (B i)) (B j)) (B k) = 0
  ·inli:Fin 7k:Fin 7⊢ ((cubeTriLin (B i)) (B i)) (B k) = 0 exact Bi_Bi_Bj_cubic i kAll goals completed! 🐙
  ·inri:Fin 7j:Fin 7k:Fin 7hij:i ≠ j⊢ ((cubeTriLin (B i)) (B j)) (B k) = 0 exact Bi_Bj_ne_cubic hij (B k)All goals completed! 🐙

set_option backward.isDefEq.respectTransparency false in
theorem B_in_accCube (f : Fin 7 → ℚ) : accCube (∑ i, f i • B i) = 0 := byf:Fin 7 → ℚ⊢ accCube (∑ i, f i • B i) = 0
  change cubeTriLin _ _ _ = 0f:Fin 7 → ℚ⊢ ((cubeTriLin (∑ i, f i • B i)) (∑ i, f i • B i)) (∑ i, f i • B i) = 0
  rw [cubeTriLin.map_sum₁₂₃f:Fin 7 → ℚ⊢ ∑ i, ∑ k, ∑ l, ((cubeTriLin (f i • B i)) (f k • B k)) (f l • B l) = 0f:Fin 7 → ℚ⊢ ∑ i, ∑ k, ∑ l, ((cubeTriLin (f i • B i)) (f k • B k)) (f l • B l) = 0]f:Fin 7 → ℚ⊢ ∑ i, ∑ k, ∑ l, ((cubeTriLin (f i • B i)) (f k • B k)) (f l • B l) = 0
  apply Fintype.sum_eq_zero _ fun i ↦ Fintype.sum_eq_zero _ fun k ↦ Fintype.sum_eq_zero _ fun l ↦ ?_f:Fin 7 → ℚi:Fin 7k:Fin 7l:Fin 7⊢ ((cubeTriLin (f i • B i)) (f k • B k)) (f l • B l) = 0
  simp only [cubeTriLin.map_smul₁, cubeTriLin.map_smul₂, cubeTriLin.map_smul₃, Bi_Bj_Bk_cubic,
    mul_zero]All goals completed! 🐙set_option backward.isDefEq.respectTransparency false in
lemma B_sum_is_sol (f : Fin 7 → ℚ) : (SM 3).IsSolution (∑ i, f i • B i) :=
  ⟨chargeToAF (∑ i, f i • B i) (byf:Fin 7 → ℚ⊢ accGrav (∑ i, f i • B i) = 0
    simp only [map_sum, map_smul]f:Fin 7 → ℚ⊢ ∑ x, f x • accGrav (B x) = 0
    refine Fintype.sum_eq_zero _ fun i ↦ smul_eq_zero_of_right _ ?_f:Fin 7 → ℚi:Fin 7⊢ accGrav (B i) = 0
    with_unfolding_all decide +revertAll goals completed! 🐙)
    (byf:Fin 7 → ℚ⊢ accSU2 (∑ i, f i • B i) = 0
      simp only [map_sum, map_smul]f:Fin 7 → ℚ⊢ ∑ x, f x • accSU2 (B x) = 0
      refine Fintype.sum_eq_zero _ fun i ↦ smul_eq_zero_of_right _ ?_f:Fin 7 → ℚi:Fin 7⊢ accSU2 (B i) = 0
      with_unfolding_all decide +revertAll goals completed! 🐙)
    (byf:Fin 7 → ℚ⊢ accSU3 (∑ i, f i • B i) = 0
      simp only [map_sum, map_smul]f:Fin 7 → ℚ⊢ ∑ x, f x • accSU3 (B x) = 0
      refine Fintype.sum_eq_zero _ fun i ↦ smul_eq_zero_of_right _ ?_f:Fin 7 → ℚi:Fin 7⊢ accSU3 (B i) = 0
      with_unfolding_all decide +revertAll goals completed! 🐙)
    (B_in_accCube f), rfl⟩set_option backward.isDefEq.respectTransparency false in
theorem basis_linear_independent : LinearIndependent ℚ B := by⊢ LinearIndependent ℚ B
  refine Fintype.linearIndependent_iff.mpr fun f h ↦ ?_f:Fin 7 → ℚh:∑ i, f i • B i = 0⊢ ∀ (i : Fin 7), f i = 0
  have h0 := congrFun h (0 : Fin 18)f:Fin 7 → ℚh:∑ i, f i • B i = 0h0:(∑ i, f i • B i) 0 = 0 0⊢ ∀ (i : Fin 7), f i = 0
  have h1 := congrFun h (3 : Fin 18)f:Fin 7 → ℚh:∑ i, f i • B i = 0h0:(∑ i, f i • B i) 0 = 0 0h1:(∑ i, f i • B i) 3 = 0 3⊢ ∀ (i : Fin 7), f i = 0
  have h2 := congrFun h (6 : Fin 18)f:Fin 7 → ℚh:∑ i, f i • B i = 0h0:(∑ i, f i • B i) 0 = 0 0h1:(∑ i, f i • B i) 3 = 0 3h2:(∑ i, f i • B i) 6 = 0 6⊢ ∀ (i : Fin 7), f i = 0
  have h3 := congrFun h (9 : Fin 18)f:Fin 7 → ℚh:∑ i, f i • B i = 0h0:(∑ i, f i • B i) 0 = 0 0h1:(∑ i, f i • B i) 3 = 0 3h2:(∑ i, f i • B i) 6 = 0 6h3:(∑ i, f i • B i) 9 = 0 9⊢ ∀ (i : Fin 7), f i = 0
  have h4 := congrFun h (12 : Fin 18)f:Fin 7 → ℚh:∑ i, f i • B i = 0h0:(∑ i, f i • B i) 0 = 0 0h1:(∑ i, f i • B i) 3 = 0 3h2:(∑ i, f i • B i) 6 = 0 6h3:(∑ i, f i • B i) 9 = 0 9h4:(∑ i, f i • B i) 12 = 0 12⊢ ∀ (i : Fin 7), f i = 0
  have h5 := congrFun h (15 : Fin 18)f:Fin 7 → ℚh:∑ i, f i • B i = 0h0:(∑ i, f i • B i) 0 = 0 0h1:(∑ i, f i • B i) 3 = 0 3h2:(∑ i, f i • B i) 6 = 0 6h3:(∑ i, f i • B i) 9 = 0 9h4:(∑ i, f i • B i) 12 = 0 12h5:(∑ i, f i • B i) 15 = 0 15⊢ ∀ (i : Fin 7), f i = 0
  have h6 := congrFun h (5 : Fin 18)f:Fin 7 → ℚh:∑ i, f i • B i = 0h0:(∑ i, f i • B i) 0 = 0 0h1:(∑ i, f i • B i) 3 = 0 3h2:(∑ i, f i • B i) 6 = 0 6h3:(∑ i, f i • B i) 9 = 0 9h4:(∑ i, f i • B i) 12 = 0 12h5:(∑ i, f i • B i) 15 = 0 15h6:(∑ i, f i • B i) 5 = 0 5⊢ ∀ (i : Fin 7), f i = 0
  simp only [Fin.sum_univ_seven, B, B₀, B₁, B₂, B₃, B₄, B₅, B₆, HSMul.hSMul,
    ACCSystemCharges.chargesAddCommMonoid_add, ACCSystemCharges.chargesModule_smul, Fin.isValue,
    Equiv.invFun_as_coe, toSpeciesEquiv_symm_apply, Fin.divNat, Nat.reduceMul, Fin.coe_ofNat_eq_mod,
    Nat.zero_mod, Nat.zero_div, Fin.zero_eta, Fin.modNat, mul_one, mul_zero, add_zero,
    Nat.reduceMod, Nat.ofNat_pos, Nat.div_self, Fin.mk_one, Nat.mod_self, zero_add,
    Nat.reduceDiv, Fin.reduceFinMk] at h0 h1 h2 h3 h4 h5 h6f:Fin 7 → ℚh:∑ i, f i • B i = 0h0:f 0 = 0 0h1:f 1 = 0 3h2:f 2 = 0 6h3:f 3 = 0 9h4:f 4 = 0 12h5:f 5 = 0 15h6:f 6 = 0 5⊢ ∀ (i : Fin 7), f i = 0
  intro if:Fin 7 → ℚh:∑ i, f i • B i = 0h0:f 0 = 0 0h1:f 1 = 0 3h2:f 2 = 0 6h3:f 3 = 0 9h4:f 4 = 0 12h5:f 5 = 0 15h6:f 6 = 0 5i:Fin 7⊢ f i = 0
  fin_cases i«0»f:Fin 7 → ℚh:∑ i, f i • B i = 0h0:f 0 = 0 0h1:f 1 = 0 3h2:f 2 = 0 6h3:f 3 = 0 9h4:f 4 = 0 12h5:f 5 = 0 15h6:f 6 = 0 5⊢ f ((fun i => i) ⟨0, ⋯⟩) = 0«1»f:Fin 7 → ℚh:∑ i, f i • B i = 0h0:f 0 = 0 0h1:f 1 = 0 3h2:f 2 = 0 6h3:f 3 = 0 9h4:f 4 = 0 12h5:f 5 = 0 15h6:f 6 = 0 5⊢ f ((fun i => i) ⟨1, ⋯⟩) = 0«2»f:Fin 7 → ℚh:∑ i, f i • B i = 0h0:f 0 = 0 0h1:f 1 = 0 3h2:f 2 = 0 6h3:f 3 = 0 9h4:f 4 = 0 12h5:f 5 = 0 15h6:f 6 = 0 5⊢ f ((fun i => i) ⟨2, ⋯⟩) = 0«3»f:Fin 7 → ℚh:∑ i, f i • B i = 0h0:f 0 = 0 0h1:f 1 = 0 3h2:f 2 = 0 6h3:f 3 = 0 9h4:f 4 = 0 12h5:f 5 = 0 15h6:f 6 = 0 5⊢ f ((fun i => i) ⟨3, ⋯⟩) = 0«4»f:Fin 7 → ℚh:∑ i, f i • B i = 0h0:f 0 = 0 0h1:f 1 = 0 3h2:f 2 = 0 6h3:f 3 = 0 9h4:f 4 = 0 12h5:f 5 = 0 15h6:f 6 = 0 5⊢ f ((fun i => i) ⟨4, ⋯⟩) = 0«5»f:Fin 7 → ℚh:∑ i, f i • B i = 0h0:f 0 = 0 0h1:f 1 = 0 3h2:f 2 = 0 6h3:f 3 = 0 9h4:f 4 = 0 12h5:f 5 = 0 15h6:f 6 = 0 5⊢ f ((fun i => i) ⟨5, ⋯⟩) = 0«6»f:Fin 7 → ℚh:∑ i, f i • B i = 0h0:f 0 = 0 0h1:f 1 = 0 3h2:f 2 = 0 6h3:f 3 = 0 9h4:f 4 = 0 12h5:f 5 = 0 15h6:f 6 = 0 5⊢ f ((fun i => i) ⟨6, ⋯⟩) = 0 <;>«0»f:Fin 7 → ℚh:∑ i, f i • B i = 0h0:f 0 = 0 0h1:f 1 = 0 3h2:f 2 = 0 6h3:f 3 = 0 9h4:f 4 = 0 12h5:f 5 = 0 15h6:f 6 = 0 5⊢ f ((fun i => i) ⟨0, ⋯⟩) = 0«1»f:Fin 7 → ℚh:∑ i, f i • B i = 0h0:f 0 = 0 0h1:f 1 = 0 3h2:f 2 = 0 6h3:f 3 = 0 9h4:f 4 = 0 12h5:f 5 = 0 15h6:f 6 = 0 5⊢ f ((fun i => i) ⟨1, ⋯⟩) = 0«2»f:Fin 7 → ℚh:∑ i, f i • B i = 0h0:f 0 = 0 0h1:f 1 = 0 3h2:f 2 = 0 6h3:f 3 = 0 9h4:f 4 = 0 12h5:f 5 = 0 15h6:f 6 = 0 5⊢ f ((fun i => i) ⟨2, ⋯⟩) = 0«3»f:Fin 7 → ℚh:∑ i, f i • B i = 0h0:f 0 = 0 0h1:f 1 = 0 3h2:f 2 = 0 6h3:f 3 = 0 9h4:f 4 = 0 12h5:f 5 = 0 15h6:f 6 = 0 5⊢ f ((fun i => i) ⟨3, ⋯⟩) = 0«4»f:Fin 7 → ℚh:∑ i, f i • B i = 0h0:f 0 = 0 0h1:f 1 = 0 3h2:f 2 = 0 6h3:f 3 = 0 9h4:f 4 = 0 12h5:f 5 = 0 15h6:f 6 = 0 5⊢ f ((fun i => i) ⟨4, ⋯⟩) = 0«5»f:Fin 7 → ℚh:∑ i, f i • B i = 0h0:f 0 = 0 0h1:f 1 = 0 3h2:f 2 = 0 6h3:f 3 = 0 9h4:f 4 = 0 12h5:f 5 = 0 15h6:f 6 = 0 5⊢ f ((fun i => i) ⟨5, ⋯⟩) = 0«6»f:Fin 7 → ℚh:∑ i, f i • B i = 0h0:f 0 = 0 0h1:f 1 = 0 3h2:f 2 = 0 6h3:f 3 = 0 9h4:f 4 = 0 12h5:f 5 = 0 15h6:f 6 = 0 5⊢ f ((fun i => i) ⟨6, ⋯⟩) = 0 assumptionAll goals completed! 🐙theorem seven_dim_plane_exists : ∃ (B : Fin 7 → (SM 3).Charges),
    LinearIndependent ℚ B ∧ ∀ (f : Fin 7 → ℚ), (SM 3).IsSolution (∑ i, f i • B i) :=
  ⟨PlaneSeven.B, And.intro PlaneSeven.basis_linear_independent PlaneSeven.B_sum_is_sol⟩