Physlib.QFT.QED.AnomalyCancellation.Even.LineInCubic

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.BasisLinear
public import Physlib.QFT.QED.AnomalyCancellation.LineInPlaneCond

Line In Cubic Even case

We say that a linear solution satisfies the lineInCubic property if the line through that point and through the two different planes formed by the basis of LinSols lies in the cubic.

We show that for a solution all its permutations satisfy this property, then there exists a permutation for which it lies in the plane spanned by the first part of the basis.

The main reference for this file is:

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

@[expose] public section

A property on LinSols, satisfied if every point on the line between the two planes in the basis through that point is in the cubic.

def LineInCubic (S : (PureU1 (2 * n.succ)).LinSols) : Prop :=
  ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = Pa g f) (a b : ℚ),
  accCube (2 * n.succ) (a • P g + b • P! f) = 0

set_option backward.isDefEq.respectTransparency false in
lemma lineInCubic_expand {S : (PureU1 (2 * n.succ)).LinSols} (h : LineInCubic S) :
    ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = Pa g f) (a b : ℚ),
    3 * a * b * (a * accCubeTriLinSymm (P g) (P g) (P! f)
    + b * accCubeTriLinSymm (P! f) (P! f) (P g)) = 0 := byn:ℕS:(PureU1 (2 * n.succ)).LinSolsh:LineInCubic S⊢ ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ),
  S.val = Pa g f →
    ∀ (a b : ℚ),
      3 * a * b * (a * ((accCubeTriLinSymm (P g)) (P g)) (P! f) + b * ((accCubeTriLinSymm (P! f)) (P! f)) (P g)) = 0
  intro g f hS a bn:ℕS:(PureU1 (2 * n.succ)).LinSolsh:LineInCubic Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚ⊢ 3 * a * b * (a * ((accCubeTriLinSymm (P g)) (P g)) (P! f) + b * ((accCubeTriLinSymm (P! f)) (P! f)) (P g)) = 0
  have h1 := h g f hS a bn:ℕS:(PureU1 (2 * n.succ)).LinSolsh:LineInCubic Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚh1:(accCube (2 * n.succ)) (a • P g + b • P! f) = 0⊢ 3 * a * b * (a * ((accCubeTriLinSymm (P g)) (P g)) (P! f) + b * ((accCubeTriLinSymm (P! f)) (P! f)) (P g)) = 0
  change accCubeTriLinSymm.toCubic (a • P g + b • P! f) = 0 at h1n:ℕS:(PureU1 (2 * n.succ)).LinSolsh:LineInCubic Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚh1:accCubeTriLinSymm.toCubic (a • P g + b • P! f) = 0⊢ 3 * a * b * (a * ((accCubeTriLinSymm (P g)) (P g)) (P! f) + b * ((accCubeTriLinSymm (P! f)) (P! f)) (P g)) = 0
  simp only [TriLinearSymm.toCubic_add, HomogeneousCubic.map_smul,
    accCubeTriLinSymm.map_smul₁, accCubeTriLinSymm.map_smul₂, accCubeTriLinSymm.map_smul₃] at h1n:ℕS:(PureU1 (2 * n.succ)).LinSolsh:LineInCubic Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚh1:a ^ 3 * accCubeTriLinSymm.toCubic (P g) + b ^ 3 * accCubeTriLinSymm.toCubic (P! f) +
      3 * (a * (a * (b * ((accCubeTriLinSymm (P g)) (P g)) (P! f)))) +
    3 * (b * (b * (a * ((accCubeTriLinSymm (P! f)) (P! f)) (P g)))) =
  0⊢ 3 * a * b * (a * ((accCubeTriLinSymm (P g)) (P g)) (P! f) + b * ((accCubeTriLinSymm (P! f)) (P! f)) (P g)) = 0
  erw [P_accCube,n:ℕS:(PureU1 (2 * n.succ)).LinSolsh:LineInCubic Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚh1:a ^ 3 * 0 + b ^ 3 * accCubeTriLinSymm.toCubic (P! f) + 3 * (a * (a * (b * ((accCubeTriLinSymm (P g)) (P g)) (P! f)))) +
    3 * (b * (b * (a * ((accCubeTriLinSymm (P! f)) (P! f)) (P g)))) =
  0⊢ 3 * a * b * (a * ((accCubeTriLinSymm (P g)) (P g)) (P! f) + b * ((accCubeTriLinSymm (P! f)) (P! f)) (P g)) = 0 P!_accCuben:ℕS:(PureU1 (2 * n.succ)).LinSolsh:LineInCubic Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚh1: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)))) =
  0⊢ 3 * a * b * (a * ((accCubeTriLinSymm (P g)) (P g)) (P! f) + b * ((accCubeTriLinSymm (P! f)) (P! f)) (P g)) = 0]n:ℕS:(PureU1 (2 * n.succ)).LinSolsh:LineInCubic Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = Pa g fa:ℚb:ℚh1: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)))) =
  0⊢ 3 * a * b * (a * ((accCubeTriLinSymm (P g)) (P g)) (P! f) + b * ((accCubeTriLinSymm (P! f)) (P! f)) (P g)) = 0 at h1
  linear_combination h1All goals completed! 🐙

