Physlib.QFT.QED.AnomalyCancellation.Odd.Parameterization

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.QFT.QED.AnomalyCancellation.Odd.LineInCubic

Parameterization in odd case

Given maps g : Fin n → ℚ, f : Fin n → ℚ and a : ℚ we form a solution to the anomaly equations. We show that every solution can be got in this way, up to permutation, unless it is zero.

The main reference is:

https://arxiv.org/pdf/1912.04804.pdf

@[expose] public section

Given a g f : Fin n → ℚ and a a : ℚ we form a linear solution. We will later show that this can be extended to a complete solution.

def parameterizationAsLinear (g f : Fin n → ℚ) (a : ℚ) :
    (PureU1 (2 * n + 1)).LinSols :=
  a •
    ((accCubeTriLinSymm (Shifted.planeCharges f) (Shifted.planeCharges f)
        (Unshifted.planeCharges g)) • Unshifted.planeLinSols g +
      (- accCubeTriLinSymm (Unshifted.planeCharges g) (Unshifted.planeCharges g)
        (Shifted.planeCharges f)) • Shifted.planeLinSols f)



lemma parameterizationAsLinear_val (g f : Fin n → ℚ) (a : ℚ) :
    (parameterizationAsLinear g f a).val =
    a •
      ((accCubeTriLinSymm (Shifted.planeCharges f) (Shifted.planeCharges f)
          (Unshifted.planeCharges g)) • Unshifted.planeCharges g +
        (- accCubeTriLinSymm (Unshifted.planeCharges g) (Unshifted.planeCharges g)
          (Shifted.planeCharges f)) • Shifted.planeCharges f) := byn:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ (parameterizationAsLinear g f a).val =
  a •
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
        Unshifted.planeCharges g +
      -((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
        Shifted.planeCharges f)
  rw [parameterizationAsLinearn:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ (a •
      (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
          Unshifted.planeLinSols g +
        -((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
          Shifted.planeLinSols f)).val =
  a •
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
        Unshifted.planeCharges g +
      -((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
        Shifted.planeCharges f)n:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ (a •
      (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
          Unshifted.planeLinSols g +
        -((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
          Shifted.planeLinSols f)).val =
  a •
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
        Unshifted.planeCharges g +
      -((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
        Shifted.planeCharges f)]n:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ (a •
      (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
          Unshifted.planeLinSols g +
        -((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
          Shifted.planeLinSols f)).val =
  a •
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
        Unshifted.planeCharges g +
      -((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
        Shifted.planeCharges f)
  change a • (_ • (Unshifted.planeLinSols g).val + _ • (Shifted.planeLinSols f).val) = _n:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ a •
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
        (Unshifted.planeLinSols g).val +
      -((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
        (Shifted.planeLinSols f).val) =
  a •
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
        Unshifted.planeCharges g +
      -((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
        Shifted.planeCharges f)
  rw [Unshifted.planeLinSols_val,n:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ a •
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
        Unshifted.planeCharges g +
      -((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
        (Shifted.planeLinSols f).val) =
  a •
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
        Unshifted.planeCharges g +
      -((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
        Shifted.planeCharges f)All goals completed! 🐙 Shifted.planeLinSols_valn:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ a •
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
        Unshifted.planeCharges g +
      -((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
        Shifted.planeCharges f) =
  a •
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
        Unshifted.planeCharges g +
      -((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
        Shifted.planeCharges f)All goals completed! 🐙]All goals completed! 🐙

The parameterization satisfies the cubic ACC.

set_option backward.isDefEq.respectTransparency false in


lemma parameterizationCharge_cube (g f : Fin n → ℚ) (a : ℚ) :
    accCube (2 * n + 1) (parameterizationAsLinear g f a).val = 0 := byn:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ (accCube (2 * n + 1)) (parameterizationAsLinear g f a).val = 0
  change accCubeTriLinSymm.toCubic _ = 0n:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ accCubeTriLinSymm.toCubic (parameterizationAsLinear g f a).val = 0
  rw [parameterizationAsLinear_valn:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ accCubeTriLinSymm.toCubic
    (a •
      (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
          Unshifted.planeCharges g +
        -((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
          Shifted.planeCharges f)) =
  0n:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ accCubeTriLinSymm.toCubic
    (a •
      (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
          Unshifted.planeCharges g +
        -((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
          Shifted.planeCharges f)) =
  0]n:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ accCubeTriLinSymm.toCubic
    (a •
      (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
          Unshifted.planeCharges g +
        -((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
          Shifted.planeCharges f)) =
  0
  rw [HomogeneousCubic.map_smuln:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    accCubeTriLinSymm.toCubic
      (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
          Unshifted.planeCharges g +
        -((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
          Shifted.planeCharges f) =
  0n:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    accCubeTriLinSymm.toCubic
      (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
          Unshifted.planeCharges g +
        -((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
          Shifted.planeCharges f) =
  0]n:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    accCubeTriLinSymm.toCubic
      (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
          Unshifted.planeCharges g +
        -((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
          Shifted.planeCharges f) =
  0
  rw [TriLinearSymm.toCubic_addn:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (accCubeTriLinSymm.toCubic
            (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
              Unshifted.planeCharges g) +
          accCubeTriLinSymm.toCubic
            (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
              Shifted.planeCharges f) +
        3 *
          ((accCubeTriLinSymm
                (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
                  Unshifted.planeCharges g))
              (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
                Unshifted.planeCharges g))
            (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
              Shifted.planeCharges f) +
      3 *
        ((accCubeTriLinSymm
              (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
                Shifted.planeCharges f))
            (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
              Shifted.planeCharges f))
          (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
            Unshifted.planeCharges g)) =
  0n:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (accCubeTriLinSymm.toCubic
            (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
              Unshifted.planeCharges g) +
          accCubeTriLinSymm.toCubic
            (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
              Shifted.planeCharges f) +
        3 *
          ((accCubeTriLinSymm
                (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
                  Unshifted.planeCharges g))
              (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
                Unshifted.planeCharges g))
            (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
              Shifted.planeCharges f) +
      3 *
        ((accCubeTriLinSymm
              (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
                Shifted.planeCharges f))
            (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
              Shifted.planeCharges f))
          (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
            Unshifted.planeCharges g)) =
  0]n:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (accCubeTriLinSymm.toCubic
            (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
              Unshifted.planeCharges g) +
          accCubeTriLinSymm.toCubic
            (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
              Shifted.planeCharges f) +
        3 *
          ((accCubeTriLinSymm
                (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
                  Unshifted.planeCharges g))
              (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
                Unshifted.planeCharges g))
            (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
              Shifted.planeCharges f) +
      3 *
        ((accCubeTriLinSymm
              (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
                Shifted.planeCharges f))
            (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
              Shifted.planeCharges f))
          (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
            Unshifted.planeCharges g)) =
  0
  rw [HomogeneousCubic.map_smul,n:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) ^ 3 *
            accCubeTriLinSymm.toCubic (Unshifted.planeCharges g) +
          accCubeTriLinSymm.toCubic
            (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
              Shifted.planeCharges f) +
        3 *
          ((accCubeTriLinSymm
                (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
                  Unshifted.planeCharges g))
              (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
                Unshifted.planeCharges g))
            (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
              Shifted.planeCharges f) +
      3 *
        ((accCubeTriLinSymm
              (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
                Shifted.planeCharges f))
            (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
              Shifted.planeCharges f))
          (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
            Unshifted.planeCharges g)) =
  0n:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) ^ 3 *
            accCubeTriLinSymm.toCubic (Unshifted.planeCharges g) +
          (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f)) ^ 3 *
            accCubeTriLinSymm.toCubic (Shifted.planeCharges f) +
        3 *
          ((accCubeTriLinSymm
                (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
                  Unshifted.planeCharges g))
              (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
                Unshifted.planeCharges g))
            (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
              Shifted.planeCharges f) +
      3 *
        ((accCubeTriLinSymm
              (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
                Shifted.planeCharges f))
            (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
              Shifted.planeCharges f))
          (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
            Unshifted.planeCharges g)) =
  0 HomogeneousCubic.map_smuln:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) ^ 3 *
            accCubeTriLinSymm.toCubic (Unshifted.planeCharges g) +
          (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f)) ^ 3 *
            accCubeTriLinSymm.toCubic (Shifted.planeCharges f) +
        3 *
          ((accCubeTriLinSymm
                (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
                  Unshifted.planeCharges g))
              (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
                Unshifted.planeCharges g))
            (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
              Shifted.planeCharges f) +
      3 *
        ((accCubeTriLinSymm
              (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
                Shifted.planeCharges f))
            (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
              Shifted.planeCharges f))
          (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
            Unshifted.planeCharges g)) =
  0n:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) ^ 3 *
            accCubeTriLinSymm.toCubic (Unshifted.planeCharges g) +
          (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f)) ^ 3 *
            accCubeTriLinSymm.toCubic (Shifted.planeCharges f) +
        3 *
          ((accCubeTriLinSymm
                (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
                  Unshifted.planeCharges g))
              (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
                Unshifted.planeCharges g))
            (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
              Shifted.planeCharges f) +
      3 *
        ((accCubeTriLinSymm
              (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
                Shifted.planeCharges f))
            (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
              Shifted.planeCharges f))
          (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
            Unshifted.planeCharges g)) =
  0]n:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) ^ 3 *
            accCubeTriLinSymm.toCubic (Unshifted.planeCharges g) +
          (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f)) ^ 3 *
            accCubeTriLinSymm.toCubic (Shifted.planeCharges f) +
        3 *
          ((accCubeTriLinSymm
                (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
                  Unshifted.planeCharges g))
              (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
                Unshifted.planeCharges g))
            (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
              Shifted.planeCharges f) +
      3 *
        ((accCubeTriLinSymm
              (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
                Shifted.planeCharges f))
            (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
              Shifted.planeCharges f))
          (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
            Unshifted.planeCharges g)) =
  0
  erw [Unshifted.planeCharges_accCube g,n:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) ^ 3 * 0 +
          (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f)) ^ 3 *
            accCubeTriLinSymm.toCubic (Shifted.planeCharges f) +
        3 *
          ((accCubeTriLinSymm
                (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
                  Unshifted.planeCharges g))
              (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
                Unshifted.planeCharges g))
            (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
              Shifted.planeCharges f) +
      3 *
        ((accCubeTriLinSymm
              (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
                Shifted.planeCharges f))
            (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
              Shifted.planeCharges f))
          (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
            Unshifted.planeCharges g)) =
  0 Shifted.planeCharges_accCube fn:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) ^ 3 * 0 +
          (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f)) ^ 3 *
            0 +
        3 *
          ((accCubeTriLinSymm
                (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
                  Unshifted.planeCharges g))
              (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
                Unshifted.planeCharges g))
            (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
              Shifted.planeCharges f) +
      3 *
        ((accCubeTriLinSymm
              (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
                Shifted.planeCharges f))
            (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
              Shifted.planeCharges f))
          (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
            Unshifted.planeCharges g)) =
  0]n:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) ^ 3 * 0 +
          (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f)) ^ 3 *
            0 +
        3 *
          ((accCubeTriLinSymm
                (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
                  Unshifted.planeCharges g))
              (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
                Unshifted.planeCharges g))
            (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
              Shifted.planeCharges f) +
      3 *
        ((accCubeTriLinSymm
              (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
                Shifted.planeCharges f))
            (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
              Shifted.planeCharges f))
          (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
            Unshifted.planeCharges g)) =
  0
  rw [accCubeTriLinSymm.map_smul₁,n:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) ^ 3 * 0 +
          (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f)) ^ 3 *
            0 +
        3 *
          (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) *
            ((accCubeTriLinSymm (Unshifted.planeCharges g))
                (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
                  Unshifted.planeCharges g))
              (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
                Shifted.planeCharges f)) +
      3 *
        ((accCubeTriLinSymm
              (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
                Shifted.planeCharges f))
            (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
              Shifted.planeCharges f))
          (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
            Unshifted.planeCharges g)) =
  0n:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) ^ 3 * 0 +
          (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f)) ^ 3 *
            0 +
        3 *
          (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) *
            (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) *
              (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) *
                ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g))
                  (Shifted.planeCharges f)))) +
      3 *
        (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) *
          (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) *
            (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) *
              ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g))))) =
  0 accCubeTriLinSymm.map_smul₂,n:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) ^ 3 * 0 +
          (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f)) ^ 3 *
            0 +
        3 *
          (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) *
            (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) *
              ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g))
                (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
                  Shifted.planeCharges f))) +
      3 *
        ((accCubeTriLinSymm
              (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
                Shifted.planeCharges f))
            (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
              Shifted.planeCharges f))
          (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
            Unshifted.planeCharges g)) =
  0n:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) ^ 3 * 0 +
          (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f)) ^ 3 *
            0 +
        3 *
          (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) *
            (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) *
              (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) *
                ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g))
                  (Shifted.planeCharges f)))) +
      3 *
        (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) *
          (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) *
            (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) *
              ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g))))) =
  0
    accCubeTriLinSymm.map_smul₃,n:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) ^ 3 * 0 +
          (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f)) ^ 3 *
            0 +
        3 *
          (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) *
            (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) *
              (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) *
                ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g))
                  (Shifted.planeCharges f)))) +
      3 *
        ((accCubeTriLinSymm
              (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
                Shifted.planeCharges f))
            (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
              Shifted.planeCharges f))
          (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
            Unshifted.planeCharges g)) =
  0n:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) ^ 3 * 0 +
          (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f)) ^ 3 *
            0 +
        3 *
          (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) *
            (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) *
              (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) *
                ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g))
                  (Shifted.planeCharges f)))) +
      3 *
        (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) *
          (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) *
            (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) *
              ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g))))) =
  0 accCubeTriLinSymm.map_smul₁,n:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) ^ 3 * 0 +
          (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f)) ^ 3 *
            0 +
        3 *
          (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) *
            (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) *
              (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) *
                ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g))
                  (Shifted.planeCharges f)))) +
      3 *
        (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) *
          ((accCubeTriLinSymm (Shifted.planeCharges f))
              (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
                Shifted.planeCharges f))
            (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
              Unshifted.planeCharges g))) =
  0n:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) ^ 3 * 0 +
          (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f)) ^ 3 *
            0 +
        3 *
          (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) *
            (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) *
              (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) *
                ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g))
                  (Shifted.planeCharges f)))) +
      3 *
        (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) *
          (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) *
            (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) *
              ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g))))) =
  0 accCubeTriLinSymm.map_smul₂,n:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) ^ 3 * 0 +
          (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f)) ^ 3 *
            0 +
        3 *
          (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) *
            (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) *
              (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) *
                ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g))
                  (Shifted.planeCharges f)))) +
      3 *
        (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) *
          (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) *
            ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f))
              (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
                Unshifted.planeCharges g)))) =
  0n:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) ^ 3 * 0 +
          (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f)) ^ 3 *
            0 +
        3 *
          (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) *
            (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) *
              (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) *
                ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g))
                  (Shifted.planeCharges f)))) +
      3 *
        (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) *
          (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) *
            (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) *
              ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g))))) =
  0
    accCubeTriLinSymm.map_smul₃n:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) ^ 3 * 0 +
          (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f)) ^ 3 *
            0 +
        3 *
          (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) *
            (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) *
              (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) *
                ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g))
                  (Shifted.planeCharges f)))) +
      3 *
        (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) *
          (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) *
            (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) *
              ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g))))) =
  0n:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) ^ 3 * 0 +
          (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f)) ^ 3 *
            0 +
        3 *
          (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) *
            (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) *
              (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) *
                ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g))
                  (Shifted.planeCharges f)))) +
      3 *
        (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) *
          (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) *
            (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) *
              ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g))))) =
  0]n:ℕg:Fin n → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) ^ 3 * 0 +
          (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f)) ^ 3 *
            0 +
        3 *
          (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) *
            (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) *
              (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) *
                ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g))
                  (Shifted.planeCharges f)))) +
      3 *
        (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) *
          (-((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) *
            (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) *
              ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g))))) =
  0
  ringAll goals completed! 🐙

