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

Line In Cubic Odd 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 the charge must be zero.

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 + 1)).LinSols) : Prop :=
  ∀ (g f : Fin n → ℚ) (_ : S.val = Pa g f) (a b : ℚ),
  accCube (2 * n + 1) (a • P g + b • P! f) = 0

The condition that a linear solution sits on a line between the two planes within the cubic expands into a on accCubeTriLinSymm applied to the points within the planes.

set_option backward.isDefEq.respectTransparency false in

lemma lineInCubic_expand {S : (PureU1 (2 * n + 1)).LinSols} (h : LineInCubic S) :
    ∀ (g : Fin n → ℚ) (f : Fin n → ℚ) (_ : S.val = P g + P! 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 + 1)).LinSolsh:LineInCubic S⊢ ∀ (g f : Fin n → ℚ),
  S.val = P g + P! 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 + 1)).LinSolsh:LineInCubic Sg:Fin n → ℚf:Fin n → ℚhS:S.val = P g + P! 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 + 1)).LinSolsh:LineInCubic Sg:Fin n → ℚf:Fin n → ℚhS:S.val = P g + P! fa:ℚb:ℚh1:(accCube (2 * n + 1)) (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 + 1)).LinSolsh:LineInCubic Sg:Fin n → ℚf:Fin n → ℚhS:S.val = P g + P! 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 + 1)).LinSolsh:LineInCubic Sg:Fin n → ℚf:Fin n → ℚhS:S.val = P g + P! 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 + 1)).LinSolsh:LineInCubic Sg:Fin n → ℚf:Fin n → ℚhS:S.val = P g + P! 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 + 1)).LinSolsh:LineInCubic Sg:Fin n → ℚf:Fin n → ℚhS:S.val = P g + P! 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 + 1)).LinSolsh:LineInCubic Sg:Fin n → ℚf:Fin n → ℚhS:S.val = P g + P! 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! 🐙

lemma line_in_cubic_P_P_P! {S : (PureU1 (2 * n + 1)).LinSols} (h : LineInCubic S) :
    ∀ (g : Fin n → ℚ) (f : Fin n → ℚ) (_ : S.val = P g + P! f),
    accCubeTriLinSymm (P g) (P g) (P! f) = 0 := byn:ℕS:(PureU1 (2 * n + 1)).LinSolsh:LineInCubic S⊢ ∀ (g 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 + 1)).LinSolsh:LineInCubic Sg:Fin n → ℚ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 + 1)).LinSols) : Prop :=
  ∀ (M : (FamilyPermutations (2 * n + 1)).group),
    LineInCubic ((FamilyPermutations (2 * n + 1)).linSolRep M S)

If lineInCubicPerm S, then lineInCubic S.

