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

Parameterization in even case

Given maps g : Fin n.succ → ℚ, 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, up to permutation, lives in the plane spanned by the first part of the basis vector.

The main reference is:

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

@[expose] public section

Given coefficients g of a point in P and f of a point in P!, and a rational, we get a rational a ∈ ℚ, we get a point in (PureU1 (2 * n.succ)).AnomalyFreeLinear, which we will later show extends to an anomaly free point.

def parameterizationAsLinear (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (a : ℚ) :
    (PureU1 (2 * n.succ)).LinSols :=
  a • ((accCubeTriLinSymm (P! f) (P! f) (P g)) • P' g +
  (- accCubeTriLinSymm (P g) (P g) (P! f)) • P!' f)



lemma parameterizationAsLinear_val (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (a : ℚ) :
    (parameterizationAsLinear g f a).val =
    a • ((accCubeTriLinSymm (P! f) (P! f) (P g)) • P g +
    (- accCubeTriLinSymm (P g) (P g) (P! f)) • P! f) := byn:ℕg:Fin n.succ → ℚf:Fin n → ℚa:ℚ⊢ (parameterizationAsLinear g f a).val =
  a • (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g + -((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f)
  rw [parameterizationAsLinearn:ℕg:Fin n.succ → ℚf:Fin n → ℚa:ℚ⊢ (a • (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P' g + -((accCubeTriLinSymm (P g)) (P g)) (P! f) • P!' f)).val =
  a • (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g + -((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f)n:ℕg:Fin n.succ → ℚf:Fin n → ℚa:ℚ⊢ (a • (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P' g + -((accCubeTriLinSymm (P g)) (P g)) (P! f) • P!' f)).val =
  a • (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g + -((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f)]n:ℕg:Fin n.succ → ℚf:Fin n → ℚa:ℚ⊢ (a • (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P' g + -((accCubeTriLinSymm (P g)) (P g)) (P! f) • P!' f)).val =
  a • (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g + -((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f)
  change a • (_ • (P' g).val + _ • (P!' f).val) = _n:ℕg:Fin n.succ → ℚf:Fin n → ℚa:ℚ⊢ a • (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • (P' g).val + -((accCubeTriLinSymm (P g)) (P g)) (P! f) • (P!' f).val) =
  a • (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g + -((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f)
  rw [P'_val,n:ℕg:Fin n.succ → ℚf:Fin n → ℚa:ℚ⊢ a • (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g + -((accCubeTriLinSymm (P g)) (P g)) (P! f) • (P!' f).val) =
  a • (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g + -((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f)All goals completed! 🐙 P!'_valn:ℕg:Fin n.succ → ℚf:Fin n → ℚa:ℚ⊢ a • (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g + -((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f) =
  a • (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g + -((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f)All goals completed! 🐙]All goals completed! 🐙



set_option backward.isDefEq.respectTransparency false in
lemma parameterizationCharge_cube (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (a : ℚ) :
    accCube (2* n.succ) (parameterizationAsLinear g f a).val = 0 := byn:ℕg:Fin n.succ → ℚf:Fin n → ℚa:ℚ⊢ (accCube (2 * n.succ)) (parameterizationAsLinear g f a).val = 0
  change accCubeTriLinSymm.toCubic _ = 0n:ℕg:Fin n.succ → ℚf:Fin n → ℚa:ℚ⊢ accCubeTriLinSymm.toCubic (parameterizationAsLinear g f a).val = 0
  rw [parameterizationAsLinear_val,n:ℕg:Fin n.succ → ℚf:Fin n → ℚa:ℚ⊢ accCubeTriLinSymm.toCubic
    (a • (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g + -((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f)) =
  0n:ℕg:Fin n.succ → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (P! f)) (P! f)) (P g) ^ 3 * accCubeTriLinSymm.toCubic (P g) +
          (-((accCubeTriLinSymm (P g)) (P g)) (P! f)) ^ 3 * accCubeTriLinSymm.toCubic (P! f) +
        3 *
          ((accCubeTriLinSymm (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g))
              (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g))
            (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f) +
      3 *
        ((accCubeTriLinSymm (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f))
            (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f))
          (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g)) =
  0 HomogeneousCubic.map_smul,n:ℕg:Fin n.succ → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    accCubeTriLinSymm.toCubic
      (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g + -((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f) =
  0n:ℕg:Fin n.succ → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (P! f)) (P! f)) (P g) ^ 3 * accCubeTriLinSymm.toCubic (P g) +
          (-((accCubeTriLinSymm (P g)) (P g)) (P! f)) ^ 3 * accCubeTriLinSymm.toCubic (P! f) +
        3 *
          ((accCubeTriLinSymm (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g))
              (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g))
            (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f) +
      3 *
        ((accCubeTriLinSymm (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f))
            (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f))
          (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g)) =
  0
    TriLinearSymm.toCubic_add,n:ℕg:Fin n.succ → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (accCubeTriLinSymm.toCubic (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g) +
          accCubeTriLinSymm.toCubic (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f) +
        3 *
          ((accCubeTriLinSymm (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g))
              (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g))
            (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f) +
      3 *
        ((accCubeTriLinSymm (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f))
            (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f))
          (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g)) =
  0n:ℕg:Fin n.succ → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (P! f)) (P! f)) (P g) ^ 3 * accCubeTriLinSymm.toCubic (P g) +
          (-((accCubeTriLinSymm (P g)) (P g)) (P! f)) ^ 3 * accCubeTriLinSymm.toCubic (P! f) +
        3 *
          ((accCubeTriLinSymm (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g))
              (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g))
            (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f) +
      3 *
        ((accCubeTriLinSymm (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f))
            (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f))
          (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g)) =
  0 HomogeneousCubic.map_smul,n:ℕg:Fin n.succ → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (P! f)) (P! f)) (P g) ^ 3 * accCubeTriLinSymm.toCubic (P g) +
          accCubeTriLinSymm.toCubic (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f) +
        3 *
          ((accCubeTriLinSymm (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g))
              (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g))
            (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f) +
      3 *
        ((accCubeTriLinSymm (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f))
            (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f))
          (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g)) =
  0n:ℕg:Fin n.succ → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (P! f)) (P! f)) (P g) ^ 3 * accCubeTriLinSymm.toCubic (P g) +
          (-((accCubeTriLinSymm (P g)) (P g)) (P! f)) ^ 3 * accCubeTriLinSymm.toCubic (P! f) +
        3 *
          ((accCubeTriLinSymm (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g))
              (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g))
            (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f) +
      3 *
        ((accCubeTriLinSymm (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f))
            (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f))
          (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g)) =
  0 HomogeneousCubic.map_smuln:ℕg:Fin n.succ → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (P! f)) (P! f)) (P g) ^ 3 * accCubeTriLinSymm.toCubic (P g) +
          (-((accCubeTriLinSymm (P g)) (P g)) (P! f)) ^ 3 * accCubeTriLinSymm.toCubic (P! f) +
        3 *
          ((accCubeTriLinSymm (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g))
              (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g))
            (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f) +
      3 *
        ((accCubeTriLinSymm (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f))
            (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f))
          (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g)) =
  0n:ℕg:Fin n.succ → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (P! f)) (P! f)) (P g) ^ 3 * accCubeTriLinSymm.toCubic (P g) +
          (-((accCubeTriLinSymm (P g)) (P g)) (P! f)) ^ 3 * accCubeTriLinSymm.toCubic (P! f) +
        3 *
          ((accCubeTriLinSymm (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g))
              (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g))
            (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f) +
      3 *
        ((accCubeTriLinSymm (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f))
            (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f))
          (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g)) =
  0]n:ℕg:Fin n.succ → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (P! f)) (P! f)) (P g) ^ 3 * accCubeTriLinSymm.toCubic (P g) +
          (-((accCubeTriLinSymm (P g)) (P g)) (P! f)) ^ 3 * accCubeTriLinSymm.toCubic (P! f) +
        3 *
          ((accCubeTriLinSymm (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g))
              (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g))
            (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f) +
      3 *
        ((accCubeTriLinSymm (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f))
            (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f))
          (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g)) =
  0
  erw [P_accCube,n:ℕg:Fin n.succ → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (P! f)) (P! f)) (P g) ^ 3 * 0 +
          (-((accCubeTriLinSymm (P g)) (P g)) (P! f)) ^ 3 * accCubeTriLinSymm.toCubic (P! f) +
        3 *
          ((accCubeTriLinSymm (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g))
              (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g))
            (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f) +
      3 *
        ((accCubeTriLinSymm (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f))
            (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f))
          (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g)) =
  0 P!_accCuben:ℕg:Fin n.succ → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (P! f)) (P! f)) (P g) ^ 3 * 0 + (-((accCubeTriLinSymm (P g)) (P g)) (P! f)) ^ 3 * 0 +
        3 *
          ((accCubeTriLinSymm (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g))
              (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g))
            (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f) +
      3 *
        ((accCubeTriLinSymm (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f))
            (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f))
          (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g)) =
  0]n:ℕg:Fin n.succ → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (P! f)) (P! f)) (P g) ^ 3 * 0 + (-((accCubeTriLinSymm (P g)) (P g)) (P! f)) ^ 3 * 0 +
        3 *
          ((accCubeTriLinSymm (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g))
              (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g))
            (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f) +
      3 *
        ((accCubeTriLinSymm (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f))
            (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f))
          (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g)) =
  0
  rw [accCubeTriLinSymm.map_smul₁,n:ℕg:Fin n.succ → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (P! f)) (P! f)) (P g) ^ 3 * 0 + (-((accCubeTriLinSymm (P g)) (P g)) (P! f)) ^ 3 * 0 +
        3 *
          (((accCubeTriLinSymm (P! f)) (P! f)) (P g) *
            ((accCubeTriLinSymm (P g)) (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g))
              (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f)) +
      3 *
        ((accCubeTriLinSymm (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f))
            (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f))
          (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g)) =
  0n:ℕg:Fin n.succ → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (P! f)) (P! f)) (P g) ^ 3 * 0 + (-((accCubeTriLinSymm (P g)) (P g)) (P! f)) ^ 3 * 0 +
        3 *
          (((accCubeTriLinSymm (P! f)) (P! f)) (P g) *
            (((accCubeTriLinSymm (P! f)) (P! f)) (P g) *
              (-((accCubeTriLinSymm (P g)) (P g)) (P! f) * ((accCubeTriLinSymm (P g)) (P g)) (P! f)))) +
      3 *
        (-((accCubeTriLinSymm (P g)) (P g)) (P! f) *
          (-((accCubeTriLinSymm (P g)) (P g)) (P! f) *
            (((accCubeTriLinSymm (P! f)) (P! f)) (P g) * ((accCubeTriLinSymm (P! f)) (P! f)) (P g))))) =
  0 accCubeTriLinSymm.map_smul₂,n:ℕg:Fin n.succ → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (P! f)) (P! f)) (P g) ^ 3 * 0 + (-((accCubeTriLinSymm (P g)) (P g)) (P! f)) ^ 3 * 0 +
        3 *
          (((accCubeTriLinSymm (P! f)) (P! f)) (P g) *
            (((accCubeTriLinSymm (P! f)) (P! f)) (P g) *
              ((accCubeTriLinSymm (P g)) (P g)) (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f))) +
      3 *
        ((accCubeTriLinSymm (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f))
            (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f))
          (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g)) =
  0n:ℕg:Fin n.succ → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (P! f)) (P! f)) (P g) ^ 3 * 0 + (-((accCubeTriLinSymm (P g)) (P g)) (P! f)) ^ 3 * 0 +
        3 *
          (((accCubeTriLinSymm (P! f)) (P! f)) (P g) *
            (((accCubeTriLinSymm (P! f)) (P! f)) (P g) *
              (-((accCubeTriLinSymm (P g)) (P g)) (P! f) * ((accCubeTriLinSymm (P g)) (P g)) (P! f)))) +
      3 *
        (-((accCubeTriLinSymm (P g)) (P g)) (P! f) *
          (-((accCubeTriLinSymm (P g)) (P g)) (P! f) *
            (((accCubeTriLinSymm (P! f)) (P! f)) (P g) * ((accCubeTriLinSymm (P! f)) (P! f)) (P g))))) =
  0
    accCubeTriLinSymm.map_smul₃,n:ℕg:Fin n.succ → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (P! f)) (P! f)) (P g) ^ 3 * 0 + (-((accCubeTriLinSymm (P g)) (P g)) (P! f)) ^ 3 * 0 +
        3 *
          (((accCubeTriLinSymm (P! f)) (P! f)) (P g) *
            (((accCubeTriLinSymm (P! f)) (P! f)) (P g) *
              (-((accCubeTriLinSymm (P g)) (P g)) (P! f) * ((accCubeTriLinSymm (P g)) (P g)) (P! f)))) +
      3 *
        ((accCubeTriLinSymm (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f))
            (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f))
          (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g)) =
  0n:ℕg:Fin n.succ → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (P! f)) (P! f)) (P g) ^ 3 * 0 + (-((accCubeTriLinSymm (P g)) (P g)) (P! f)) ^ 3 * 0 +
        3 *
          (((accCubeTriLinSymm (P! f)) (P! f)) (P g) *
            (((accCubeTriLinSymm (P! f)) (P! f)) (P g) *
              (-((accCubeTriLinSymm (P g)) (P g)) (P! f) * ((accCubeTriLinSymm (P g)) (P g)) (P! f)))) +
      3 *
        (-((accCubeTriLinSymm (P g)) (P g)) (P! f) *
          (-((accCubeTriLinSymm (P g)) (P g)) (P! f) *
            (((accCubeTriLinSymm (P! f)) (P! f)) (P g) * ((accCubeTriLinSymm (P! f)) (P! f)) (P g))))) =
  0 accCubeTriLinSymm.map_smul₁,n:ℕg:Fin n.succ → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (P! f)) (P! f)) (P g) ^ 3 * 0 + (-((accCubeTriLinSymm (P g)) (P g)) (P! f)) ^ 3 * 0 +
        3 *
          (((accCubeTriLinSymm (P! f)) (P! f)) (P g) *
            (((accCubeTriLinSymm (P! f)) (P! f)) (P g) *
              (-((accCubeTriLinSymm (P g)) (P g)) (P! f) * ((accCubeTriLinSymm (P g)) (P g)) (P! f)))) +
      3 *
        (-((accCubeTriLinSymm (P g)) (P g)) (P! f) *
          ((accCubeTriLinSymm (P! f)) (-((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f))
            (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g))) =
  0n:ℕg:Fin n.succ → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (P! f)) (P! f)) (P g) ^ 3 * 0 + (-((accCubeTriLinSymm (P g)) (P g)) (P! f)) ^ 3 * 0 +
        3 *
          (((accCubeTriLinSymm (P! f)) (P! f)) (P g) *
            (((accCubeTriLinSymm (P! f)) (P! f)) (P g) *
              (-((accCubeTriLinSymm (P g)) (P g)) (P! f) * ((accCubeTriLinSymm (P g)) (P g)) (P! f)))) +
      3 *
        (-((accCubeTriLinSymm (P g)) (P g)) (P! f) *
          (-((accCubeTriLinSymm (P g)) (P g)) (P! f) *
            (((accCubeTriLinSymm (P! f)) (P! f)) (P g) * ((accCubeTriLinSymm (P! f)) (P! f)) (P g))))) =
  0 accCubeTriLinSymm.map_smul₂,n:ℕg:Fin n.succ → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (P! f)) (P! f)) (P g) ^ 3 * 0 + (-((accCubeTriLinSymm (P g)) (P g)) (P! f)) ^ 3 * 0 +
        3 *
          (((accCubeTriLinSymm (P! f)) (P! f)) (P g) *
            (((accCubeTriLinSymm (P! f)) (P! f)) (P g) *
              (-((accCubeTriLinSymm (P g)) (P g)) (P! f) * ((accCubeTriLinSymm (P g)) (P g)) (P! f)))) +
      3 *
        (-((accCubeTriLinSymm (P g)) (P g)) (P! f) *
          (-((accCubeTriLinSymm (P g)) (P g)) (P! f) *
            ((accCubeTriLinSymm (P! f)) (P! f)) (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g)))) =
  0n:ℕg:Fin n.succ → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (P! f)) (P! f)) (P g) ^ 3 * 0 + (-((accCubeTriLinSymm (P g)) (P g)) (P! f)) ^ 3 * 0 +
        3 *
          (((accCubeTriLinSymm (P! f)) (P! f)) (P g) *
            (((accCubeTriLinSymm (P! f)) (P! f)) (P g) *
              (-((accCubeTriLinSymm (P g)) (P g)) (P! f) * ((accCubeTriLinSymm (P g)) (P g)) (P! f)))) +
      3 *
        (-((accCubeTriLinSymm (P g)) (P g)) (P! f) *
          (-((accCubeTriLinSymm (P g)) (P g)) (P! f) *
            (((accCubeTriLinSymm (P! f)) (P! f)) (P g) * ((accCubeTriLinSymm (P! f)) (P! f)) (P g))))) =
  0
    accCubeTriLinSymm.map_smul₃n:ℕg:Fin n.succ → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (P! f)) (P! f)) (P g) ^ 3 * 0 + (-((accCubeTriLinSymm (P g)) (P g)) (P! f)) ^ 3 * 0 +
        3 *
          (((accCubeTriLinSymm (P! f)) (P! f)) (P g) *
            (((accCubeTriLinSymm (P! f)) (P! f)) (P g) *
              (-((accCubeTriLinSymm (P g)) (P g)) (P! f) * ((accCubeTriLinSymm (P g)) (P g)) (P! f)))) +
      3 *
        (-((accCubeTriLinSymm (P g)) (P g)) (P! f) *
          (-((accCubeTriLinSymm (P g)) (P g)) (P! f) *
            (((accCubeTriLinSymm (P! f)) (P! f)) (P g) * ((accCubeTriLinSymm (P! f)) (P! f)) (P g))))) =
  0n:ℕg:Fin n.succ → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (P! f)) (P! f)) (P g) ^ 3 * 0 + (-((accCubeTriLinSymm (P g)) (P g)) (P! f)) ^ 3 * 0 +
        3 *
          (((accCubeTriLinSymm (P! f)) (P! f)) (P g) *
            (((accCubeTriLinSymm (P! f)) (P! f)) (P g) *
              (-((accCubeTriLinSymm (P g)) (P g)) (P! f) * ((accCubeTriLinSymm (P g)) (P g)) (P! f)))) +
      3 *
        (-((accCubeTriLinSymm (P g)) (P g)) (P! f) *
          (-((accCubeTriLinSymm (P g)) (P g)) (P! f) *
            (((accCubeTriLinSymm (P! f)) (P! f)) (P g) * ((accCubeTriLinSymm (P! f)) (P! f)) (P g))))) =
  0]n:ℕg:Fin n.succ → ℚf:Fin n → ℚa:ℚ⊢ a ^ 3 *
    (((accCubeTriLinSymm (P! f)) (P! f)) (P g) ^ 3 * 0 + (-((accCubeTriLinSymm (P g)) (P g)) (P! f)) ^ 3 * 0 +
        3 *
          (((accCubeTriLinSymm (P! f)) (P! f)) (P g) *
            (((accCubeTriLinSymm (P! f)) (P! f)) (P g) *
              (-((accCubeTriLinSymm (P g)) (P g)) (P! f) * ((accCubeTriLinSymm (P g)) (P g)) (P! f)))) +
      3 *
        (-((accCubeTriLinSymm (P g)) (P g)) (P! f) *
          (-((accCubeTriLinSymm (P g)) (P g)) (P! f) *
            (((accCubeTriLinSymm (P! f)) (P! f)) (P g) * ((accCubeTriLinSymm (P! f)) (P! f)) (P g))))) =
  0
  ringAll goals completed! 🐙