This lemma states that for a given S of type (PureU1 (2 * n.succ)).AnomalyFreeLinear and a proof h that the line through S lies on a cubic curve, for any functions g : Fin n.succ → ℚ and f : Fin n → ℚ, if S.val = P g + P! f, then accCubeTriLinSymm.toFun (P g, P g, P! f) = 0.

lemma line_in_cubic_P_P_P! {S : (PureU1 (2 * n.succ)).LinSols} (h : LineInCubic S) :
    ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = P g + P! f),
    accCubeTriLinSymm (P g) (P g) (P! f) = 0 := byn:ℕS:(PureU1 (2 * n.succ)).LinSolsh:LineInCubic S⊢ ∀ (g : Fin n.succ → ℚ) (f : Fin n → ℚ), S.val = P g + P! f → ((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0
  intro g f hSn:ℕS:(PureU1 (2 * n.succ)).LinSolsh:LineInCubic Sg:Fin n.succ → ℚf:Fin n → ℚhS:S.val = P g + P! f⊢ ((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0
  linear_combination 2 / 3 * (lineInCubic_expand h g f hS 1 1) -
    (lineInCubic_expand h g f hS 1 2) / 6All goals completed! 🐙

A LinSol satisfies LineInCubicPerm if all its permutations satisfy lineInCubic.

def LineInCubicPerm (S : (PureU1 (2 * n.succ)).LinSols) : Prop :=
  ∀ (M : (FamilyPermutations (2 * n.succ)).group),
  LineInCubic ((FamilyPermutations (2 * n.succ)).linSolRep M S)

If lineInCubicPerm S then lineInCubic S.

lemma lineInCubicPerm_self {S : (PureU1 (2 * n.succ)).LinSols}
    (hS : LineInCubicPerm S) : LineInCubic S := hS 1

If lineInCubicPerm S then lineInCubicPerm (M S) for all permutations M.

lemma lineInCubicPerm_permute {S : (PureU1 (2 * n.succ)).LinSols}
    (hS : LineInCubicPerm S) (M' : (FamilyPermutations (2 * n.succ)).group) :
    LineInCubicPerm ((FamilyPermutations (2 * n.succ)).linSolRep M' S) := byn:ℕS:(PureU1 (2 * n.succ)).LinSolshS:LineInCubicPerm SM':(FamilyPermutations (2 * n.succ)).group⊢ LineInCubicPerm (((FamilyPermutations (2 * n.succ)).linSolRep M') S)
  intro Mn:ℕS:(PureU1 (2 * n.succ)).LinSolshS:LineInCubicPerm SM':(FamilyPermutations (2 * n.succ)).groupM:(FamilyPermutations (2 * n.succ)).group⊢ LineInCubic (((FamilyPermutations (2 * n.succ)).linSolRep M) (((FamilyPermutations (2 * n.succ)).linSolRep M') S))
  have h := hS (M * M')n:ℕS:(PureU1 (2 * n.succ)).LinSolshS:LineInCubicPerm SM':(FamilyPermutations (2 * n.succ)).groupM:(FamilyPermutations (2 * n.succ)).grouph:LineInCubic (((FamilyPermutations (2 * n.succ)).linSolRep (M * M')) S)⊢ LineInCubic (((FamilyPermutations (2 * n.succ)).linSolRep M) (((FamilyPermutations (2 * n.succ)).linSolRep M') S))
  erw [(FamilyPermutations (2 * n.succ)).linSolRep.map_mul M M'n:ℕS:(PureU1 (2 * n.succ)).LinSolshS:LineInCubicPerm SM':(FamilyPermutations (2 * n.succ)).groupM:(FamilyPermutations (2 * n.succ)).grouph:LineInCubic (((FamilyPermutations (2 * n.succ)).linSolRep M * (FamilyPermutations (2 * n.succ)).linSolRep M') S)⊢ LineInCubic (((FamilyPermutations (2 * n.succ)).linSolRep M) (((FamilyPermutations (2 * n.succ)).linSolRep M') S))]n:ℕS:(PureU1 (2 * n.succ)).LinSolshS:LineInCubicPerm SM':(FamilyPermutations (2 * n.succ)).groupM:(FamilyPermutations (2 * n.succ)).grouph:LineInCubic (((FamilyPermutations (2 * n.succ)).linSolRep M * (FamilyPermutations (2 * n.succ)).linSolRep M') S)⊢ LineInCubic (((FamilyPermutations (2 * n.succ)).linSolRep M) (((FamilyPermutations (2 * n.succ)).linSolRep M') S)) at h
  exact hAll goals completed! 🐙

              

set_option backward.isDefEq.respectTransparency false in
lemma lineInCubicPerm_swap {S : (PureU1 (2 * n.succ)).LinSols}
    (LIC : LineInCubicPerm S) :
    ∀ (j : Fin n) (g : Fin n.succ → ℚ) (f : Fin n → ℚ) (_ : S.val = Pa g f),
      (S.val (evenShiftSnd j) - S.val (evenShiftFst j))
      * accCubeTriLinSymm (P g) (P g) (basis!AsCharges j) = 0 := byn:ℕS:(PureU1 (2 * n.succ)).LinSolsLIC:LineInCubicPerm S⊢ ∀ (j : Fin n) (g : Fin n.succ → ℚ) (f : Fin n → ℚ),
  S.val = Pa g f →
    (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0
  intro j g f hn:ℕS:(PureU1 (2 * n.succ)).LinSolsLIC:LineInCubicPerm Sj:Fin ng:Fin n.succ → ℚf:Fin n → ℚh:S.val = Pa g f⊢ (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0
  obtain ⟨g', f', hall⟩ := span_basis_swap! j rfl g f hn:ℕS:(PureU1 (2 * n.succ)).LinSolsLIC:LineInCubicPerm Sj:Fin ng:Fin n.succ → ℚf:Fin n → ℚh:S.val = Pa g fg':Fin n.succ → ℚf':Fin n → ℚhall:(((FamilyPermutations (2 * n.succ)).linSolRep (Equiv.swap (evenShiftFst j) (evenShiftSnd j))) S).val = P g' + P! f' ∧
  P! f' = P! f + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • basis!AsCharges j ∧ g' = g⊢ (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0
  have h1 := line_in_cubic_P_P_P! (lineInCubicPerm_self LIC) g f hn:ℕS:(PureU1 (2 * n.succ)).LinSolsLIC:LineInCubicPerm Sj:Fin ng:Fin n.succ → ℚf:Fin n → ℚh:S.val = Pa g fg':Fin n.succ → ℚf':Fin n → ℚhall:(((FamilyPermutations (2 * n.succ)).linSolRep (Equiv.swap (evenShiftFst j) (evenShiftSnd j))) S).val = P g' + P! f' ∧
  P! f' = P! f + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • basis!AsCharges j ∧ g' = gh1:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0⊢ (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0
  have h2 := line_in_cubic_P_P_P!
    (lineInCubicPerm_self (lineInCubicPerm_permute LIC
    (Equiv.swap (evenShiftFst j) (evenShiftSnd j)))) g' f' hall.1n:ℕS:(PureU1 (2 * n.succ)).LinSolsLIC:LineInCubicPerm Sj:Fin ng:Fin n.succ → ℚf:Fin n → ℚh:S.val = Pa g fg':Fin n.succ → ℚf':Fin n → ℚhall:(((FamilyPermutations (2 * n.succ)).linSolRep (Equiv.swap (evenShiftFst j) (evenShiftSnd j))) S).val = P g' + P! f' ∧
  P! f' = P! f + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • basis!AsCharges j ∧ g' = gh1:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0h2:((accCubeTriLinSymm (P g')) (P g')) (P! f') = 0⊢ (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0
  rw [hall.2.1,n:ℕS:(PureU1 (2 * n.succ)).LinSolsLIC:LineInCubicPerm Sj:Fin ng:Fin n.succ → ℚf:Fin n → ℚh:S.val = Pa g fg':Fin n.succ → ℚf':Fin n → ℚhall:(((FamilyPermutations (2 * n.succ)).linSolRep (Equiv.swap (evenShiftFst j) (evenShiftSnd j))) S).val = P g' + P! f' ∧
  P! f' = P! f + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • basis!AsCharges j ∧ g' = gh1:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0h2:((accCubeTriLinSymm (P g')) (P g')) (P! f + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • basis!AsCharges j) = 0⊢ (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0n:ℕS:(PureU1 (2 * n.succ)).LinSolsLIC:LineInCubicPerm Sj:Fin ng:Fin n.succ → ℚf:Fin n → ℚh:S.val = Pa g fg':Fin n.succ → ℚf':Fin n → ℚhall:(((FamilyPermutations (2 * n.succ)).linSolRep (Equiv.swap (evenShiftFst j) (evenShiftSnd j))) S).val = P g' + P! f' ∧
  P! f' = P! f + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • basis!AsCharges j ∧ g' = gh1:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0h2:0 + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0⊢ (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0 hall.2.2,n:ℕS:(PureU1 (2 * n.succ)).LinSolsLIC:LineInCubicPerm Sj:Fin ng:Fin n.succ → ℚf:Fin n → ℚh:S.val = Pa g fg':Fin n.succ → ℚf':Fin n → ℚhall:(((FamilyPermutations (2 * n.succ)).linSolRep (Equiv.swap (evenShiftFst j) (evenShiftSnd j))) S).val = P g' + P! f' ∧
  P! f' = P! f + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • basis!AsCharges j ∧ g' = gh1:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0h2:((accCubeTriLinSymm (P g)) (P g)) (P! f + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • basis!AsCharges j) = 0⊢ (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0n:ℕS:(PureU1 (2 * n.succ)).LinSolsLIC:LineInCubicPerm Sj:Fin ng:Fin n.succ → ℚf:Fin n → ℚh:S.val = Pa g fg':Fin n.succ → ℚf':Fin n → ℚhall:(((FamilyPermutations (2 * n.succ)).linSolRep (Equiv.swap (evenShiftFst j) (evenShiftSnd j))) S).val = P g' + P! f' ∧
  P! f' = P! f + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • basis!AsCharges j ∧ g' = gh1:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0h2:0 + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0⊢ (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0 accCubeTriLinSymm.map_add₃,n:ℕS:(PureU1 (2 * n.succ)).LinSolsLIC:LineInCubicPerm Sj:Fin ng:Fin n.succ → ℚf:Fin n → ℚh:S.val = Pa g fg':Fin n.succ → ℚf':Fin n → ℚhall:(((FamilyPermutations (2 * n.succ)).linSolRep (Equiv.swap (evenShiftFst j) (evenShiftSnd j))) S).val = P g' + P! f' ∧
  P! f' = P! f + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • basis!AsCharges j ∧ g' = gh1:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0h2:((accCubeTriLinSymm (P g)) (P g)) (P! f) +
    ((accCubeTriLinSymm (P g)) (P g)) ((S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • basis!AsCharges j) =
  0⊢ (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0n:ℕS:(PureU1 (2 * n.succ)).LinSolsLIC:LineInCubicPerm Sj:Fin ng:Fin n.succ → ℚf:Fin n → ℚh:S.val = Pa g fg':Fin n.succ → ℚf':Fin n → ℚhall:(((FamilyPermutations (2 * n.succ)).linSolRep (Equiv.swap (evenShiftFst j) (evenShiftSnd j))) S).val = P g' + P! f' ∧
  P! f' = P! f + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • basis!AsCharges j ∧ g' = gh1:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0h2:0 + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0⊢ (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0 h1,n:ℕS:(PureU1 (2 * n.succ)).LinSolsLIC:LineInCubicPerm Sj:Fin ng:Fin n.succ → ℚf:Fin n → ℚh:S.val = Pa g fg':Fin n.succ → ℚf':Fin n → ℚhall:(((FamilyPermutations (2 * n.succ)).linSolRep (Equiv.swap (evenShiftFst j) (evenShiftSnd j))) S).val = P g' + P! f' ∧
  P! f' = P! f + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • basis!AsCharges j ∧ g' = gh1:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0h2:0 + ((accCubeTriLinSymm (P g)) (P g)) ((S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • basis!AsCharges j) = 0⊢ (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0n:ℕS:(PureU1 (2 * n.succ)).LinSolsLIC:LineInCubicPerm Sj:Fin ng:Fin n.succ → ℚf:Fin n → ℚh:S.val = Pa g fg':Fin n.succ → ℚf':Fin n → ℚhall:(((FamilyPermutations (2 * n.succ)).linSolRep (Equiv.swap (evenShiftFst j) (evenShiftSnd j))) S).val = P g' + P! f' ∧
  P! f' = P! f + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • basis!AsCharges j ∧ g' = gh1:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0h2:0 + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0⊢ (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0 accCubeTriLinSymm.map_smul₃n:ℕS:(PureU1 (2 * n.succ)).LinSolsLIC:LineInCubicPerm Sj:Fin ng:Fin n.succ → ℚf:Fin n → ℚh:S.val = Pa g fg':Fin n.succ → ℚf':Fin n → ℚhall:(((FamilyPermutations (2 * n.succ)).linSolRep (Equiv.swap (evenShiftFst j) (evenShiftSnd j))) S).val = P g' + P! f' ∧
  P! f' = P! f + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • basis!AsCharges j ∧ g' = gh1:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0h2:0 + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0⊢ (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0n:ℕS:(PureU1 (2 * n.succ)).LinSolsLIC:LineInCubicPerm Sj:Fin ng:Fin n.succ → ℚf:Fin n → ℚh:S.val = Pa g fg':Fin n.succ → ℚf':Fin n → ℚhall:(((FamilyPermutations (2 * n.succ)).linSolRep (Equiv.swap (evenShiftFst j) (evenShiftSnd j))) S).val = P g' + P! f' ∧
  P! f' = P! f + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • basis!AsCharges j ∧ g' = gh1:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0h2:0 + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0⊢ (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0] at h2n:ℕS:(PureU1 (2 * n.succ)).LinSolsLIC:LineInCubicPerm Sj:Fin ng:Fin n.succ → ℚf:Fin n → ℚh:S.val = Pa g fg':Fin n.succ → ℚf':Fin n → ℚhall:(((FamilyPermutations (2 * n.succ)).linSolRep (Equiv.swap (evenShiftFst j) (evenShiftSnd j))) S).val = P g' + P! f' ∧
  P! f' = P! f + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) • basis!AsCharges j ∧ g' = gh1:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0h2:0 + (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0⊢ (S.val (evenShiftSnd j) - S.val (evenShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0
  simpa using h2All goals completed! 🐙

lemma P_P_P!_accCube' {S : (PureU1 (2 * n.succ.succ)).LinSols}
    (f : Fin n.succ.succ → ℚ) (g : Fin n.succ → ℚ) (hS : S.val = Pa f g) :
    accCubeTriLinSymm (P f) (P f) (basis!AsCharges (Fin.last n)) =
    - (S.val (evenShiftSnd (Fin.last n)) + S.val (evenShiftFst (Fin.last n))) *
    (2 * S.val evenShiftLast +
    S.val (evenShiftSnd (Fin.last n)) + S.val (evenShiftFst (Fin.last n))) := byn:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ → ℚhS:S.val = Pa f g⊢ ((accCubeTriLinSymm (P f)) (P f)) (basis!AsCharges (Fin.last n)) =
  -(S.val (evenShiftSnd (Fin.last n)) + S.val (evenShiftFst (Fin.last n))) *
    (2 * S.val evenShiftLast + S.val (evenShiftSnd (Fin.last n)) + S.val (evenShiftFst (Fin.last n)))
  rw [P_P_P!_accCube f (Fin.last n),n:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ → ℚhS:S.val = Pa f g⊢ f (Fin.last n).succ ^ 2 - f (Fin.last n).castSucc ^ 2 =
  -(S.val (evenShiftSnd (Fin.last n)) + S.val (evenShiftFst (Fin.last n))) *
    (2 * S.val evenShiftLast + S.val (evenShiftSnd (Fin.last n)) + S.val (evenShiftFst (Fin.last n)))n:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ → ℚhS:S.val = Pa f g⊢ f (Fin.last n.succ) ^ 2 - f (Fin.last n).castSucc ^ 2 =
  -(-f (Fin.last n).castSucc - g (Fin.last n) + (f (Fin.last n.succ) + g (Fin.last n))) *
    (2 * -f (Fin.last (n + 1)) + (-f (Fin.last n).castSucc - g (Fin.last n)) + (f (Fin.last n.succ) + g (Fin.last n))) hS,n:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ → ℚhS:S.val = Pa f g⊢ f (Fin.last n).succ ^ 2 - f (Fin.last n).castSucc ^ 2 =
  -(Pa f g (evenShiftSnd (Fin.last n)) + Pa f g (evenShiftFst (Fin.last n))) *
    (2 * Pa f g evenShiftLast + Pa f g (evenShiftSnd (Fin.last n)) + Pa f g (evenShiftFst (Fin.last n)))n:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ → ℚhS:S.val = Pa f g⊢ f (Fin.last n.succ) ^ 2 - f (Fin.last n).castSucc ^ 2 =
  -(-f (Fin.last n).castSucc - g (Fin.last n) + (f (Fin.last n.succ) + g (Fin.last n))) *
    (2 * -f (Fin.last (n + 1)) + (-f (Fin.last n).castSucc - g (Fin.last n)) + (f (Fin.last n.succ) + g (Fin.last n))) Pa_evenShiftSnd,n:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ → ℚhS:S.val = Pa f g⊢ f (Fin.last n).succ ^ 2 - f (Fin.last n).castSucc ^ 2 =
  -(-f (Fin.last n).castSucc - g (Fin.last n) + Pa f g (evenShiftFst (Fin.last n))) *
    (2 * Pa f g evenShiftLast + (-f (Fin.last n).castSucc - g (Fin.last n)) + Pa f g (evenShiftFst (Fin.last n)))n:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ → ℚhS:S.val = Pa f g⊢ f (Fin.last n.succ) ^ 2 - f (Fin.last n).castSucc ^ 2 =
  -(-f (Fin.last n).castSucc - g (Fin.last n) + (f (Fin.last n.succ) + g (Fin.last n))) *
    (2 * -f (Fin.last (n + 1)) + (-f (Fin.last n).castSucc - g (Fin.last n)) + (f (Fin.last n.succ) + g (Fin.last n))) Pa_evenShiftFst,n:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ → ℚhS:S.val = Pa f g⊢ f (Fin.last n).succ ^ 2 - f (Fin.last n).castSucc ^ 2 =
  -(-f (Fin.last n).castSucc - g (Fin.last n) + (f (Fin.last n).succ + g (Fin.last n))) *
    (2 * Pa f g evenShiftLast + (-f (Fin.last n).castSucc - g (Fin.last n)) + (f (Fin.last n).succ + g (Fin.last n)))n:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ → ℚhS:S.val = Pa f g⊢ f (Fin.last n.succ) ^ 2 - f (Fin.last n).castSucc ^ 2 =
  -(-f (Fin.last n).castSucc - g (Fin.last n) + (f (Fin.last n.succ) + g (Fin.last n))) *
    (2 * -f (Fin.last (n + 1)) + (-f (Fin.last n).castSucc - g (Fin.last n)) + (f (Fin.last n.succ) + g (Fin.last n))) Pa_evenShiftLast,n:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ → ℚhS:S.val = Pa f g⊢ f (Fin.last n).succ ^ 2 - f (Fin.last n).castSucc ^ 2 =
  -(-f (Fin.last n).castSucc - g (Fin.last n) + (f (Fin.last n).succ + g (Fin.last n))) *
    (2 * -f (Fin.last (n + 1)) + (-f (Fin.last n).castSucc - g (Fin.last n)) + (f (Fin.last n).succ + g (Fin.last n)))n:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ → ℚhS:S.val = Pa f g⊢ f (Fin.last n.succ) ^ 2 - f (Fin.last n).castSucc ^ 2 =
  -(-f (Fin.last n).castSucc - g (Fin.last n) + (f (Fin.last n.succ) + g (Fin.last n))) *
    (2 * -f (Fin.last (n + 1)) + (-f (Fin.last n).castSucc - g (Fin.last n)) + (f (Fin.last n.succ) + g (Fin.last n)))
    Fin.succ_lastn:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ → ℚhS:S.val = Pa f g⊢ f (Fin.last n.succ) ^ 2 - f (Fin.last n).castSucc ^ 2 =
  -(-f (Fin.last n).castSucc - g (Fin.last n) + (f (Fin.last n.succ) + g (Fin.last n))) *
    (2 * -f (Fin.last (n + 1)) + (-f (Fin.last n).castSucc - g (Fin.last n)) + (f (Fin.last n.succ) + g (Fin.last n)))n:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ → ℚhS:S.val = Pa f g⊢ f (Fin.last n.succ) ^ 2 - f (Fin.last n).castSucc ^ 2 =
  -(-f (Fin.last n).castSucc - g (Fin.last n) + (f (Fin.last n.succ) + g (Fin.last n))) *
    (2 * -f (Fin.last (n + 1)) + (-f (Fin.last n).castSucc - g (Fin.last n)) + (f (Fin.last n.succ) + g (Fin.last n)))]n:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ → ℚhS:S.val = Pa f g⊢ f (Fin.last n.succ) ^ 2 - f (Fin.last n).castSucc ^ 2 =
  -(-f (Fin.last n).castSucc - g (Fin.last n) + (f (Fin.last n.succ) + g (Fin.last n))) *
    (2 * -f (Fin.last (n + 1)) + (-f (Fin.last n).castSucc - g (Fin.last n)) + (f (Fin.last n.succ) + g (Fin.last n)))
  ringAll goals completed! 🐙

lemma lineInCubicPerm_last_cond {S : (PureU1 (2 * n.succ.succ)).LinSols}
    (LIC : LineInCubicPerm S) :
    LineInPlaneProp
    ((S.val (evenShiftSnd (Fin.last n))), ((S.val (evenShiftFst (Fin.last n))),
      (S.val evenShiftLast))) := byn:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsLIC:LineInCubicPerm S⊢ LineInPlaneProp (S.val (evenShiftSnd (Fin.last n)), S.val (evenShiftFst (Fin.last n)), S.val evenShiftLast)
  obtain ⟨g, f, hfg⟩ := span_basis Sn:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsLIC:LineInCubicPerm Sg:Fin (n + 1).succ → ℚf:Fin (n + 1) → ℚhfg:S.val = P g + P! f⊢ LineInPlaneProp (S.val (evenShiftSnd (Fin.last n)), S.val (evenShiftFst (Fin.last n)), S.val evenShiftLast)
  have h1 := lineInCubicPerm_swap LIC (Fin.last n) g f hfgn:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsLIC:LineInCubicPerm Sg:Fin (n + 1).succ → ℚf:Fin (n + 1) → ℚhfg:S.val = P g + P! fh1:(S.val (evenShiftSnd (Fin.last n)) - S.val (evenShiftFst (Fin.last n))) *
    ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges (Fin.last n)) =
  0⊢ LineInPlaneProp (S.val (evenShiftSnd (Fin.last n)), S.val (evenShiftFst (Fin.last n)), S.val evenShiftLast)
  rw [P_P_P!_accCube' g f hfgn:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsLIC:LineInCubicPerm Sg:Fin (n + 1).succ → ℚf:Fin (n + 1) → ℚhfg:S.val = P g + P! fh1:(S.val (evenShiftSnd (Fin.last n)) - S.val (evenShiftFst (Fin.last n))) *
    (-(S.val (evenShiftSnd (Fin.last n)) + S.val (evenShiftFst (Fin.last n))) *
      (2 * S.val evenShiftLast + S.val (evenShiftSnd (Fin.last n)) + S.val (evenShiftFst (Fin.last n)))) =
  0⊢ LineInPlaneProp (S.val (evenShiftSnd (Fin.last n)), S.val (evenShiftFst (Fin.last n)), S.val evenShiftLast)n:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsLIC:LineInCubicPerm Sg:Fin (n + 1).succ → ℚf:Fin (n + 1) → ℚhfg:S.val = P g + P! fh1:(S.val (evenShiftSnd (Fin.last n)) - S.val (evenShiftFst (Fin.last n))) *
    (-(S.val (evenShiftSnd (Fin.last n)) + S.val (evenShiftFst (Fin.last n))) *
      (2 * S.val evenShiftLast + S.val (evenShiftSnd (Fin.last n)) + S.val (evenShiftFst (Fin.last n)))) =
  0⊢ LineInPlaneProp (S.val (evenShiftSnd (Fin.last n)), S.val (evenShiftFst (Fin.last n)), S.val evenShiftLast)] at h1n:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsLIC:LineInCubicPerm Sg:Fin (n + 1).succ → ℚf:Fin (n + 1) → ℚhfg:S.val = P g + P! fh1:(S.val (evenShiftSnd (Fin.last n)) - S.val (evenShiftFst (Fin.last n))) *
    (-(S.val (evenShiftSnd (Fin.last n)) + S.val (evenShiftFst (Fin.last n))) *
      (2 * S.val evenShiftLast + S.val (evenShiftSnd (Fin.last n)) + S.val (evenShiftFst (Fin.last n)))) =
  0⊢ LineInPlaneProp (S.val (evenShiftSnd (Fin.last n)), S.val (evenShiftFst (Fin.last n)), S.val evenShiftLast)
  simp only [Nat.succ_eq_add_one, neg_add_rev, mul_eq_zero] at h1n:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsLIC:LineInCubicPerm Sg:Fin (n + 1).succ → ℚf:Fin (n + 1) → ℚhfg:S.val = P g + P! fh1:S.val (evenShiftSnd (Fin.last n)) - S.val (evenShiftFst (Fin.last n)) = 0 ∨
  -S.val (evenShiftFst (Fin.last n)) + -S.val (evenShiftSnd (Fin.last n)) = 0 ∨
    2 * S.val evenShiftLast + S.val (evenShiftSnd (Fin.last n)) + S.val (evenShiftFst (Fin.last n)) = 0⊢ LineInPlaneProp (S.val (evenShiftSnd (Fin.last n)), S.val (evenShiftFst (Fin.last n)), S.val evenShiftLast)
  rcases h1 with h1 | h1 | h1inln:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsLIC:LineInCubicPerm Sg:Fin (n + 1).succ → ℚf:Fin (n + 1) → ℚhfg:S.val = P g + P! fh1:S.val (evenShiftSnd (Fin.last n)) - S.val (evenShiftFst (Fin.last n)) = 0⊢ LineInPlaneProp (S.val (evenShiftSnd (Fin.last n)), S.val (evenShiftFst (Fin.last n)), S.val evenShiftLast)inr.inln:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsLIC:LineInCubicPerm Sg:Fin (n + 1).succ → ℚf:Fin (n + 1) → ℚhfg:S.val = P g + P! fh1:-S.val (evenShiftFst (Fin.last n)) + -S.val (evenShiftSnd (Fin.last n)) = 0⊢ LineInPlaneProp (S.val (evenShiftSnd (Fin.last n)), S.val (evenShiftFst (Fin.last n)), S.val evenShiftLast)inr.inrn:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsLIC:LineInCubicPerm Sg:Fin (n + 1).succ → ℚf:Fin (n + 1) → ℚhfg:S.val = P g + P! fh1:2 * S.val evenShiftLast + S.val (evenShiftSnd (Fin.last n)) + S.val (evenShiftFst (Fin.last n)) = 0⊢ LineInPlaneProp (S.val (evenShiftSnd (Fin.last n)), S.val (evenShiftFst (Fin.last n)), S.val evenShiftLast)
  ·inln:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsLIC:LineInCubicPerm Sg:Fin (n + 1).succ → ℚf:Fin (n + 1) → ℚhfg:S.val = P g + P! fh1:S.val (evenShiftSnd (Fin.last n)) - S.val (evenShiftFst (Fin.last n)) = 0⊢ LineInPlaneProp (S.val (evenShiftSnd (Fin.last n)), S.val (evenShiftFst (Fin.last n)), S.val evenShiftLast) exact Or.inl (byn:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsLIC:LineInCubicPerm Sg:Fin (n + 1).succ → ℚf:Fin (n + 1) → ℚhfg:S.val = P g + P! fh1:S.val (evenShiftSnd (Fin.last n)) - S.val (evenShiftFst (Fin.last n)) = 0⊢ (S.val (evenShiftSnd (Fin.last n)), S.val (evenShiftFst (Fin.last n)), S.val evenShiftLast).1 =
  (S.val (evenShiftSnd (Fin.last n)), S.val (evenShiftFst (Fin.last n)), S.val evenShiftLast).2.1 linear_combination h1All goals completed! 🐙)
  ·inr.inln:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsLIC:LineInCubicPerm Sg:Fin (n + 1).succ → ℚf:Fin (n + 1) → ℚhfg:S.val = P g + P! fh1:-S.val (evenShiftFst (Fin.last n)) + -S.val (evenShiftSnd (Fin.last n)) = 0⊢ LineInPlaneProp (S.val (evenShiftSnd (Fin.last n)), S.val (evenShiftFst (Fin.last n)), S.val evenShiftLast) exact Or.inr (Or.inl (byn:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsLIC:LineInCubicPerm Sg:Fin (n + 1).succ → ℚf:Fin (n + 1) → ℚhfg:S.val = P g + P! fh1:-S.val (evenShiftFst (Fin.last n)) + -S.val (evenShiftSnd (Fin.last n)) = 0⊢ (S.val (evenShiftSnd (Fin.last n)), S.val (evenShiftFst (Fin.last n)), S.val evenShiftLast).1 =
  -(S.val (evenShiftSnd (Fin.last n)), S.val (evenShiftFst (Fin.last n)), S.val evenShiftLast).2.1 linear_combination -(1 * h1)All goals completed! 🐙))
  ·inr.inrn:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsLIC:LineInCubicPerm Sg:Fin (n + 1).succ → ℚf:Fin (n + 1) → ℚhfg:S.val = P g + P! fh1:2 * S.val evenShiftLast + S.val (evenShiftSnd (Fin.last n)) + S.val (evenShiftFst (Fin.last n)) = 0⊢ LineInPlaneProp (S.val (evenShiftSnd (Fin.last n)), S.val (evenShiftFst (Fin.last n)), S.val evenShiftLast) exact Or.inr (Or.inr h1)All goals completed! 🐙lemma lineInCubicPerm_last_perm {S : (PureU1 (2 * n.succ.succ)).LinSols}
    (LIC : LineInCubicPerm S) : LineInPlaneCond S := byn:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsLIC:LineInCubicPerm S⊢ LineInPlaneCond S
  refine @Prop_three (2 * n.succ.succ) LineInPlaneProp S
    (evenShiftSnd (Fin.last n)) (evenShiftFst (Fin.last n))
    evenShiftLast ?_ ?_ ?_ ?_refine_1n:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsLIC:LineInCubicPerm S⊢ evenShiftSnd (Fin.last n) ≠ evenShiftFst (Fin.last n)refine_2n:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsLIC:LineInCubicPerm S⊢ evenShiftSnd (Fin.last n) ≠ evenShiftLastrefine_3n:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsLIC:LineInCubicPerm S⊢ evenShiftFst (Fin.last n) ≠ evenShiftLastrefine_4n:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsLIC:LineInCubicPerm S⊢ ∀ (f : (FamilyPermutations (2 * n.succ.succ)).group),
  LineInPlaneProp
    ((((FamilyPermutations (2 * n.succ.succ)).linSolRep f) S).val (evenShiftSnd (Fin.last n)),
      (((FamilyPermutations (2 * n.succ.succ)).linSolRep f) S).val (evenShiftFst (Fin.last n)),
      (((FamilyPermutations (2 * n.succ.succ)).linSolRep f) S).val evenShiftLast)
  ·refine_1n:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsLIC:LineInCubicPerm S⊢ evenShiftSnd (Fin.last n) ≠ evenShiftFst (Fin.last n) simp [Fin.ext_iff, evenShiftSnd, evenShiftFst]All goals completed! 🐙
  ·refine_2n:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsLIC:LineInCubicPerm S⊢ evenShiftSnd (Fin.last n) ≠ evenShiftLast simp [Fin.ext_iff, evenShiftSnd, evenShiftLast]All goals completed! 🐙
  ·refine_3n:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsLIC:LineInCubicPerm S⊢ evenShiftFst (Fin.last n) ≠ evenShiftLast simp [Fin.ext_iff, evenShiftFst, evenShiftLast]refine_3n:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsLIC:LineInCubicPerm S⊢ ¬n = n + 1 + (n + 1)
    omegaAll goals completed! 🐙
  ·refine_4n:ℕS:(PureU1 (2 * n.succ.succ)).LinSolsLIC:LineInCubicPerm S⊢ ∀ (f : (FamilyPermutations (2 * n.succ.succ)).group),
  LineInPlaneProp
    ((((FamilyPermutations (2 * n.succ.succ)).linSolRep f) S).val (evenShiftSnd (Fin.last n)),
      (((FamilyPermutations (2 * n.succ.succ)).linSolRep f) S).val (evenShiftFst (Fin.last n)),
      (((FamilyPermutations (2 * n.succ.succ)).linSolRep f) S).val evenShiftLast) exact fun M => lineInCubicPerm_last_cond (lineInCubicPerm_permute LIC M)All goals completed! 🐙lemma lineInCubicPerm_constAbs {S : (PureU1 (2 * n.succ.succ)).Sols}
    (LIC : LineInCubicPerm S.1.1) : ConstAbs S.val :=
  linesInPlane_constAbs_AF S (lineInCubicPerm_last_perm LIC)theorem lineInCubicPerm_vectorLike {S : (PureU1 (2 * n.succ.succ)).Sols}
    (LIC : LineInCubicPerm S.1.1) : VectorLikeEven S.val :=
  ConstAbs.boundary_value_even S.1.1 (lineInCubicPerm_constAbs LIC)theorem lineInCubicPerm_in_plane (S : (PureU1 (2 * n.succ.succ)).Sols)
    (LIC : LineInCubicPerm S.1.1) : ∃ (M : (FamilyPermutations (2 * n.succ.succ)).group),
    (FamilyPermutations (2 * n.succ.succ)).linSolRep M S.1.1
    ∈ Submodule.span ℚ (Set.range basis) :=
  vectorLikeEven_in_span S.1.1 (lineInCubicPerm_vectorLike LIC)