lemma lineInCubicPerm_self {S : (PureU1 (2 * n + 1)).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 + 1)).LinSols}
    (hS : LineInCubicPerm S) (M' : (FamilyPermutations (2 * n + 1)).group) :
    LineInCubicPerm ((FamilyPermutations (2 * n + 1)).linSolRep M' S) :=
  fun M => hS (M * M')

              

set_option backward.isDefEq.respectTransparency false in
lemma lineInCubicPerm_swap {S : (PureU1 (2 * n.succ + 1)).LinSols}
    (LIC : LineInCubicPerm S) :
    ∀ (j : Fin n.succ) (g f : Fin n.succ → ℚ) (_ : S.val = Pa g f),
      (S.val (oddShiftSnd j) - S.val (oddShiftFst j))
      * accCubeTriLinSymm (P g) (P g) (basis!AsCharges j) = 0 := byn:ℕS:(PureU1 (2 * n.succ + 1)).LinSolsLIC:LineInCubicPerm S⊢ ∀ (j : Fin n.succ) (g f : Fin n.succ → ℚ),
  S.val = Pa g f →
    (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0
  intro j g f hn:ℕS:(PureU1 (2 * n.succ + 1)).LinSolsLIC:LineInCubicPerm Sj:Fin n.succg:Fin n.succ → ℚf:Fin n.succ → ℚh:S.val = Pa g f⊢ (S.val (oddShiftSnd j) - S.val (oddShiftFst 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 + 1)).LinSolsLIC:LineInCubicPerm Sj:Fin n.succg:Fin n.succ → ℚf:Fin n.succ → ℚh:S.val = Pa g fg':Fin n.succ → ℚf':Fin n.succ → ℚhall:(((FamilyPermutations (2 * n.succ + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S).val = P g' + P! f' ∧
  P! f' = P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∧ g' = g⊢ (S.val (oddShiftSnd j) - S.val (oddShiftFst 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 + 1)).LinSolsLIC:LineInCubicPerm Sj:Fin n.succg:Fin n.succ → ℚf:Fin n.succ → ℚh:S.val = Pa g fg':Fin n.succ → ℚf':Fin n.succ → ℚhall:(((FamilyPermutations (2 * n.succ + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S).val = P g' + P! f' ∧
  P! f' = P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∧ g' = gh1:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0⊢ (S.val (oddShiftSnd j) - S.val (oddShiftFst 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 (oddShiftFst j) (oddShiftSnd j)))) g' f' hall.1n:ℕS:(PureU1 (2 * n.succ + 1)).LinSolsLIC:LineInCubicPerm Sj:Fin n.succg:Fin n.succ → ℚf:Fin n.succ → ℚh:S.val = Pa g fg':Fin n.succ → ℚf':Fin n.succ → ℚhall:(((FamilyPermutations (2 * n.succ + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S).val = P g' + P! f' ∧
  P! f' = P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∧ g' = gh1:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0h2:((accCubeTriLinSymm (P g')) (P g')) (P! f') = 0⊢ (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0
  rw [hall.2.1,n:ℕS:(PureU1 (2 * n.succ + 1)).LinSolsLIC:LineInCubicPerm Sj:Fin n.succg:Fin n.succ → ℚf:Fin n.succ → ℚh:S.val = Pa g fg':Fin n.succ → ℚf':Fin n.succ → ℚhall:(((FamilyPermutations (2 * n.succ + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S).val = P g' + P! f' ∧
  P! f' = P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∧ g' = gh1:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0h2:((accCubeTriLinSymm (P g')) (P g')) (P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j) = 0⊢ (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0n:ℕS:(PureU1 (2 * n.succ + 1)).LinSolsLIC:LineInCubicPerm Sj:Fin n.succg:Fin n.succ → ℚf:Fin n.succ → ℚh:S.val = Pa g fg':Fin n.succ → ℚf':Fin n.succ → ℚhall:(((FamilyPermutations (2 * n.succ + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S).val = P g' + P! f' ∧
  P! f' = P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∧ g' = gh1:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0h2:0 + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0⊢ (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0 hall.2.2,n:ℕS:(PureU1 (2 * n.succ + 1)).LinSolsLIC:LineInCubicPerm Sj:Fin n.succg:Fin n.succ → ℚf:Fin n.succ → ℚh:S.val = Pa g fg':Fin n.succ → ℚf':Fin n.succ → ℚhall:(((FamilyPermutations (2 * n.succ + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S).val = P g' + P! f' ∧
  P! f' = P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∧ g' = gh1:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0h2:((accCubeTriLinSymm (P g)) (P g)) (P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j) = 0⊢ (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0n:ℕS:(PureU1 (2 * n.succ + 1)).LinSolsLIC:LineInCubicPerm Sj:Fin n.succg:Fin n.succ → ℚf:Fin n.succ → ℚh:S.val = Pa g fg':Fin n.succ → ℚf':Fin n.succ → ℚhall:(((FamilyPermutations (2 * n.succ + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S).val = P g' + P! f' ∧
  P! f' = P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∧ g' = gh1:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0h2:0 + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0⊢ (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0 accCubeTriLinSymm.map_add₃,n:ℕS:(PureU1 (2 * n.succ + 1)).LinSolsLIC:LineInCubicPerm Sj:Fin n.succg:Fin n.succ → ℚf:Fin n.succ → ℚh:S.val = Pa g fg':Fin n.succ → ℚf':Fin n.succ → ℚhall:(((FamilyPermutations (2 * n.succ + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S).val = P g' + P! f' ∧
  P! f' = P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst 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 (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j) =
  0⊢ (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0n:ℕS:(PureU1 (2 * n.succ + 1)).LinSolsLIC:LineInCubicPerm Sj:Fin n.succg:Fin n.succ → ℚf:Fin n.succ → ℚh:S.val = Pa g fg':Fin n.succ → ℚf':Fin n.succ → ℚhall:(((FamilyPermutations (2 * n.succ + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S).val = P g' + P! f' ∧
  P! f' = P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∧ g' = gh1:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0h2:0 + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0⊢ (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0 h1,n:ℕS:(PureU1 (2 * n.succ + 1)).LinSolsLIC:LineInCubicPerm Sj:Fin n.succg:Fin n.succ → ℚf:Fin n.succ → ℚh:S.val = Pa g fg':Fin n.succ → ℚf':Fin n.succ → ℚhall:(((FamilyPermutations (2 * n.succ + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S).val = P g' + P! f' ∧
  P! f' = P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∧ g' = gh1:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0h2:0 + ((accCubeTriLinSymm (P g)) (P g)) ((S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j) = 0⊢ (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0n:ℕS:(PureU1 (2 * n.succ + 1)).LinSolsLIC:LineInCubicPerm Sj:Fin n.succg:Fin n.succ → ℚf:Fin n.succ → ℚh:S.val = Pa g fg':Fin n.succ → ℚf':Fin n.succ → ℚhall:(((FamilyPermutations (2 * n.succ + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S).val = P g' + P! f' ∧
  P! f' = P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∧ g' = gh1:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0h2:0 + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0⊢ (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0 accCubeTriLinSymm.map_smul₃n:ℕS:(PureU1 (2 * n.succ + 1)).LinSolsLIC:LineInCubicPerm Sj:Fin n.succg:Fin n.succ → ℚf:Fin n.succ → ℚh:S.val = Pa g fg':Fin n.succ → ℚf':Fin n.succ → ℚhall:(((FamilyPermutations (2 * n.succ + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S).val = P g' + P! f' ∧
  P! f' = P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∧ g' = gh1:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0h2:0 + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0⊢ (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0n:ℕS:(PureU1 (2 * n.succ + 1)).LinSolsLIC:LineInCubicPerm Sj:Fin n.succg:Fin n.succ → ℚf:Fin n.succ → ℚh:S.val = Pa g fg':Fin n.succ → ℚf':Fin n.succ → ℚhall:(((FamilyPermutations (2 * n.succ + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S).val = P g' + P! f' ∧
  P! f' = P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∧ g' = gh1:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0h2:0 + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0⊢ (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0] at h2n:ℕS:(PureU1 (2 * n.succ + 1)).LinSolsLIC:LineInCubicPerm Sj:Fin n.succg:Fin n.succ → ℚf:Fin n.succ → ℚh:S.val = Pa g fg':Fin n.succ → ℚf':Fin n.succ → ℚhall:(((FamilyPermutations (2 * n.succ + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S).val = P g' + P! f' ∧
  P! f' = P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∧ g' = gh1:((accCubeTriLinSymm (P g)) (P g)) (P! f) = 0h2:0 + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = 0⊢ (S.val (oddShiftSnd j) - S.val (oddShiftFst 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 + 1)).LinSols}
    (f g : Fin n.succ.succ → ℚ) (hS : S.val = Pa f g) :
    accCubeTriLinSymm (P f) (P f) (basis!AsCharges 0) =
    (S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
    (2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) := byn:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ.succ → ℚhS:S.val = Pa f g⊢ ((accCubeTriLinSymm (P f)) (P f)) (basis!AsCharges 0) =
  (S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
    (2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0))
  rw [P_P_P!_accCube f 0,n:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ.succ → ℚhS:S.val = Pa f g⊢ P f (oddShiftFst 0) ^ 2 - f 0 ^ 2 =
  (S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
    (2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0))n:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ.succ → ℚhS:S.val = Pa f g⊢ P f (oddShiftFst 0) ^ 2 - S.val oddShiftShiftZero ^ 2 =
  (S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
    (2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) ← Pa_oddShiftShiftZero f g,n:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ.succ → ℚhS:S.val = Pa f g⊢ P f (oddShiftFst 0) ^ 2 - Pa f g oddShiftShiftZero ^ 2 =
  (S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
    (2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0))n:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ.succ → ℚhS:S.val = Pa f g⊢ P f (oddShiftFst 0) ^ 2 - S.val oddShiftShiftZero ^ 2 =
  (S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
    (2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) ← hSn:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ.succ → ℚhS:S.val = Pa f g⊢ P f (oddShiftFst 0) ^ 2 - S.val oddShiftShiftZero ^ 2 =
  (S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
    (2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0))n:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ.succ → ℚhS:S.val = Pa f g⊢ P f (oddShiftFst 0) ^ 2 - S.val oddShiftShiftZero ^ 2 =
  (S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
    (2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0))]n:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ.succ → ℚhS:S.val = Pa f g⊢ P f (oddShiftFst 0) ^ 2 - S.val oddShiftShiftZero ^ 2 =
  (S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
    (2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0))
  nth_rewrite 1 [show oddShiftFst (0 : Fin n.succ.succ) = oddFst 1 from rfl]n:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ.succ → ℚhS:S.val = Pa f g⊢ P f (oddFst 1) ^ 2 - S.val oddShiftShiftZero ^ 2 =
  (S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
    (2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0))
  rw [P_oddFstn:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ.succ → ℚhS:S.val = Pa f g⊢ f 1 ^ 2 - S.val oddShiftShiftZero ^ 2 =
  (S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
    (2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0))n:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ.succ → ℚhS:S.val = Pa f g⊢ f 1 ^ 2 - S.val oddShiftShiftZero ^ 2 =
  (S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
    (2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0))]n:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ.succ → ℚhS:S.val = Pa f g⊢ f 1 ^ 2 - S.val oddShiftShiftZero ^ 2 =
  (S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
    (2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0))
  have h1 := Pa_oddShiftShiftZero f gn:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ.succ → ℚhS:S.val = Pa f gh1:Pa f g oddShiftShiftZero = f 0⊢ f 1 ^ 2 - S.val oddShiftShiftZero ^ 2 =
  (S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
    (2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0))
  have h4 := Pa_oddShiftShiftSnd f g 0n:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ.succ → ℚhS:S.val = Pa f gh1:Pa f g oddShiftShiftZero = f 0h4:Pa f g (oddShiftShiftSnd 0) = -f 0 - g 0⊢ f 1 ^ 2 - S.val oddShiftShiftZero ^ 2 =
  (S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
    (2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0))
  have h2 := Pa_oddShiftShiftFst f g 0n:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ.succ → ℚhS:S.val = Pa f gh1:Pa f g oddShiftShiftZero = f 0h4:Pa f g (oddShiftShiftSnd 0) = -f 0 - g 0h2:Pa f g (oddShiftShiftFst 0) = f (Fin.succ 0) + g (Fin.castSucc 0)⊢ f 1 ^ 2 - S.val oddShiftShiftZero ^ 2 =
  (S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
    (2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0))
  rw [← hSn:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ.succ → ℚhS:S.val = Pa f gh1:S.val oddShiftShiftZero = f 0h4:S.val (oddShiftShiftSnd 0) = -f 0 - g 0h2:S.val (oddShiftShiftFst 0) = f (Fin.succ 0) + g (Fin.castSucc 0)⊢ f 1 ^ 2 - S.val oddShiftShiftZero ^ 2 =
  (S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
    (2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0))n:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ.succ → ℚhS:S.val = Pa f gh1:S.val oddShiftShiftZero = f 0h4:S.val (oddShiftShiftSnd 0) = -f 0 - g 0h2:S.val (oddShiftShiftFst 0) = f (Fin.succ 0) + g (Fin.castSucc 0)⊢ f 1 ^ 2 - S.val oddShiftShiftZero ^ 2 =
  (S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
    (2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0))] at h1 h2 h4n:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ.succ → ℚhS:S.val = Pa f gh1:S.val oddShiftShiftZero = f 0h4:S.val (oddShiftShiftSnd 0) = -f 0 - g 0h2:S.val (oddShiftShiftFst 0) = f (Fin.succ 0) + g (Fin.castSucc 0)⊢ f 1 ^ 2 - S.val oddShiftShiftZero ^ 2 =
  (S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
    (2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0))
  simp only [Nat.succ_eq_add_one, Fin.succ_zero_eq_one, Fin.castSucc_zero] at h2n:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ.succ → ℚhS:S.val = Pa f gh1:S.val oddShiftShiftZero = f 0h4:S.val (oddShiftShiftSnd 0) = -f 0 - g 0h2:S.val (oddShiftShiftFst 0) = f 1 + g 0⊢ f 1 ^ 2 - S.val oddShiftShiftZero ^ 2 =
  (S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
    (2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0))
  have h5 : f 1 = S.val (oddShiftShiftFst 0) + S.val oddShiftShiftZero +
      S.val (oddShiftShiftSnd 0) := byn:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ.succ → ℚhS:S.val = Pa f g⊢ ((accCubeTriLinSymm (P f)) (P f)) (basis!AsCharges 0) =
  (S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
    (2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0))n:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ.succ → ℚhS:S.val = Pa f gh1:S.val oddShiftShiftZero = f 0h4:S.val (oddShiftShiftSnd 0) = -f 0 - g 0h2:S.val (oddShiftShiftFst 0) = f 1 + g 0h5:f 1 = S.val (oddShiftShiftFst 0) + S.val oddShiftShiftZero + S.val (oddShiftShiftSnd 0)⊢ f 1 ^ 2 - S.val oddShiftShiftZero ^ 2 =
  (S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
    (2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0))
    linear_combination -h1 - h4 - h2n:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ.succ → ℚhS:S.val = Pa f gh1:S.val oddShiftShiftZero = f 0h4:S.val (oddShiftShiftSnd 0) = -f 0 - g 0h2:S.val (oddShiftShiftFst 0) = f 1 + g 0h5:f 1 = S.val (oddShiftShiftFst 0) + S.val oddShiftShiftZero + S.val (oddShiftShiftSnd 0)⊢ f 1 ^ 2 - S.val oddShiftShiftZero ^ 2 =
  (S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
    (2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0))n:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ.succ → ℚhS:S.val = Pa f gh1:S.val oddShiftShiftZero = f 0h4:S.val (oddShiftShiftSnd 0) = -f 0 - g 0h2:S.val (oddShiftShiftFst 0) = f 1 + g 0h5:f 1 = S.val (oddShiftShiftFst 0) + S.val oddShiftShiftZero + S.val (oddShiftShiftSnd 0)⊢ f 1 ^ 2 - S.val oddShiftShiftZero ^ 2 =
  (S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
    (2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0))
  rw [h5,n:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ.succ → ℚhS:S.val = Pa f gh1:S.val oddShiftShiftZero = f 0h4:S.val (oddShiftShiftSnd 0) = -f 0 - g 0h2:S.val (oddShiftShiftFst 0) = f 1 + g 0h5:f 1 = S.val (oddShiftShiftFst 0) + S.val oddShiftShiftZero + S.val (oddShiftShiftSnd 0)⊢ (S.val (oddShiftShiftFst 0) + S.val oddShiftShiftZero + S.val (oddShiftShiftSnd 0)) ^ 2 - S.val oddShiftShiftZero ^ 2 =
  (S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
    (2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0))n:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ.succ → ℚhS:S.val = Pa f gh1:S.val oddShiftShiftZero = f 0h4:S.val (oddShiftShiftSnd 0) = -f 0 - g 0h2:S.val (oddShiftShiftFst 0) = f 1 + g 0h5:f 1 = S.val (oddShiftShiftFst 0) + S.val oddShiftShiftZero + S.val (oddShiftShiftSnd 0)⊢ (S.val (oddShiftFst 0) + S.val oddShiftZero + S.val (oddShiftSnd 0)) ^ 2 - S.val oddShiftZero ^ 2 =
  (S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
    (2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) oddShiftShiftSnd_eq_oddShiftSnd,n:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ.succ → ℚhS:S.val = Pa f gh1:S.val oddShiftShiftZero = f 0h4:S.val (oddShiftShiftSnd 0) = -f 0 - g 0h2:S.val (oddShiftShiftFst 0) = f 1 + g 0h5:f 1 = S.val (oddShiftShiftFst 0) + S.val oddShiftShiftZero + S.val (oddShiftShiftSnd 0)⊢ (S.val (oddShiftShiftFst 0) + S.val oddShiftShiftZero + S.val (oddShiftSnd 0)) ^ 2 - S.val oddShiftShiftZero ^ 2 =
  (S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
    (2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0))n:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ.succ → ℚhS:S.val = Pa f gh1:S.val oddShiftShiftZero = f 0h4:S.val (oddShiftShiftSnd 0) = -f 0 - g 0h2:S.val (oddShiftShiftFst 0) = f 1 + g 0h5:f 1 = S.val (oddShiftShiftFst 0) + S.val oddShiftShiftZero + S.val (oddShiftShiftSnd 0)⊢ (S.val (oddShiftFst 0) + S.val oddShiftZero + S.val (oddShiftSnd 0)) ^ 2 - S.val oddShiftZero ^ 2 =
  (S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
    (2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0))
    show (oddShiftShiftFst (0 : Fin n.succ)) = oddShiftFst 0 from rfl,n:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ.succ → ℚhS:S.val = Pa f gh1:S.val oddShiftShiftZero = f 0h4:S.val (oddShiftShiftSnd 0) = -f 0 - g 0h2:S.val (oddShiftShiftFst 0) = f 1 + g 0h5:f 1 = S.val (oddShiftShiftFst 0) + S.val oddShiftShiftZero + S.val (oddShiftShiftSnd 0)⊢ (S.val (oddShiftFst 0) + S.val oddShiftShiftZero + S.val (oddShiftSnd 0)) ^ 2 - S.val oddShiftShiftZero ^ 2 =
  (S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
    (2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0))n:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ.succ → ℚhS:S.val = Pa f gh1:S.val oddShiftShiftZero = f 0h4:S.val (oddShiftShiftSnd 0) = -f 0 - g 0h2:S.val (oddShiftShiftFst 0) = f 1 + g 0h5:f 1 = S.val (oddShiftShiftFst 0) + S.val oddShiftShiftZero + S.val (oddShiftShiftSnd 0)⊢ (S.val (oddShiftFst 0) + S.val oddShiftZero + S.val (oddShiftSnd 0)) ^ 2 - S.val oddShiftZero ^ 2 =
  (S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
    (2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0))
    oddShiftShiftZero_eq_oddShiftZeron:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ.succ → ℚhS:S.val = Pa f gh1:S.val oddShiftShiftZero = f 0h4:S.val (oddShiftShiftSnd 0) = -f 0 - g 0h2:S.val (oddShiftShiftFst 0) = f 1 + g 0h5:f 1 = S.val (oddShiftShiftFst 0) + S.val oddShiftShiftZero + S.val (oddShiftShiftSnd 0)⊢ (S.val (oddShiftFst 0) + S.val oddShiftZero + S.val (oddShiftSnd 0)) ^ 2 - S.val oddShiftZero ^ 2 =
  (S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
    (2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0))n:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ.succ → ℚhS:S.val = Pa f gh1:S.val oddShiftShiftZero = f 0h4:S.val (oddShiftShiftSnd 0) = -f 0 - g 0h2:S.val (oddShiftShiftFst 0) = f 1 + g 0h5:f 1 = S.val (oddShiftShiftFst 0) + S.val oddShiftShiftZero + S.val (oddShiftShiftSnd 0)⊢ (S.val (oddShiftFst 0) + S.val oddShiftZero + S.val (oddShiftSnd 0)) ^ 2 - S.val oddShiftZero ^ 2 =
  (S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
    (2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0))]n:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsf:Fin n.succ.succ → ℚg:Fin n.succ.succ → ℚhS:S.val = Pa f gh1:S.val oddShiftShiftZero = f 0h4:S.val (oddShiftShiftSnd 0) = -f 0 - g 0h2:S.val (oddShiftShiftFst 0) = f 1 + g 0h5:f 1 = S.val (oddShiftShiftFst 0) + S.val oddShiftShiftZero + S.val (oddShiftShiftSnd 0)⊢ (S.val (oddShiftFst 0) + S.val oddShiftZero + S.val (oddShiftSnd 0)) ^ 2 - S.val oddShiftZero ^ 2 =
  (S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
    (2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0))
  ringAll goals completed! 🐙

lemma lineInCubicPerm_last_cond {S : (PureU1 (2 * n.succ.succ+1)).LinSols}
    (LIC : LineInCubicPerm S) :
    LineInPlaneProp ((S.val (oddShiftSnd 0)), ((S.val (oddShiftFst 0)), (S.val oddShiftZero))) := byn:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsLIC:LineInCubicPerm S⊢ LineInPlaneProp (S.val (oddShiftSnd 0), S.val (oddShiftFst 0), S.val oddShiftZero)
  obtain ⟨g, f, hfg⟩ := span_basis Sn:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsLIC:LineInCubicPerm Sg:Fin (n + 1).succ → ℚf:Fin (n + 1).succ → ℚhfg:S.val = P g + P! f⊢ LineInPlaneProp (S.val (oddShiftSnd 0), S.val (oddShiftFst 0), S.val oddShiftZero)
  have h1 := lineInCubicPerm_swap LIC 0 g f hfgn:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsLIC:LineInCubicPerm Sg:Fin (n + 1).succ → ℚf:Fin (n + 1).succ → ℚhfg:S.val = P g + P! fh1:(S.val (oddShiftSnd 0) - S.val (oddShiftFst 0)) * ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges 0) = 0⊢ LineInPlaneProp (S.val (oddShiftSnd 0), S.val (oddShiftFst 0), S.val oddShiftZero)
  rw [P_P_P!_accCube' g f hfgn:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsLIC:LineInCubicPerm Sg:Fin (n + 1).succ → ℚf:Fin (n + 1).succ → ℚhfg:S.val = P g + P! fh1:(S.val (oddShiftSnd 0) - S.val (oddShiftFst 0)) *
    ((S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
      (2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0))) =
  0⊢ LineInPlaneProp (S.val (oddShiftSnd 0), S.val (oddShiftFst 0), S.val oddShiftZero)n:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsLIC:LineInCubicPerm Sg:Fin (n + 1).succ → ℚf:Fin (n + 1).succ → ℚhfg:S.val = P g + P! fh1:(S.val (oddShiftSnd 0) - S.val (oddShiftFst 0)) *
    ((S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
      (2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0))) =
  0⊢ LineInPlaneProp (S.val (oddShiftSnd 0), S.val (oddShiftFst 0), S.val oddShiftZero)] at h1n:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsLIC:LineInCubicPerm Sg:Fin (n + 1).succ → ℚf:Fin (n + 1).succ → ℚhfg:S.val = P g + P! fh1:(S.val (oddShiftSnd 0) - S.val (oddShiftFst 0)) *
    ((S.val (oddShiftFst 0) + S.val (oddShiftSnd 0)) *
      (2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0))) =
  0⊢ LineInPlaneProp (S.val (oddShiftSnd 0), S.val (oddShiftFst 0), S.val oddShiftZero)
  simp only [Nat.succ_eq_add_one, mul_eq_zero] at h1n:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsLIC:LineInCubicPerm Sg:Fin (n + 1).succ → ℚf:Fin (n + 1).succ → ℚhfg:S.val = P g + P! fh1:S.val (oddShiftSnd 0) - S.val (oddShiftFst 0) = 0 ∨
  S.val (oddShiftFst 0) + S.val (oddShiftSnd 0) = 0 ∨
    2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0) = 0⊢ LineInPlaneProp (S.val (oddShiftSnd 0), S.val (oddShiftFst 0), S.val oddShiftZero)
  rcases h1 with h1 | h1 | h1inln:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsLIC:LineInCubicPerm Sg:Fin (n + 1).succ → ℚf:Fin (n + 1).succ → ℚhfg:S.val = P g + P! fh1:S.val (oddShiftSnd 0) - S.val (oddShiftFst 0) = 0⊢ LineInPlaneProp (S.val (oddShiftSnd 0), S.val (oddShiftFst 0), S.val oddShiftZero)inr.inln:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsLIC:LineInCubicPerm Sg:Fin (n + 1).succ → ℚf:Fin (n + 1).succ → ℚhfg:S.val = P g + P! fh1:S.val (oddShiftFst 0) + S.val (oddShiftSnd 0) = 0⊢ LineInPlaneProp (S.val (oddShiftSnd 0), S.val (oddShiftFst 0), S.val oddShiftZero)inr.inrn:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsLIC:LineInCubicPerm Sg:Fin (n + 1).succ → ℚf:Fin (n + 1).succ → ℚhfg:S.val = P g + P! fh1:2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0) = 0⊢ LineInPlaneProp (S.val (oddShiftSnd 0), S.val (oddShiftFst 0), S.val oddShiftZero)
  ·inln:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsLIC:LineInCubicPerm Sg:Fin (n + 1).succ → ℚf:Fin (n + 1).succ → ℚhfg:S.val = P g + P! fh1:S.val (oddShiftSnd 0) - S.val (oddShiftFst 0) = 0⊢ LineInPlaneProp (S.val (oddShiftSnd 0), S.val (oddShiftFst 0), S.val oddShiftZero) exact Or.inl (byn:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsLIC:LineInCubicPerm Sg:Fin (n + 1).succ → ℚf:Fin (n + 1).succ → ℚhfg:S.val = P g + P! fh1:S.val (oddShiftSnd 0) - S.val (oddShiftFst 0) = 0⊢ (S.val (oddShiftSnd 0), S.val (oddShiftFst 0), S.val oddShiftZero).1 =
  (S.val (oddShiftSnd 0), S.val (oddShiftFst 0), S.val oddShiftZero).2.1 linear_combination h1All goals completed! 🐙)
  ·inr.inln:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsLIC:LineInCubicPerm Sg:Fin (n + 1).succ → ℚf:Fin (n + 1).succ → ℚhfg:S.val = P g + P! fh1:S.val (oddShiftFst 0) + S.val (oddShiftSnd 0) = 0⊢ LineInPlaneProp (S.val (oddShiftSnd 0), S.val (oddShiftFst 0), S.val oddShiftZero) exact Or.inr (Or.inl (byn:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsLIC:LineInCubicPerm Sg:Fin (n + 1).succ → ℚf:Fin (n + 1).succ → ℚhfg:S.val = P g + P! fh1:S.val (oddShiftFst 0) + S.val (oddShiftSnd 0) = 0⊢ (S.val (oddShiftSnd 0), S.val (oddShiftFst 0), S.val oddShiftZero).1 =
  -(S.val (oddShiftSnd 0), S.val (oddShiftFst 0), S.val oddShiftZero).2.1 linear_combination h1All goals completed! 🐙))
  ·inr.inrn:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsLIC:LineInCubicPerm Sg:Fin (n + 1).succ → ℚf:Fin (n + 1).succ → ℚhfg:S.val = P g + P! fh1:2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0) = 0⊢ LineInPlaneProp (S.val (oddShiftSnd 0), S.val (oddShiftFst 0), S.val oddShiftZero) exact Or.inr (Or.inr (byn:ℕS:(PureU1 (2 * n.succ.succ + 1)).LinSolsLIC:LineInCubicPerm Sg:Fin (n + 1).succ → ℚf:Fin (n + 1).succ → ℚhfg:S.val = P g + P! fh1:2 * S.val oddShiftZero + S.val (oddShiftFst 0) + S.val (oddShiftSnd 0) = 0⊢ 2 * (S.val (oddShiftSnd 0), S.val (oddShiftFst 0), S.val oddShiftZero).2.2 +
      (S.val (oddShiftSnd 0), S.val (oddShiftFst 0), S.val oddShiftZero).1 +
    (S.val (oddShiftSnd 0), S.val (oddShiftFst 0), S.val oddShiftZero).2.1 =
  0 linear_combination h1All goals completed! 🐙))lemma lineInCubicPerm_last_perm {S : (PureU1 (2 * n.succ.succ + 1)).LinSols}
    (LIC : LineInCubicPerm S) : LineInPlaneCond S :=
  @Prop_three (2 * n.succ.succ + 1) LineInPlaneProp S (oddShiftSnd 0) (oddShiftFst 0)
    oddShiftZero (ne_of_beq_false rfl) (ne_of_beq_false rfl) (ne_of_beq_false rfl)
    (fun M => lineInCubicPerm_last_cond (lineInCubicPerm_permute LIC M))lemma lineInCubicPerm_constAbs {S : (PureU1 (2 * n.succ.succ + 1)).LinSols}
    (LIC : LineInCubicPerm S) : ConstAbs S.val :=
  linesInPlane_constAbs (lineInCubicPerm_last_perm LIC)theorem lineInCubicPerm_zero {S : (PureU1 (2 * n.succ.succ + 1)).LinSols}
    (LIC : LineInCubicPerm S) : S = 0 :=
  ConstAbs.boundary_value_odd S (lineInCubicPerm_constAbs LIC)