Given a g f : Fin n → ℚ and a a : ℚ we form a solution.

def parameterization (g f : Fin n → ℚ) (a : ℚ) :
    (PureU1 (2 * n + 1)).Sols :=
  ⟨⟨parameterizationAsLinear g f a, fun i => Fin.elim0 i⟩,
  parameterizationCharge_cube g f a⟩



lemma anomalyFree_param {S : (PureU1 (2 * n + 1)).Sols}
    (g f : Fin n → ℚ) (hS : S.val = Unshifted.planeCharges g + Shifted.planeCharges f) :
    accCubeTriLinSymm (Unshifted.planeCharges g) (Unshifted.planeCharges g)
      (Shifted.planeCharges f) =
    - accCubeTriLinSymm (Shifted.planeCharges f) (Shifted.planeCharges f)
      (Unshifted.planeCharges g) := byn:ℕS:(PureU1 (2 * n + 1)).Solsg:Fin n → ℚf:Fin n → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) =
  -((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g)
  have hC := S.cubicSoln:ℕS:(PureU1 (2 * n + 1)).Solsg:Fin n → ℚf:Fin n → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges fhC:(PureU1 (2 * n + 1)).cubicACC S.val = 0⊢ ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) =
  -((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g)
  rw [hSn:ℕS:(PureU1 (2 * n + 1)).Solsg:Fin n → ℚf:Fin n → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges fhC:(PureU1 (2 * n + 1)).cubicACC (Unshifted.planeCharges g + Shifted.planeCharges f) = 0⊢ ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) =
  -((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g)n:ℕS:(PureU1 (2 * n + 1)).Solsg:Fin n → ℚf:Fin n → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges fhC:(PureU1 (2 * n + 1)).cubicACC (Unshifted.planeCharges g + Shifted.planeCharges f) = 0⊢ ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) =
  -((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g)] at hCn:ℕS:(PureU1 (2 * n + 1)).Solsg:Fin n → ℚf:Fin n → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges fhC:(PureU1 (2 * n + 1)).cubicACC (Unshifted.planeCharges g + Shifted.planeCharges f) = 0⊢ ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) =
  -((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g)
  change (accCube (2 * n + 1)) (Unshifted.planeCharges g + Shifted.planeCharges f) = 0 at hCn:ℕS:(PureU1 (2 * n + 1)).Solsg:Fin n → ℚf:Fin n → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges fhC:(accCube (2 * n + 1)) (Unshifted.planeCharges g + Shifted.planeCharges f) = 0⊢ ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) =
  -((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g)
  erw [TriLinearSymm.toCubic_addn:ℕS:(PureU1 (2 * n + 1)).Solsg:Fin n → ℚf:Fin n → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges fhC:accCubeTriLinSymm.toCubic (Unshifted.planeCharges g) + accCubeTriLinSymm.toCubic (Shifted.planeCharges f) +
      3 * ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) +
    3 * ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) =
  0⊢ ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) =
  -((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g)]n:ℕS:(PureU1 (2 * n + 1)).Solsg:Fin n → ℚf:Fin n → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges fhC:accCubeTriLinSymm.toCubic (Unshifted.planeCharges g) + accCubeTriLinSymm.toCubic (Shifted.planeCharges f) +
      3 * ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) +
    3 * ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) =
  0⊢ ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) =
  -((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) at hC
  erw [Unshifted.planeCharges_accCuben:ℕS:(PureU1 (2 * n + 1)).Solsg:Fin n → ℚf:Fin n → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges fhC:0 + accCubeTriLinSymm.toCubic (Shifted.planeCharges f) +
      3 * ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) +
    3 * ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) =
  0⊢ ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) =
  -((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g)]n:ℕS:(PureU1 (2 * n + 1)).Solsg:Fin n → ℚf:Fin n → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges fhC:0 + accCubeTriLinSymm.toCubic (Shifted.planeCharges f) +
      3 * ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) +
    3 * ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) =
  0⊢ ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) =
  -((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) at hC
  erw [Shifted.planeCharges_accCuben:ℕS:(PureU1 (2 * n + 1)).Solsg:Fin n → ℚf:Fin n → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges fhC:0 + 0 + 3 * ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) +
    3 * ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) =
  0⊢ ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) =
  -((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g)]n:ℕS:(PureU1 (2 * n + 1)).Solsg:Fin n → ℚf:Fin n → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges fhC:0 + 0 + 3 * ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) +
    3 * ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) =
  0⊢ ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) =
  -((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) at hC
  linear_combination hC / 3All goals completed! 🐙

A proposition on a solution which is true if accCubeTriLinSymm (Unshifted.planeCharges g, Unshifted.planeCharges g, Shifted.planeCharges f) ≠ 0. In this case our parameterization above will be able to recover this point.

def GenericCase (S : (PureU1 (2 * n.succ + 1)).Sols) : Prop :=
  ∀ (g f : Fin n.succ → ℚ)
    (_ : S.val = Unshifted.planeCharges g + Shifted.planeCharges f),
  accCubeTriLinSymm (Unshifted.planeCharges g) (Unshifted.planeCharges g)
    (Shifted.planeCharges f) ≠ 0



lemma genericCase_exists (S : (PureU1 (2 * n.succ + 1)).Sols)
    (hs : ∃ (g f : Fin n.succ → ℚ),
      S.val = Unshifted.planeCharges g + Shifted.planeCharges f ∧
      accCubeTriLinSymm (Unshifted.planeCharges g) (Unshifted.planeCharges g)
        (Shifted.planeCharges f) ≠ 0) : GenericCase S := byn:ℕS:(PureU1 (2 * n.succ + 1)).Solshs:∃ g f,
  S.val = Unshifted.planeCharges g + Shifted.planeCharges f ∧
    ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) ≠ 0⊢ GenericCase S
  intro g f hS hCn:ℕS:(PureU1 (2 * n.succ + 1)).Solshs:∃ g f,
  S.val = Unshifted.planeCharges g + Shifted.planeCharges f ∧
    ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) ≠ 0g:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges fhC:((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0⊢ False
  obtain ⟨g', f', hS', hC'⟩ := hsn:ℕS:(PureU1 (2 * n.succ + 1)).Solsg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges fhC:((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0g':Fin n.succ → ℚf':Fin n.succ → ℚhS':S.val = Unshifted.planeCharges g' + Shifted.planeCharges f'hC':((accCubeTriLinSymm (Unshifted.planeCharges g')) (Unshifted.planeCharges g')) (Shifted.planeCharges f') ≠ 0⊢ False
  rw [hSn:ℕS:(PureU1 (2 * n.succ + 1)).Solsg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges fhC:((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0g':Fin n.succ → ℚf':Fin n.succ → ℚhS':Unshifted.planeCharges g + Shifted.planeCharges f = Unshifted.planeCharges g' + Shifted.planeCharges f'hC':((accCubeTriLinSymm (Unshifted.planeCharges g')) (Unshifted.planeCharges g')) (Shifted.planeCharges f') ≠ 0⊢ Falsen:ℕS:(PureU1 (2 * n.succ + 1)).Solsg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges fhC:((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0g':Fin n.succ → ℚf':Fin n.succ → ℚhS':Unshifted.planeCharges g + Shifted.planeCharges f = Unshifted.planeCharges g' + Shifted.planeCharges f'hC':((accCubeTriLinSymm (Unshifted.planeCharges g')) (Unshifted.planeCharges g')) (Shifted.planeCharges f') ≠ 0⊢ False] at hS'n:ℕS:(PureU1 (2 * n.succ + 1)).Solsg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges fhC:((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0g':Fin n.succ → ℚf':Fin n.succ → ℚhS':Unshifted.planeCharges g + Shifted.planeCharges f = Unshifted.planeCharges g' + Shifted.planeCharges f'hC':((accCubeTriLinSymm (Unshifted.planeCharges g')) (Unshifted.planeCharges g')) (Shifted.planeCharges f') ≠ 0⊢ False
  erw [Pa_eqn:ℕS:(PureU1 (2 * n.succ + 1)).Solsg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges fhC:((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0g':Fin n.succ → ℚf':Fin n.succ → ℚhS':g = g' ∧ f = f'hC':((accCubeTriLinSymm (Unshifted.planeCharges g')) (Unshifted.planeCharges g')) (Shifted.planeCharges f') ≠ 0⊢ False]n:ℕS:(PureU1 (2 * n.succ + 1)).Solsg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges fhC:((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0g':Fin n.succ → ℚf':Fin n.succ → ℚhS':g = g' ∧ f = f'hC':((accCubeTriLinSymm (Unshifted.planeCharges g')) (Unshifted.planeCharges g')) (Shifted.planeCharges f') ≠ 0⊢ False at hS'
  rw [hS'.1,n:ℕS:(PureU1 (2 * n.succ + 1)).Solsg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges fg':Fin n.succ → ℚhC:((accCubeTriLinSymm (Unshifted.planeCharges g')) (Unshifted.planeCharges g')) (Shifted.planeCharges f) = 0f':Fin n.succ → ℚhS':g = g' ∧ f = f'hC':((accCubeTriLinSymm (Unshifted.planeCharges g')) (Unshifted.planeCharges g')) (Shifted.planeCharges f') ≠ 0⊢ Falsen:ℕS:(PureU1 (2 * n.succ + 1)).Solsg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges fg':Fin n.succ → ℚf':Fin n.succ → ℚhC:((accCubeTriLinSymm (Unshifted.planeCharges g')) (Unshifted.planeCharges g')) (Shifted.planeCharges f') = 0hS':g = g' ∧ f = f'hC':((accCubeTriLinSymm (Unshifted.planeCharges g')) (Unshifted.planeCharges g')) (Shifted.planeCharges f') ≠ 0⊢ False hS'.2n:ℕS:(PureU1 (2 * n.succ + 1)).Solsg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges fg':Fin n.succ → ℚf':Fin n.succ → ℚhC:((accCubeTriLinSymm (Unshifted.planeCharges g')) (Unshifted.planeCharges g')) (Shifted.planeCharges f') = 0hS':g = g' ∧ f = f'hC':((accCubeTriLinSymm (Unshifted.planeCharges g')) (Unshifted.planeCharges g')) (Shifted.planeCharges f') ≠ 0⊢ Falsen:ℕS:(PureU1 (2 * n.succ + 1)).Solsg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges fg':Fin n.succ → ℚf':Fin n.succ → ℚhC:((accCubeTriLinSymm (Unshifted.planeCharges g')) (Unshifted.planeCharges g')) (Shifted.planeCharges f') = 0hS':g = g' ∧ f = f'hC':((accCubeTriLinSymm (Unshifted.planeCharges g')) (Unshifted.planeCharges g')) (Shifted.planeCharges f') ≠ 0⊢ False] at hCn:ℕS:(PureU1 (2 * n.succ + 1)).Solsg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges fg':Fin n.succ → ℚf':Fin n.succ → ℚhC:((accCubeTriLinSymm (Unshifted.planeCharges g')) (Unshifted.planeCharges g')) (Shifted.planeCharges f') = 0hS':g = g' ∧ f = f'hC':((accCubeTriLinSymm (Unshifted.planeCharges g')) (Unshifted.planeCharges g')) (Shifted.planeCharges f') ≠ 0⊢ False
  exact hC' hCAll goals completed! 🐙

A proposition on a solution which is true if accCubeTriLinSymm (Unshifted.planeCharges g, Unshifted.planeCharges g, Shifted.planeCharges f) ≠ 0. In this case we will show that S is zero if it is true for all permutations.

def SpecialCase (S : (PureU1 (2 * n.succ + 1)).Sols) : Prop :=
  ∀ (g f : Fin n.succ → ℚ)
    (_ : S.val = Unshifted.planeCharges g + Shifted.planeCharges f),
  accCubeTriLinSymm (Unshifted.planeCharges g) (Unshifted.planeCharges g)
    (Shifted.planeCharges f) = 0

              

lemma specialCase_exists (S : (PureU1 (2 * n.succ + 1)).Sols)
    (hs : ∃ (g f : Fin n.succ → ℚ),
      S.val = Unshifted.planeCharges g + Shifted.planeCharges f ∧
      accCubeTriLinSymm (Unshifted.planeCharges g) (Unshifted.planeCharges g)
        (Shifted.planeCharges f) = 0) : SpecialCase S := byn:ℕS:(PureU1 (2 * n.succ + 1)).Solshs:∃ g f,
  S.val = Unshifted.planeCharges g + Shifted.planeCharges f ∧
    ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0⊢ SpecialCase S
  intro g f hSn:ℕS:(PureU1 (2 * n.succ + 1)).Solshs:∃ g f,
  S.val = Unshifted.planeCharges g + Shifted.planeCharges f ∧
    ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0g:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0
  obtain ⟨g', f', hS', hC'⟩ := hsn:ℕS:(PureU1 (2 * n.succ + 1)).Solsg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges fg':Fin n.succ → ℚf':Fin n.succ → ℚhS':S.val = Unshifted.planeCharges g' + Shifted.planeCharges f'hC':((accCubeTriLinSymm (Unshifted.planeCharges g')) (Unshifted.planeCharges g')) (Shifted.planeCharges f') = 0⊢ ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0
  rw [hSn:ℕS:(PureU1 (2 * n.succ + 1)).Solsg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges fg':Fin n.succ → ℚf':Fin n.succ → ℚhS':Unshifted.planeCharges g + Shifted.planeCharges f = Unshifted.planeCharges g' + Shifted.planeCharges f'hC':((accCubeTriLinSymm (Unshifted.planeCharges g')) (Unshifted.planeCharges g')) (Shifted.planeCharges f') = 0⊢ ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0n:ℕS:(PureU1 (2 * n.succ + 1)).Solsg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges fg':Fin n.succ → ℚf':Fin n.succ → ℚhS':Unshifted.planeCharges g + Shifted.planeCharges f = Unshifted.planeCharges g' + Shifted.planeCharges f'hC':((accCubeTriLinSymm (Unshifted.planeCharges g')) (Unshifted.planeCharges g')) (Shifted.planeCharges f') = 0⊢ ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0] at hS'n:ℕS:(PureU1 (2 * n.succ + 1)).Solsg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges fg':Fin n.succ → ℚf':Fin n.succ → ℚhS':Unshifted.planeCharges g + Shifted.planeCharges f = Unshifted.planeCharges g' + Shifted.planeCharges f'hC':((accCubeTriLinSymm (Unshifted.planeCharges g')) (Unshifted.planeCharges g')) (Shifted.planeCharges f') = 0⊢ ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0
  erw [Pa_eqn:ℕS:(PureU1 (2 * n.succ + 1)).Solsg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges fg':Fin n.succ → ℚf':Fin n.succ → ℚhS':g = g' ∧ f = f'hC':((accCubeTriLinSymm (Unshifted.planeCharges g')) (Unshifted.planeCharges g')) (Shifted.planeCharges f') = 0⊢ ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0]n:ℕS:(PureU1 (2 * n.succ + 1)).Solsg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges fg':Fin n.succ → ℚf':Fin n.succ → ℚhS':g = g' ∧ f = f'hC':((accCubeTriLinSymm (Unshifted.planeCharges g')) (Unshifted.planeCharges g')) (Shifted.planeCharges f') = 0⊢ ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0 at hS'
  rw [hS'.1,n:ℕS:(PureU1 (2 * n.succ + 1)).Solsg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges fg':Fin n.succ → ℚf':Fin n.succ → ℚhS':g = g' ∧ f = f'hC':((accCubeTriLinSymm (Unshifted.planeCharges g')) (Unshifted.planeCharges g')) (Shifted.planeCharges f') = 0⊢ ((accCubeTriLinSymm (Unshifted.planeCharges g')) (Unshifted.planeCharges g')) (Shifted.planeCharges f) = 0n:ℕS:(PureU1 (2 * n.succ + 1)).Solsg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges fg':Fin n.succ → ℚf':Fin n.succ → ℚhS':g = g' ∧ f = f'hC':((accCubeTriLinSymm (Unshifted.planeCharges g')) (Unshifted.planeCharges g')) (Shifted.planeCharges f') = 0⊢ ((accCubeTriLinSymm (Unshifted.planeCharges g')) (Unshifted.planeCharges g')) (Shifted.planeCharges f') = 0 hS'.2n:ℕS:(PureU1 (2 * n.succ + 1)).Solsg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges fg':Fin n.succ → ℚf':Fin n.succ → ℚhS':g = g' ∧ f = f'hC':((accCubeTriLinSymm (Unshifted.planeCharges g')) (Unshifted.planeCharges g')) (Shifted.planeCharges f') = 0⊢ ((accCubeTriLinSymm (Unshifted.planeCharges g')) (Unshifted.planeCharges g')) (Shifted.planeCharges f') = 0n:ℕS:(PureU1 (2 * n.succ + 1)).Solsg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges fg':Fin n.succ → ℚf':Fin n.succ → ℚhS':g = g' ∧ f = f'hC':((accCubeTriLinSymm (Unshifted.planeCharges g')) (Unshifted.planeCharges g')) (Shifted.planeCharges f') = 0⊢ ((accCubeTriLinSymm (Unshifted.planeCharges g')) (Unshifted.planeCharges g')) (Shifted.planeCharges f') = 0]n:ℕS:(PureU1 (2 * n.succ + 1)).Solsg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges fg':Fin n.succ → ℚf':Fin n.succ → ℚhS':g = g' ∧ f = f'hC':((accCubeTriLinSymm (Unshifted.planeCharges g')) (Unshifted.planeCharges g')) (Shifted.planeCharges f') = 0⊢ ((accCubeTriLinSymm (Unshifted.planeCharges g')) (Unshifted.planeCharges g')) (Shifted.planeCharges f') = 0
  exact hC'All goals completed! 🐙

lemma generic_or_special (S : (PureU1 (2 * n.succ + 1)).Sols) :
    GenericCase S ∨ SpecialCase S := byn:ℕS:(PureU1 (2 * n.succ + 1)).Sols⊢ GenericCase S ∨ SpecialCase S
  obtain ⟨g, f, h⟩ := span_basis S.1.1n:ℕS:(PureU1 (2 * n.succ + 1)).Solsg:Fin n.succ → ℚf:Fin n.succ → ℚh:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ GenericCase S ∨ SpecialCase S
  have h1 :
      accCubeTriLinSymm (Unshifted.planeCharges g) (Unshifted.planeCharges g)
        (Shifted.planeCharges f) ≠ 0 ∨
      accCubeTriLinSymm (Unshifted.planeCharges g) (Unshifted.planeCharges g)
        (Shifted.planeCharges f) = 0 := by
    exact ne_or_eq _ _n:ℕS:(PureU1 (2 * n.succ + 1)).Solsg:Fin n.succ → ℚf:Fin n.succ → ℚh:S.val = Unshifted.planeCharges g + Shifted.planeCharges fh1:((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) ≠ 0 ∨
  ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0⊢ GenericCase S ∨ SpecialCase Sn:ℕS:(PureU1 (2 * n.succ + 1)).Solsg:Fin n.succ → ℚf:Fin n.succ → ℚh:S.val = Unshifted.planeCharges g + Shifted.planeCharges fh1:((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) ≠ 0 ∨
  ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0⊢ GenericCase S ∨ SpecialCase S
  cases h1inln:ℕS:(PureU1 (2 * n.succ + 1)).Solsg:Fin n.succ → ℚf:Fin n.succ → ℚh:S.val = Unshifted.planeCharges g + Shifted.planeCharges fh✝:((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) ≠ 0⊢ GenericCase S ∨ SpecialCase Sinrn:ℕS:(PureU1 (2 * n.succ + 1)).Solsg:Fin n.succ → ℚf:Fin n.succ → ℚh:S.val = Unshifted.planeCharges g + Shifted.planeCharges fh✝:((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0⊢ GenericCase S ∨ SpecialCase S <;>inln:ℕS:(PureU1 (2 * n.succ + 1)).Solsg:Fin n.succ → ℚf:Fin n.succ → ℚh:S.val = Unshifted.planeCharges g + Shifted.planeCharges fh✝:((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) ≠ 0⊢ GenericCase S ∨ SpecialCase Sinrn:ℕS:(PureU1 (2 * n.succ + 1)).Solsg:Fin n.succ → ℚf:Fin n.succ → ℚh:S.val = Unshifted.planeCharges g + Shifted.planeCharges fh✝:((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0⊢ GenericCase S ∨ SpecialCase S rename_i h1inrn:ℕS:(PureU1 (2 * n.succ + 1)).Solsg:Fin n.succ → ℚf:Fin n.succ → ℚh:S.val = Unshifted.planeCharges g + Shifted.planeCharges fh1:((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0⊢ GenericCase S ∨ SpecialCase S
  ·inln:ℕS:(PureU1 (2 * n.succ + 1)).Solsg:Fin n.succ → ℚf:Fin n.succ → ℚh:S.val = Unshifted.planeCharges g + Shifted.planeCharges fh1:((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) ≠ 0⊢ GenericCase S ∨ SpecialCase S exact Or.inl (genericCase_exists S ⟨g, f, h, h1⟩)All goals completed! 🐙
  ·inrn:ℕS:(PureU1 (2 * n.succ + 1)).Solsg:Fin n.succ → ℚf:Fin n.succ → ℚh:S.val = Unshifted.planeCharges g + Shifted.planeCharges fh1:((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0⊢ GenericCase S ∨ SpecialCase S exact Or.inr (specialCase_exists S ⟨g, f, h, h1⟩)All goals completed! 🐙

theorem generic_case {S : (PureU1 (2 * n.succ + 1)).Sols} (h : GenericCase S) :
    ∃ g f a, S = parameterization g f a := byn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:GenericCase S⊢ ∃ g f a, S = parameterization g f a
  obtain ⟨g, f, hS⟩ := span_basis S.1.1n:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ ∃ g f a, S = parameterization g f a
  use g, f,
    (accCubeTriLinSymm (Shifted.planeCharges f) (Shifted.planeCharges f)
      (Unshifted.planeCharges g))⁻¹hn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ S =
  parameterization g f
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g))⁻¹
  rw [parameterizationhn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ S =
  {
    toLinSols :=
      parameterizationAsLinear g f
        (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g))⁻¹,
    quadSol := ⋯, cubicSol := ⋯ }hn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ S =
  {
    toLinSols :=
      parameterizationAsLinear g f
        (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g))⁻¹,
    quadSol := ⋯, cubicSol := ⋯ }]hn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ S =
  {
    toLinSols :=
      parameterizationAsLinear g f
        (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g))⁻¹,
    quadSol := ⋯, cubicSol := ⋯ }
  apply ACCSystem.Sols.exthn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ S.val =
  {
      toLinSols :=
        parameterizationAsLinear g f
          (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g))⁻¹,
      quadSol := ⋯, cubicSol := ⋯ }.val
  rw [parameterizationAsLinear_valhn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ S.val =
  (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g))⁻¹ •
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
        Unshifted.planeCharges g +
      -((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
        Shifted.planeCharges f)hn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ S.val =
  (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g))⁻¹ •
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
        Unshifted.planeCharges g +
      -((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
        Shifted.planeCharges f)]hn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ S.val =
  (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g))⁻¹ •
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
        Unshifted.planeCharges g +
      -((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) •
        Shifted.planeCharges f)
  rw [anomalyFree_param _ _ hS,hn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ S.val =
  (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g))⁻¹ •
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
        Unshifted.planeCharges g +
      - -((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
        Shifted.planeCharges f)hn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ S.val = Unshifted.planeCharges g + Shifted.planeCharges fhn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) ≠ 0 neg_neg,hn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ S.val =
  (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g))⁻¹ •
    (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
        Unshifted.planeCharges g +
      ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
        Shifted.planeCharges f)hn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ S.val = Unshifted.planeCharges g + Shifted.planeCharges fhn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) ≠ 0 ← smul_add,hn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ S.val =
  (((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g))⁻¹ •
    ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) •
      (Unshifted.planeCharges g + Shifted.planeCharges f)hn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ S.val = Unshifted.planeCharges g + Shifted.planeCharges fhn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) ≠ 0 smul_smul,hn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ S.val =
  ((((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g))⁻¹ *
      ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g)) •
    (Unshifted.planeCharges g + Shifted.planeCharges f)hn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ S.val = Unshifted.planeCharges g + Shifted.planeCharges fhn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) ≠ 0 inv_mul_cancel₀,hn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ S.val = 1 • (Unshifted.planeCharges g + Shifted.planeCharges f)hn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) ≠ 0hn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ S.val = Unshifted.planeCharges g + Shifted.planeCharges fhn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) ≠ 0 one_smulhn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ S.val = Unshifted.planeCharges g + Shifted.planeCharges fhn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) ≠ 0hn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ S.val = Unshifted.planeCharges g + Shifted.planeCharges fhn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) ≠ 0]hn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ S.val = Unshifted.planeCharges g + Shifted.planeCharges fhn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) ≠ 0
  ·hn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ S.val = Unshifted.planeCharges g + Shifted.planeCharges f exact hSAll goals completed! 🐙
  ·hn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) ≠ 0 simpa only [Nat.succ_eq_add_one, accCubeTriLinSymm_toFun_apply_apply, ne_eq,
      anomalyFree_param _ _ hS, neg_eq_zero] using h g f hSAll goals completed! 🐙

set_option backward.isDefEq.respectTransparency false in
lemma special_case_lineInCubic {S : (PureU1 (2 * n.succ + 1)).Sols}
    (h : SpecialCase S) :
      LineInCubic S.1.1 := byn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:SpecialCase S⊢ LineInCubic S.toLinSols
  intro g f hS a bn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:SpecialCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Pa g fa:ℚb:ℚ⊢ (accCube (2 * n.succ + 1)) (a • Unshifted.planeCharges g + b • Shifted.planeCharges f) = 0
  erw [TriLinearSymm.toCubic_addn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:SpecialCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Pa g fa:ℚb:ℚ⊢ accCubeTriLinSymm.toCubic (a • Unshifted.planeCharges g) + accCubeTriLinSymm.toCubic (b • Shifted.planeCharges f) +
      3 *
        ((accCubeTriLinSymm (a • Unshifted.planeCharges g)) (a • Unshifted.planeCharges g))
          (b • Shifted.planeCharges f) +
    3 * ((accCubeTriLinSymm (b • Shifted.planeCharges f)) (b • Shifted.planeCharges f)) (a • Unshifted.planeCharges g) =
  0]n:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:SpecialCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Pa g fa:ℚb:ℚ⊢ accCubeTriLinSymm.toCubic (a • Unshifted.planeCharges g) + accCubeTriLinSymm.toCubic (b • Shifted.planeCharges f) +
      3 *
        ((accCubeTriLinSymm (a • Unshifted.planeCharges g)) (a • Unshifted.planeCharges g))
          (b • Shifted.planeCharges f) +
    3 * ((accCubeTriLinSymm (b • Shifted.planeCharges f)) (b • Shifted.planeCharges f)) (a • Unshifted.planeCharges g) =
  0
  rw [HomogeneousCubic.map_smul,n:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:SpecialCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Pa g fa:ℚb:ℚ⊢ a ^ 3 * accCubeTriLinSymm.toCubic (Unshifted.planeCharges g) + accCubeTriLinSymm.toCubic (b • Shifted.planeCharges f) +
      3 *
        ((accCubeTriLinSymm (a • Unshifted.planeCharges g)) (a • Unshifted.planeCharges g))
          (b • Shifted.planeCharges f) +
    3 * ((accCubeTriLinSymm (b • Shifted.planeCharges f)) (b • Shifted.planeCharges f)) (a • Unshifted.planeCharges g) =
  0n:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:SpecialCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Pa g fa:ℚb:ℚ⊢ a ^ 3 * accCubeTriLinSymm.toCubic (Unshifted.planeCharges g) +
        b ^ 3 * accCubeTriLinSymm.toCubic (Shifted.planeCharges f) +
      3 *
        ((accCubeTriLinSymm (a • Unshifted.planeCharges g)) (a • Unshifted.planeCharges g))
          (b • Shifted.planeCharges f) +
    3 * ((accCubeTriLinSymm (b • Shifted.planeCharges f)) (b • Shifted.planeCharges f)) (a • Unshifted.planeCharges g) =
  0 HomogeneousCubic.map_smuln:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:SpecialCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Pa g fa:ℚb:ℚ⊢ a ^ 3 * accCubeTriLinSymm.toCubic (Unshifted.planeCharges g) +
        b ^ 3 * accCubeTriLinSymm.toCubic (Shifted.planeCharges f) +
      3 *
        ((accCubeTriLinSymm (a • Unshifted.planeCharges g)) (a • Unshifted.planeCharges g))
          (b • Shifted.planeCharges f) +
    3 * ((accCubeTriLinSymm (b • Shifted.planeCharges f)) (b • Shifted.planeCharges f)) (a • Unshifted.planeCharges g) =
  0n:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:SpecialCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Pa g fa:ℚb:ℚ⊢ a ^ 3 * accCubeTriLinSymm.toCubic (Unshifted.planeCharges g) +
        b ^ 3 * accCubeTriLinSymm.toCubic (Shifted.planeCharges f) +
      3 *
        ((accCubeTriLinSymm (a • Unshifted.planeCharges g)) (a • Unshifted.planeCharges g))
          (b • Shifted.planeCharges f) +
    3 * ((accCubeTriLinSymm (b • Shifted.planeCharges f)) (b • Shifted.planeCharges f)) (a • Unshifted.planeCharges g) =
  0]n:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:SpecialCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Pa g fa:ℚb:ℚ⊢ a ^ 3 * accCubeTriLinSymm.toCubic (Unshifted.planeCharges g) +
        b ^ 3 * accCubeTriLinSymm.toCubic (Shifted.planeCharges f) +
      3 *
        ((accCubeTriLinSymm (a • Unshifted.planeCharges g)) (a • Unshifted.planeCharges g))
          (b • Shifted.planeCharges f) +
    3 * ((accCubeTriLinSymm (b • Shifted.planeCharges f)) (b • Shifted.planeCharges f)) (a • Unshifted.planeCharges g) =
  0
  erw [Unshifted.planeCharges_accCube,n:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:SpecialCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Pa g fa:ℚb:ℚ⊢ a ^ 3 * 0 + b ^ 3 * accCubeTriLinSymm.toCubic (Shifted.planeCharges f) +
      3 *
        ((accCubeTriLinSymm (a • Unshifted.planeCharges g)) (a • Unshifted.planeCharges g))
          (b • Shifted.planeCharges f) +
    3 * ((accCubeTriLinSymm (b • Shifted.planeCharges f)) (b • Shifted.planeCharges f)) (a • Unshifted.planeCharges g) =
  0 Shifted.planeCharges_accCuben:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:SpecialCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Pa g fa:ℚb:ℚ⊢ a ^ 3 * 0 + b ^ 3 * 0 +
      3 *
        ((accCubeTriLinSymm (a • Unshifted.planeCharges g)) (a • Unshifted.planeCharges g))
          (b • Shifted.planeCharges f) +
    3 * ((accCubeTriLinSymm (b • Shifted.planeCharges f)) (b • Shifted.planeCharges f)) (a • Unshifted.planeCharges g) =
  0]n:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:SpecialCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Pa g fa:ℚb:ℚ⊢ a ^ 3 * 0 + b ^ 3 * 0 +
      3 *
        ((accCubeTriLinSymm (a • Unshifted.planeCharges g)) (a • Unshifted.planeCharges g))
          (b • Shifted.planeCharges f) +
    3 * ((accCubeTriLinSymm (b • Shifted.planeCharges f)) (b • Shifted.planeCharges f)) (a • Unshifted.planeCharges g) =
  0
  have h := h g f hSn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 +
      3 *
        ((accCubeTriLinSymm (a • Unshifted.planeCharges g)) (a • Unshifted.planeCharges g))
          (b • Shifted.planeCharges f) +
    3 * ((accCubeTriLinSymm (b • Shifted.planeCharges f)) (b • Shifted.planeCharges f)) (a • Unshifted.planeCharges g) =
  0
  rw [accCubeTriLinSymm.map_smul₁,n:ℕS:(PureU1 (2 * n.succ + 1)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 +
      3 *
        (a *
          ((accCubeTriLinSymm (Unshifted.planeCharges g)) (a • Unshifted.planeCharges g))
            (b • Shifted.planeCharges f)) +
    3 * ((accCubeTriLinSymm (b • Shifted.planeCharges f)) (b • Shifted.planeCharges f)) (a • Unshifted.planeCharges g) =
  0n:ℕS:(PureU1 (2 * n.succ + 1)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * (a * (b * 0))) +
    3 *
      (b *
        (b *
          (a * ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g)))) =
  0 accCubeTriLinSymm.map_smul₂,n:ℕS:(PureU1 (2 * n.succ + 1)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 +
      3 *
        (a *
          (a *
            ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (b • Shifted.planeCharges f))) +
    3 * ((accCubeTriLinSymm (b • Shifted.planeCharges f)) (b • Shifted.planeCharges f)) (a • Unshifted.planeCharges g) =
  0n:ℕS:(PureU1 (2 * n.succ + 1)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * (a * (b * 0))) +
    3 *
      (b *
        (b *
          (a * ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g)))) =
  0
    accCubeTriLinSymm.map_smul₃,n:ℕS:(PureU1 (2 * n.succ + 1)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 +
      3 *
        (a *
          (a *
            (b *
              ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f)))) +
    3 * ((accCubeTriLinSymm (b • Shifted.planeCharges f)) (b • Shifted.planeCharges f)) (a • Unshifted.planeCharges g) =
  0n:ℕS:(PureU1 (2 * n.succ + 1)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * (a * (b * 0))) +
    3 *
      (b *
        (b *
          (a * ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g)))) =
  0 accCubeTriLinSymm.map_smul₁,n:ℕS:(PureU1 (2 * n.succ + 1)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 +
      3 *
        (a *
          (a *
            (b *
              ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f)))) +
    3 *
      (b * ((accCubeTriLinSymm (Shifted.planeCharges f)) (b • Shifted.planeCharges f)) (a • Unshifted.planeCharges g)) =
  0n:ℕS:(PureU1 (2 * n.succ + 1)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * (a * (b * 0))) +
    3 *
      (b *
        (b *
          (a * ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g)))) =
  0 accCubeTriLinSymm.map_smul₂,n:ℕS:(PureU1 (2 * n.succ + 1)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 +
      3 *
        (a *
          (a *
            (b *
              ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f)))) +
    3 *
      (b *
        (b * ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (a • Unshifted.planeCharges g))) =
  0n:ℕS:(PureU1 (2 * n.succ + 1)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * (a * (b * 0))) +
    3 *
      (b *
        (b *
          (a * ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g)))) =
  0
    accCubeTriLinSymm.map_smul₃,n:ℕS:(PureU1 (2 * n.succ + 1)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 +
      3 *
        (a *
          (a *
            (b *
              ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f)))) +
    3 *
      (b *
        (b *
          (a * ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g)))) =
  0n:ℕS:(PureU1 (2 * n.succ + 1)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * (a * (b * 0))) +
    3 *
      (b *
        (b *
          (a * ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g)))) =
  0 hn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * (a * (b * 0))) +
    3 *
      (b *
        (b *
          (a * ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g)))) =
  0n:ℕS:(PureU1 (2 * n.succ + 1)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * (a * (b * 0))) +
    3 *
      (b *
        (b *
          (a * ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g)))) =
  0]n:ℕS:(PureU1 (2 * n.succ + 1)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.planeCharges f) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * (a * (b * 0))) +
    3 *
      (b *
        (b *
          (a * ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g)))) =
  0
  rw [anomalyFree_param _ _ hSn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Pa g fa:ℚb:ℚh:-((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * (a * (b * 0))) +
    3 *
      (b *
        (b *
          (a * ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g)))) =
  0n:ℕS:(PureU1 (2 * n.succ + 1)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Pa g fa:ℚb:ℚh:-((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * (a * (b * 0))) +
    3 *
      (b *
        (b *
          (a * ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g)))) =
  0] at hn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Pa g fa:ℚb:ℚh:-((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * (a * (b * 0))) +
    3 *
      (b *
        (b *
          (a * ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g)))) =
  0
  simp only [Nat.succ_eq_add_one, accCubeTriLinSymm_toFun_apply_apply, neg_eq_zero] at hn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Pa g fa:ℚb:ℚh:∑ i, Shifted.planeCharges f i * Shifted.planeCharges f i * Unshifted.planeCharges g i = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * (a * (b * 0))) +
    3 *
      (b *
        (b *
          (a * ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g)))) =
  0
  change accCubeTriLinSymm (Shifted.planeCharges f) (Shifted.planeCharges f)
    (Unshifted.planeCharges g) = 0 at hn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * (a * (b * 0))) +
    3 *
      (b *
        (b *
          (a * ((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g)))) =
  0
  erw [hn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * (a * (b * 0))) + 3 * (b * (b * (a * 0))) = 0]n:ℕS:(PureU1 (2 * n.succ + 1)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n.succ → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (Shifted.planeCharges f)) (Shifted.planeCharges f)) (Unshifted.planeCharges g) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * (a * (b * 0))) + 3 * (b * (b * (a * 0))) = 0
  simpAll goals completed! 🐙lemma special_case_lineInCubic_perm {S : (PureU1 (2 * n.succ + 1)).Sols}
    (h : ∀ (M : (FamilyPermutations (2 * n.succ + 1)).group),
    SpecialCase ((FamilyPermutations (2 * n.succ + 1)).solAction.toFun _ _ S M)) :
    LineInCubicPerm S.1.1 := byn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:∀ (M : (FamilyPermutations (2 * n.succ + 1)).group),
  SpecialCase ((MulAction.toFun (FamilyPermutations (2 * n.succ + 1)).group (PureU1 (2 * n.succ + 1)).Sols) S M)⊢ LineInCubicPerm S.toLinSols
  intro Mn:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:∀ (M : (FamilyPermutations (2 * n.succ + 1)).group),
  SpecialCase ((MulAction.toFun (FamilyPermutations (2 * n.succ + 1)).group (PureU1 (2 * n.succ + 1)).Sols) S M)M:(FamilyPermutations (2 * n.succ + 1)).group⊢ LineInCubic (((FamilyPermutations (2 * n.succ + 1)).linSolRep M) S.toLinSols)
  have hM := special_case_lineInCubic (h M)n:ℕS:(PureU1 (2 * n.succ + 1)).Solsh:∀ (M : (FamilyPermutations (2 * n.succ + 1)).group),
  SpecialCase ((MulAction.toFun (FamilyPermutations (2 * n.succ + 1)).group (PureU1 (2 * n.succ + 1)).Sols) S M)M:(FamilyPermutations (2 * n.succ + 1)).grouphM:LineInCubic ((MulAction.toFun (FamilyPermutations (2 * n.succ + 1)).group (PureU1 (2 * n.succ + 1)).Sols) S M).toLinSols⊢ LineInCubic (((FamilyPermutations (2 * n.succ + 1)).linSolRep M) S.toLinSols)
  exact hMAll goals completed! 🐙theorem special_case {S : (PureU1 (2 * n.succ.succ + 1)).Sols}
    (h : ∀ (M : (FamilyPermutations (2 * n.succ.succ + 1)).group),
    SpecialCase ((FamilyPermutations (2 * n.succ.succ + 1)).solAction.toFun _ _ S M)) :
    S.1.1 = 0 := byn:ℕS:(PureU1 (2 * n.succ.succ + 1)).Solsh:∀ (M : (FamilyPermutations (2 * n.succ.succ + 1)).group),
  SpecialCase
    ((MulAction.toFun (FamilyPermutations (2 * n.succ.succ + 1)).group (PureU1 (2 * n.succ.succ + 1)).Sols) S M)⊢ S.toLinSols = 0
  have ht := special_case_lineInCubic_perm hn:ℕS:(PureU1 (2 * n.succ.succ + 1)).Solsh:∀ (M : (FamilyPermutations (2 * n.succ.succ + 1)).group),
  SpecialCase
    ((MulAction.toFun (FamilyPermutations (2 * n.succ.succ + 1)).group (PureU1 (2 * n.succ.succ + 1)).Sols) S M)ht:LineInCubicPerm S.toLinSols⊢ S.toLinSols = 0
  exact lineInCubicPerm_zero htAll goals completed! 🐙