The construction of a Sol from a Fin n.succ → ℚ, a Fin n → ℚ and a ℚ.

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



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

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

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



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

A proposition on a solution which is true if accCubeTriLinSymm (P g, P g, P! f) = 0.

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

              

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

lemma generic_or_special (S : (PureU1 (2 * n.succ)).Sols) :
    GenericCase S ∨ SpecialCase S := byn:ℕS:(PureU1 (2 * n.succ)).Sols⊢ GenericCase S ∨ SpecialCase S
  obtain ⟨g, f, h⟩ := span_basis S.1.1n:ℕS:(PureU1 (2 * n.succ)).Solsg:Fin n.succ → ℚf:Fin n → ℚh:S.val = P g + P! f⊢ GenericCase S ∨ SpecialCase S
  have h1 : accCubeTriLinSymm (P g) (P g) (P! f) ≠ 0 ∨
    accCubeTriLinSymm (P g) (P g) (P! f) = 0 := by
    exact ne_or_eq _ _n:ℕS:(PureU1 (2 * n.succ)).Solsg:Fin n.succ → ℚf:Fin n → ℚh:S.val = P g + P! fh1:((accCubeTriLinSymm (P g)) (P g)) (P! f) ≠ 0 ∨ ((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0⊢ GenericCase S ∨ SpecialCase Sn:ℕS:(PureU1 (2 * n.succ)).Solsg:Fin n.succ → ℚf:Fin n → ℚh:S.val = P g + P! fh1:((accCubeTriLinSymm (P g)) (P g)) (P! f) ≠ 0 ∨ ((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0⊢ GenericCase S ∨ SpecialCase S
  rcases h1 with h1 | h1inln:ℕS:(PureU1 (2 * n.succ)).Solsg:Fin n.succ → ℚf:Fin n → ℚh:S.val = P g + P! fh1:((accCubeTriLinSymm (P g)) (P g)) (P! f) ≠ 0⊢ GenericCase S ∨ SpecialCase Sinrn:ℕS:(PureU1 (2 * n.succ)).Solsg:Fin n.succ → ℚf:Fin n → ℚh:S.val = P g + P! fh1:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0⊢ GenericCase S ∨ SpecialCase S
  ·inln:ℕS:(PureU1 (2 * n.succ)).Solsg:Fin n.succ → ℚf:Fin n → ℚh:S.val = P g + P! fh1:((accCubeTriLinSymm (P g)) (P g)) (P! 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)).Solsg:Fin n.succ → ℚf:Fin n → ℚh:S.val = P g + P! fh1:((accCubeTriLinSymm (P g)) (P g)) (P! 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)).Sols} (h : GenericCase S) :
    ∃ g f a, S = parameterization g f a := byn:ℕS:(PureU1 (2 * n.succ)).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)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! f⊢ ∃ g f a, S = parameterization g f a
  use g, f, (accCubeTriLinSymm (P! f) (P! f) (P g))⁻¹hn:ℕS:(PureU1 (2 * n.succ)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! f⊢ S = parameterization g f (((accCubeTriLinSymm (P! f)) (P! f)) (P g))⁻¹
  rw [parameterizationhn:ℕS:(PureU1 (2 * n.succ)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! f⊢ S =
  { toLinSols := parameterizationAsLinear g f (((accCubeTriLinSymm (P! f)) (P! f)) (P g))⁻¹, quadSol := ⋯,
    cubicSol := ⋯ }hn:ℕS:(PureU1 (2 * n.succ)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! f⊢ S =
  { toLinSols := parameterizationAsLinear g f (((accCubeTriLinSymm (P! f)) (P! f)) (P g))⁻¹, quadSol := ⋯,
    cubicSol := ⋯ }]hn:ℕS:(PureU1 (2 * n.succ)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! f⊢ S =
  { toLinSols := parameterizationAsLinear g f (((accCubeTriLinSymm (P! f)) (P! f)) (P g))⁻¹, quadSol := ⋯,
    cubicSol := ⋯ }
  apply ACCSystem.Sols.exthn:ℕS:(PureU1 (2 * n.succ)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! f⊢ S.val =
  { toLinSols := parameterizationAsLinear g f (((accCubeTriLinSymm (P! f)) (P! f)) (P g))⁻¹, quadSol := ⋯,
      cubicSol := ⋯ }.val
  rw [parameterizationAsLinear_valhn:ℕS:(PureU1 (2 * n.succ)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! f⊢ S.val =
  (((accCubeTriLinSymm (P! f)) (P! f)) (P g))⁻¹ •
    (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g + -((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f)hn:ℕS:(PureU1 (2 * n.succ)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! f⊢ S.val =
  (((accCubeTriLinSymm (P! f)) (P! f)) (P g))⁻¹ •
    (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g + -((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f)]hn:ℕS:(PureU1 (2 * n.succ)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! f⊢ S.val =
  (((accCubeTriLinSymm (P! f)) (P! f)) (P g))⁻¹ •
    (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g + -((accCubeTriLinSymm (P g)) (P g)) (P! f) • P! f)
  rw [anomalyFree_param _ _ hShn:ℕS:(PureU1 (2 * n.succ)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! f⊢ S.val =
  (((accCubeTriLinSymm (P! f)) (P! f)) (P g))⁻¹ •
    (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g + - -((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P! f)hn:ℕS:(PureU1 (2 * n.succ)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! f⊢ S.val =
  (((accCubeTriLinSymm (P! f)) (P! f)) (P g))⁻¹ •
    (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g + - -((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P! f)]hn:ℕS:(PureU1 (2 * n.succ)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! f⊢ S.val =
  (((accCubeTriLinSymm (P! f)) (P! f)) (P g))⁻¹ •
    (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g + - -((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P! f)
  rw [neg_neg,hn:ℕS:(PureU1 (2 * n.succ)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! f⊢ S.val =
  (((accCubeTriLinSymm (P! f)) (P! f)) (P g))⁻¹ •
    (((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P g + ((accCubeTriLinSymm (P! f)) (P! f)) (P g) • P! f)hn:ℕS:(PureU1 (2 * n.succ)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! f⊢ S.val = P g + P! fhn:ℕS:(PureU1 (2 * n.succ)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! f⊢ ((accCubeTriLinSymm (P! f)) (P! f)) (P g) ≠ 0 ← smul_add,hn:ℕS:(PureU1 (2 * n.succ)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! f⊢ S.val = (((accCubeTriLinSymm (P! f)) (P! f)) (P g))⁻¹ • ((accCubeTriLinSymm (P! f)) (P! f)) (P g) • (P g + P! f)hn:ℕS:(PureU1 (2 * n.succ)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! f⊢ S.val = P g + P! fhn:ℕS:(PureU1 (2 * n.succ)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! f⊢ ((accCubeTriLinSymm (P! f)) (P! f)) (P g) ≠ 0 smul_smul,hn:ℕS:(PureU1 (2 * n.succ)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! f⊢ S.val = ((((accCubeTriLinSymm (P! f)) (P! f)) (P g))⁻¹ * ((accCubeTriLinSymm (P! f)) (P! f)) (P g)) • (P g + P! f)hn:ℕS:(PureU1 (2 * n.succ)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! f⊢ S.val = P g + P! fhn:ℕS:(PureU1 (2 * n.succ)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! f⊢ ((accCubeTriLinSymm (P! f)) (P! f)) (P g) ≠ 0 inv_mul_cancel₀,hn:ℕS:(PureU1 (2 * n.succ)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! f⊢ S.val = 1 • (P g + P! f)hn:ℕS:(PureU1 (2 * n.succ)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! f⊢ ((accCubeTriLinSymm (P! f)) (P! f)) (P g) ≠ 0hn:ℕS:(PureU1 (2 * n.succ)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! f⊢ S.val = P g + P! fhn:ℕS:(PureU1 (2 * n.succ)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! f⊢ ((accCubeTriLinSymm (P! f)) (P! f)) (P g) ≠ 0 one_smulhn:ℕS:(PureU1 (2 * n.succ)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! f⊢ S.val = P g + P! fhn:ℕS:(PureU1 (2 * n.succ)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! f⊢ ((accCubeTriLinSymm (P! f)) (P! f)) (P g) ≠ 0hn:ℕS:(PureU1 (2 * n.succ)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! f⊢ S.val = P g + P! fhn:ℕS:(PureU1 (2 * n.succ)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! f⊢ ((accCubeTriLinSymm (P! f)) (P! f)) (P g) ≠ 0]hn:ℕS:(PureU1 (2 * n.succ)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! f⊢ S.val = P g + P! fhn:ℕS:(PureU1 (2 * n.succ)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! f⊢ ((accCubeTriLinSymm (P! f)) (P! f)) (P g) ≠ 0
  ·hn:ℕS:(PureU1 (2 * n.succ)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! f⊢ S.val = P g + P! f exact hSAll goals completed! 🐙
  ·hn:ℕS:(PureU1 (2 * n.succ)).Solsh:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! f⊢ ((accCubeTriLinSymm (P! f)) (P! f)) (P g) ≠ 0 have h := h g f hShn:ℕS:(PureU1 (2 * n.succ)).Solsh✝:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! fh:((accCubeTriLinSymm (P g)) (P g)) (P! f) ≠ 0⊢ ((accCubeTriLinSymm (P! f)) (P! f)) (P g) ≠ 0
    rw [anomalyFree_param _ _ hShn:ℕS:(PureU1 (2 * n.succ)).Solsh✝:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! fh:-((accCubeTriLinSymm (P! f)) (P! f)) (P g) ≠ 0⊢ ((accCubeTriLinSymm (P! f)) (P! f)) (P g) ≠ 0hn:ℕS:(PureU1 (2 * n.succ)).Solsh✝:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! fh:-((accCubeTriLinSymm (P! f)) (P! f)) (P g) ≠ 0⊢ ((accCubeTriLinSymm (P! f)) (P! f)) (P g) ≠ 0] at hhn:ℕS:(PureU1 (2 * n.succ)).Solsh✝:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! fh:-((accCubeTriLinSymm (P! f)) (P! f)) (P g) ≠ 0⊢ ((accCubeTriLinSymm (P! f)) (P! f)) (P g) ≠ 0
    simp only [Nat.succ_eq_add_one, accCubeTriLinSymm_toFun_apply_apply, ne_eq, neg_eq_zero] at hhn:ℕS:(PureU1 (2 * n.succ)).Solsh✝:GenericCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! fh:¬∑ i, P! f i * P! f i * P g i = 0⊢ ((accCubeTriLinSymm (P! f)) (P! f)) (P g) ≠ 0
    exact hAll goals completed! 🐙

set_option backward.isDefEq.respectTransparency false in
lemma special_case_lineInCubic {S : (PureU1 (2 * n.succ)).Sols}
    (h : SpecialCase S) : LineInCubic S.1.1 := byn:ℕS:(PureU1 (2 * n.succ)).Solsh:SpecialCase S⊢ LineInCubic S.toLinSols
  intro g f hS a bn:ℕS:(PureU1 (2 * n.succ)).Solsh:SpecialCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚ⊢ (accCube (2 * n.succ)) (a • P g + b • P! f) = 0
  erw [TriLinearSymm.toCubic_addn:ℕS:(PureU1 (2 * n.succ)).Solsh:SpecialCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚ⊢ accCubeTriLinSymm.toCubic (a • P g) + accCubeTriLinSymm.toCubic (b • P! f) +
      3 * ((accCubeTriLinSymm (a • P g)) (a • P g)) (b • P! f) +
    3 * ((accCubeTriLinSymm (b • P! f)) (b • P! f)) (a • P g) =
  0]n:ℕS:(PureU1 (2 * n.succ)).Solsh:SpecialCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚ⊢ accCubeTriLinSymm.toCubic (a • P g) + accCubeTriLinSymm.toCubic (b • P! f) +
      3 * ((accCubeTriLinSymm (a • P g)) (a • P g)) (b • P! f) +
    3 * ((accCubeTriLinSymm (b • P! f)) (b • P! f)) (a • P g) =
  0
  rw [HomogeneousCubic.map_smul,n:ℕS:(PureU1 (2 * n.succ)).Solsh:SpecialCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚ⊢ a ^ 3 * accCubeTriLinSymm.toCubic (P g) + accCubeTriLinSymm.toCubic (b • P! f) +
      3 * ((accCubeTriLinSymm (a • P g)) (a • P g)) (b • P! f) +
    3 * ((accCubeTriLinSymm (b • P! f)) (b • P! f)) (a • P g) =
  0n:ℕS:(PureU1 (2 * n.succ)).Solsh:SpecialCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚ⊢ a ^ 3 * accCubeTriLinSymm.toCubic (P g) + b ^ 3 * accCubeTriLinSymm.toCubic (P! f) +
      3 * ((accCubeTriLinSymm (a • P g)) (a • P g)) (b • P! f) +
    3 * ((accCubeTriLinSymm (b • P! f)) (b • P! f)) (a • P g) =
  0 HomogeneousCubic.map_smuln:ℕS:(PureU1 (2 * n.succ)).Solsh:SpecialCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚ⊢ a ^ 3 * accCubeTriLinSymm.toCubic (P g) + b ^ 3 * accCubeTriLinSymm.toCubic (P! f) +
      3 * ((accCubeTriLinSymm (a • P g)) (a • P g)) (b • P! f) +
    3 * ((accCubeTriLinSymm (b • P! f)) (b • P! f)) (a • P g) =
  0n:ℕS:(PureU1 (2 * n.succ)).Solsh:SpecialCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚ⊢ a ^ 3 * accCubeTriLinSymm.toCubic (P g) + b ^ 3 * accCubeTriLinSymm.toCubic (P! f) +
      3 * ((accCubeTriLinSymm (a • P g)) (a • P g)) (b • P! f) +
    3 * ((accCubeTriLinSymm (b • P! f)) (b • P! f)) (a • P g) =
  0]n:ℕS:(PureU1 (2 * n.succ)).Solsh:SpecialCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚ⊢ a ^ 3 * accCubeTriLinSymm.toCubic (P g) + b ^ 3 * accCubeTriLinSymm.toCubic (P! f) +
      3 * ((accCubeTriLinSymm (a • P g)) (a • P g)) (b • P! f) +
    3 * ((accCubeTriLinSymm (b • P! f)) (b • P! f)) (a • P g) =
  0
  erw [P_accCube,n:ℕS:(PureU1 (2 * n.succ)).Solsh:SpecialCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚ⊢ a ^ 3 * 0 + b ^ 3 * accCubeTriLinSymm.toCubic (P! f) + 3 * ((accCubeTriLinSymm (a • P g)) (a • P g)) (b • P! f) +
    3 * ((accCubeTriLinSymm (b • P! f)) (b • P! f)) (a • P g) =
  0 P!_accCuben:ℕS:(PureU1 (2 * n.succ)).Solsh:SpecialCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚ⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * ((accCubeTriLinSymm (a • P g)) (a • P g)) (b • P! f) +
    3 * ((accCubeTriLinSymm (b • P! f)) (b • P! f)) (a • P g) =
  0]n:ℕS:(PureU1 (2 * n.succ)).Solsh:SpecialCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚ⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * ((accCubeTriLinSymm (a • P g)) (a • P g)) (b • P! f) +
    3 * ((accCubeTriLinSymm (b • P! f)) (b • P! f)) (a • P g) =
  0
  have h := h g f hSn:ℕS:(PureU1 (2 * n.succ)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * ((accCubeTriLinSymm (a • P g)) (a • P g)) (b • P! f) +
    3 * ((accCubeTriLinSymm (b • P! f)) (b • P! f)) (a • P g) =
  0
  rw [accCubeTriLinSymm.map_smul₁,n:ℕS:(PureU1 (2 * n.succ)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * ((accCubeTriLinSymm (P g)) (a • P g)) (b • P! f)) +
    3 * ((accCubeTriLinSymm (b • P! f)) (b • P! f)) (a • P g) =
  0n:ℕS:(PureU1 (2 * n.succ)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * (a * (b * 0))) + 3 * (b * (b * (a * ((accCubeTriLinSymm (P! f)) (P! f)) (P g)))) = 0 accCubeTriLinSymm.map_smul₂,n:ℕS:(PureU1 (2 * n.succ)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * (a * ((accCubeTriLinSymm (P g)) (P g)) (b • P! f))) +
    3 * ((accCubeTriLinSymm (b • P! f)) (b • P! f)) (a • P g) =
  0n:ℕS:(PureU1 (2 * n.succ)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * (a * (b * 0))) + 3 * (b * (b * (a * ((accCubeTriLinSymm (P! f)) (P! f)) (P g)))) = 0
    accCubeTriLinSymm.map_smul₃,n:ℕS:(PureU1 (2 * n.succ)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * (a * (b * ((accCubeTriLinSymm (P g)) (P g)) (P! f)))) +
    3 * ((accCubeTriLinSymm (b • P! f)) (b • P! f)) (a • P g) =
  0n:ℕS:(PureU1 (2 * n.succ)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * (a * (b * 0))) + 3 * (b * (b * (a * ((accCubeTriLinSymm (P! f)) (P! f)) (P g)))) = 0 accCubeTriLinSymm.map_smul₁,n:ℕS:(PureU1 (2 * n.succ)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * (a * (b * ((accCubeTriLinSymm (P g)) (P g)) (P! f)))) +
    3 * (b * ((accCubeTriLinSymm (P! f)) (b • P! f)) (a • P g)) =
  0n:ℕS:(PureU1 (2 * n.succ)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * (a * (b * 0))) + 3 * (b * (b * (a * ((accCubeTriLinSymm (P! f)) (P! f)) (P g)))) = 0 accCubeTriLinSymm.map_smul₂,n:ℕS:(PureU1 (2 * n.succ)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * (a * (b * ((accCubeTriLinSymm (P g)) (P g)) (P! f)))) +
    3 * (b * (b * ((accCubeTriLinSymm (P! f)) (P! f)) (a • P g))) =
  0n:ℕS:(PureU1 (2 * n.succ)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * (a * (b * 0))) + 3 * (b * (b * (a * ((accCubeTriLinSymm (P! f)) (P! f)) (P g)))) = 0
    accCubeTriLinSymm.map_smul₃,n:ℕS:(PureU1 (2 * n.succ)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * (a * (b * ((accCubeTriLinSymm (P g)) (P g)) (P! f)))) +
    3 * (b * (b * (a * ((accCubeTriLinSymm (P! f)) (P! f)) (P g)))) =
  0n:ℕS:(PureU1 (2 * n.succ)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * (a * (b * 0))) + 3 * (b * (b * (a * ((accCubeTriLinSymm (P! f)) (P! f)) (P g)))) = 0 hn:ℕS:(PureU1 (2 * n.succ)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * (a * (b * 0))) + 3 * (b * (b * (a * ((accCubeTriLinSymm (P! f)) (P! f)) (P g)))) = 0n:ℕS:(PureU1 (2 * n.succ)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * (a * (b * 0))) + 3 * (b * (b * (a * ((accCubeTriLinSymm (P! f)) (P! f)) (P g)))) = 0]n:ℕS:(PureU1 (2 * n.succ)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * (a * (b * 0))) + 3 * (b * (b * (a * ((accCubeTriLinSymm (P! f)) (P! f)) (P g)))) = 0
  rw [anomalyFree_param _ _ hSn:ℕS:(PureU1 (2 * n.succ)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚh:-((accCubeTriLinSymm (P! f)) (P! f)) (P g) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * (a * (b * 0))) + 3 * (b * (b * (a * ((accCubeTriLinSymm (P! f)) (P! f)) (P g)))) = 0n:ℕS:(PureU1 (2 * n.succ)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚh:-((accCubeTriLinSymm (P! f)) (P! f)) (P g) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * (a * (b * 0))) + 3 * (b * (b * (a * ((accCubeTriLinSymm (P! f)) (P! f)) (P g)))) = 0] at hn:ℕS:(PureU1 (2 * n.succ)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚh:-((accCubeTriLinSymm (P! f)) (P! f)) (P g) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * (a * (b * 0))) + 3 * (b * (b * (a * ((accCubeTriLinSymm (P! f)) (P! f)) (P g)))) = 0
  simp only [Nat.succ_eq_add_one, accCubeTriLinSymm_toFun_apply_apply, neg_eq_zero] at hn:ℕS:(PureU1 (2 * n.succ)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚh:∑ i, P! f i * P! f i * P g i = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * (a * (b * 0))) + 3 * (b * (b * (a * ((accCubeTriLinSymm (P! f)) (P! f)) (P g)))) = 0
  change accCubeTriLinSymm (P! f) (P! f) (P g) = 0 at hn:ℕS:(PureU1 (2 * n.succ)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (P! f)) (P! f)) (P g) = 0⊢ a ^ 3 * 0 + b ^ 3 * 0 + 3 * (a * (a * (b * 0))) + 3 * (b * (b * (a * ((accCubeTriLinSymm (P! f)) (P! f)) (P g)))) = 0
  erw [hn:ℕS:(PureU1 (2 * n.succ)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (P! f)) (P! f)) (P 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)).Solsh✝:SpecialCase Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚh:((accCubeTriLinSymm (P! f)) (P! f)) (P 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)).Sols}
    (h : ∀ (M : (FamilyPermutations (2 * n.succ)).group),
    SpecialCase ((FamilyPermutations (2 * n.succ)).solAction.toFun _ _ S M)) :
    LineInCubicPerm S.1.1 :=
  fun M => special_case_lineInCubic (h M)theorem special_case {S : (PureU1 (2 * n.succ.succ)).Sols}
    (h : ∀ (M : (FamilyPermutations (2 * n.succ.succ)).group),
    SpecialCase ((FamilyPermutations (2 * n.succ.succ)).solAction.toFun _ _ S M)) :
    ∃ (M : (FamilyPermutations (2 * n.succ.succ)).group),
    ((FamilyPermutations (2 * n.succ.succ)).solAction.toFun _ _ S M).1.1
    ∈ Submodule.span ℚ (Set.range basis) :=
  lineInCubicPerm_in_plane S (special_case_lineInCubic_perm h)