Physlib.QFT.QED.AnomalyCancellation.Odd.BasisLinear

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

Splitting the linear solutions in the odd case into two ACC-satisfying planes

i. Overview

We split the linear solutions of PureU1 (2 * n + 1) into two planes, where every point in either plane satisfies both the linear and cubic anomaly cancellation conditions.

ii. Key results

Unshifted.planeLinSols : The inclusion of the unshifted plane into linear solutions

Unshifted.planeCharges_accCube : The statement that charges from the unshifted plane satisfy the cubic ACC

Shifted.planeLinSols : The inclusion of the shifted plane.

Shifted.planeCharges_accCube : The statement that charges from the shifted plane satisfy the cubic ACC

span_basis : Every linear solution is the sum of a point from each plane.

iii. Table of contents

A. Splitting the charges up into groups

A.1. The symmetric split: Spltting the charges up via (n + 1) + 1

A.2. The shifted split: Spltting the charges up via 1 + n + n

A.3. The shifte shifted split: Spltting the charges up via ((1+n)+1) + n.succ

A.4. Relating the splittings together

B. The unshifted plane

B.1. The basis vectors of the unshifted plane as charges

B.2. Components of the basis vectors as charges

B.3. The basis vectors satisfy the linear ACCs

B.4. The basis vectors as LinSols

B.5. The inclusion of the unshifted plane into charges

B.6. Components of the unshifted plane

B.7. Points on the unshifted plane satisfies the ACCs

B.8. Kernel of the inclusion into charges

B.9. The basis vectors are linearly independent

C. The shifted plane

C.1. The basis vectors of the shifted plane as charges

C.2. Components of the basis vectors as charges

C.3. The basis vectors satisfy the linear ACCs

C.4. The basis vectors as LinSols

C.5. Permutations equal adding basis vectors

C.6. The inclusion of the shifted plane into charges

C.7. Components of the shifted plane

C.8. Points on the shifted plane satisfies the ACCs

C.9. Kernel of the inclusion into charges

C.10. The inclusion of the shifted plane into LinSols

C.11. The basis vectors are linearly independent

D. The mixed cubic ACC from points in both planes

E. The combined basis

E.1. The combined basis as LinSols

E.2. The inclusion of the span of the combined basis into charges

E.3. Components of the inclusion

E.4. Kernel of the inclusion into charges

E.5. The inclusion of the span of the combined basis into LinSols

E.6. The combined basis vectors are linearly independent

E.7. Injectivity of the inclusion into linear solutions

E.8. Cardinality of the basis

E.9. The basis vectors as a basis

F. Every Lienar solution is the sum of a point from each plane

F.1. Relation under permutations

iv. References

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

@[expose] public section

A. Splitting the charges up into groups

We have 2 * n + 1 charges, which we split up in the following ways:

| evenFst j (0 to n) | evenSnd j (n.succ to n + n.succ)|

| evenShiftZero (0) | evenShiftFst j (1 to n) |
  evenShiftSnd j (n.succ to 2 * n) | evenShiftLast (2 * n.succ - 1) |

A.1. The symmetric split: Spltting the charges up via `(n + 1) + 1`

lemma odd_shift_eq (n : ℕ) : (1 + n) + n = 2 * n +1 := byn:ℕ⊢ 1 + n + n = 2 * n + 1
  omegaAll goals completed! 🐙

The inclusion of Fin n into Fin ((n + 1) + n) via the first n. This is then casted to Fin (2 * n + 1).

def oddFst (j : Fin n) : Fin (2 * n + 1) :=
  Fin.cast (split_odd n) (Fin.castAdd n (Fin.castAdd 1 j))

The inclusion of Fin n into Fin ((n + 1) + n) via the second n. This is then casted to Fin (2 * n + 1).

def oddSnd (j : Fin n) : Fin (2 * n + 1) :=
  Fin.cast (split_odd n) (Fin.natAdd (n+1) j)

The element representing 1 in Fin ((n + 1) + n). This is then casted to Fin (2 * n + 1).

def oddMid : Fin (2 * n + 1) :=
  Fin.cast (split_odd n) (Fin.castAdd n (Fin.natAdd n 1))



lemma sum_odd (S : Fin (2 * n + 1) → ℚ) :
    ∑ i, S i = S oddMid + ∑ i : Fin n, ((S ∘ oddFst) i + (S ∘ oddSnd) i) := byn:ℕS:Fin (2 * n + 1) → ℚ⊢ ∑ i, S i = S oddMid + ∑ i, ((S ∘ oddFst) i + (S ∘ oddSnd) i)
  have h1 : ∑ i, S i = ∑ i : Fin (n + 1 + n), S (Fin.cast (split_odd n) i) :=
    (Equiv.sum_comp (finCongr (split_odd n)) S).symmn:ℕS:Fin (2 * n + 1) → ℚh1:∑ i, S i = ∑ i, S (Fin.cast ⋯ i)⊢ ∑ i, S i = S oddMid + ∑ i, ((S ∘ oddFst) i + (S ∘ oddSnd) i)
  rw [h1,n:ℕS:Fin (2 * n + 1) → ℚh1:∑ i, S i = ∑ i, S (Fin.cast ⋯ i)⊢ ∑ i, S (Fin.cast ⋯ i) = S oddMid + ∑ i, ((S ∘ oddFst) i + (S ∘ oddSnd) i)n:ℕS:Fin (2 * n + 1) → ℚh1:∑ i, S i = ∑ i, S (Fin.cast ⋯ i)⊢ ∑ i, S (Fin.cast ⋯ (Fin.castAdd n (Fin.castAdd 1 i))) + ∑ i, S (Fin.cast ⋯ (Fin.castAdd n (Fin.natAdd n i))) +
    ∑ i, S (Fin.cast ⋯ (Fin.natAdd (n + 1) i)) =
  S oddMid + ∑ i, ((S ∘ oddFst) i + (S ∘ oddSnd) i) Fin.sum_univ_add,n:ℕS:Fin (2 * n + 1) → ℚh1:∑ i, S i = ∑ i, S (Fin.cast ⋯ i)⊢ ∑ i, S (Fin.cast ⋯ (Fin.castAdd n i)) + ∑ i, S (Fin.cast ⋯ (Fin.natAdd (n + 1) i)) =
  S oddMid + ∑ i, ((S ∘ oddFst) i + (S ∘ oddSnd) i)n:ℕS:Fin (2 * n + 1) → ℚh1:∑ i, S i = ∑ i, S (Fin.cast ⋯ i)⊢ ∑ i, S (Fin.cast ⋯ (Fin.castAdd n (Fin.castAdd 1 i))) + ∑ i, S (Fin.cast ⋯ (Fin.castAdd n (Fin.natAdd n i))) +
    ∑ i, S (Fin.cast ⋯ (Fin.natAdd (n + 1) i)) =
  S oddMid + ∑ i, ((S ∘ oddFst) i + (S ∘ oddSnd) i) Fin.sum_univ_addn:ℕS:Fin (2 * n + 1) → ℚh1:∑ i, S i = ∑ i, S (Fin.cast ⋯ i)⊢ ∑ i, S (Fin.cast ⋯ (Fin.castAdd n (Fin.castAdd 1 i))) + ∑ i, S (Fin.cast ⋯ (Fin.castAdd n (Fin.natAdd n i))) +
    ∑ i, S (Fin.cast ⋯ (Fin.natAdd (n + 1) i)) =
  S oddMid + ∑ i, ((S ∘ oddFst) i + (S ∘ oddSnd) i)n:ℕS:Fin (2 * n + 1) → ℚh1:∑ i, S i = ∑ i, S (Fin.cast ⋯ i)⊢ ∑ i, S (Fin.cast ⋯ (Fin.castAdd n (Fin.castAdd 1 i))) + ∑ i, S (Fin.cast ⋯ (Fin.castAdd n (Fin.natAdd n i))) +
    ∑ i, S (Fin.cast ⋯ (Fin.natAdd (n + 1) i)) =
  S oddMid + ∑ i, ((S ∘ oddFst) i + (S ∘ oddSnd) i)]n:ℕS:Fin (2 * n + 1) → ℚh1:∑ i, S i = ∑ i, S (Fin.cast ⋯ i)⊢ ∑ i, S (Fin.cast ⋯ (Fin.castAdd n (Fin.castAdd 1 i))) + ∑ i, S (Fin.cast ⋯ (Fin.castAdd n (Fin.natAdd n i))) +
    ∑ i, S (Fin.cast ⋯ (Fin.natAdd (n + 1) i)) =
  S oddMid + ∑ i, ((S ∘ oddFst) i + (S ∘ oddSnd) i)
  simp only [univ_unique, Fin.default_eq_zero, Fin.isValue, sum_singleton, Function.comp_apply]n:ℕS:Fin (2 * n + 1) → ℚh1:∑ i, S i = ∑ i, S (Fin.cast ⋯ i)⊢ ∑ i, S (Fin.cast ⋯ (Fin.castAdd n (Fin.castAdd 1 i))) + S (Fin.cast ⋯ (Fin.castAdd n (Fin.natAdd n 0))) +
    ∑ i, S (Fin.cast ⋯ (Fin.natAdd (n + 1) i)) =
  S oddMid + ∑ x, (S (oddFst x) + S (oddSnd x))
  nth_rewrite 2 [add_comm]n:ℕS:Fin (2 * n + 1) → ℚh1:∑ i, S i = ∑ i, S (Fin.cast ⋯ i)⊢ S (Fin.cast ⋯ (Fin.castAdd n (Fin.natAdd n 0))) + ∑ i, S (Fin.cast ⋯ (Fin.castAdd n (Fin.castAdd 1 i))) +
    ∑ i, S (Fin.cast ⋯ (Fin.natAdd (n + 1) i)) =
  S oddMid + ∑ x, (S (oddFst x) + S (oddSnd x))
  rw [add_assocn:ℕS:Fin (2 * n + 1) → ℚh1:∑ i, S i = ∑ i, S (Fin.cast ⋯ i)⊢ S (Fin.cast ⋯ (Fin.castAdd n (Fin.natAdd n 0))) +
    (∑ i, S (Fin.cast ⋯ (Fin.castAdd n (Fin.castAdd 1 i))) + ∑ i, S (Fin.cast ⋯ (Fin.natAdd (n + 1) i))) =
  S oddMid + ∑ x, (S (oddFst x) + S (oddSnd x))n:ℕS:Fin (2 * n + 1) → ℚh1:∑ i, S i = ∑ i, S (Fin.cast ⋯ i)⊢ S (Fin.cast ⋯ (Fin.castAdd n (Fin.natAdd n 0))) +
    (∑ i, S (Fin.cast ⋯ (Fin.castAdd n (Fin.castAdd 1 i))) + ∑ i, S (Fin.cast ⋯ (Fin.natAdd (n + 1) i))) =
  S oddMid + ∑ x, (S (oddFst x) + S (oddSnd x))]n:ℕS:Fin (2 * n + 1) → ℚh1:∑ i, S i = ∑ i, S (Fin.cast ⋯ i)⊢ S (Fin.cast ⋯ (Fin.castAdd n (Fin.natAdd n 0))) +
    (∑ i, S (Fin.cast ⋯ (Fin.castAdd n (Fin.castAdd 1 i))) + ∑ i, S (Fin.cast ⋯ (Fin.natAdd (n + 1) i))) =
  S oddMid + ∑ x, (S (oddFst x) + S (oddSnd x))
  rw [Finset.sum_add_distribn:ℕS:Fin (2 * n + 1) → ℚh1:∑ i, S i = ∑ i, S (Fin.cast ⋯ i)⊢ S (Fin.cast ⋯ (Fin.castAdd n (Fin.natAdd n 0))) +
    (∑ i, S (Fin.cast ⋯ (Fin.castAdd n (Fin.castAdd 1 i))) + ∑ i, S (Fin.cast ⋯ (Fin.natAdd (n + 1) i))) =
  S oddMid + (∑ x, S (oddFst x) + ∑ x, S (oddSnd x))n:ℕS:Fin (2 * n + 1) → ℚh1:∑ i, S i = ∑ i, S (Fin.cast ⋯ i)⊢ S (Fin.cast ⋯ (Fin.castAdd n (Fin.natAdd n 0))) +
    (∑ i, S (Fin.cast ⋯ (Fin.castAdd n (Fin.castAdd 1 i))) + ∑ i, S (Fin.cast ⋯ (Fin.natAdd (n + 1) i))) =
  S oddMid + (∑ x, S (oddFst x) + ∑ x, S (oddSnd x))]n:ℕS:Fin (2 * n + 1) → ℚh1:∑ i, S i = ∑ i, S (Fin.cast ⋯ i)⊢ S (Fin.cast ⋯ (Fin.castAdd n (Fin.natAdd n 0))) +
    (∑ i, S (Fin.cast ⋯ (Fin.castAdd n (Fin.castAdd 1 i))) + ∑ i, S (Fin.cast ⋯ (Fin.natAdd (n + 1) i))) =
  S oddMid + (∑ x, S (oddFst x) + ∑ x, S (oddSnd x))
  rflAll goals completed! 🐙

A.2. The shifted split: Spltting the charges up via `1 + n + n`

The inclusion of Fin n into Fin (1 + n + n) via the first n. This is then casted to Fin (2 * n + 1).

def oddShiftFst (j : Fin n) : Fin (2 * n + 1) :=
  Fin.cast (odd_shift_eq n) (Fin.castAdd n (Fin.natAdd 1 j))

The inclusion of Fin n into Fin (1 + n + n) via the second n. This is then casted to Fin (2 * n + 1).

def oddShiftSnd (j : Fin n) : Fin (2 * n + 1) :=
  Fin.cast (odd_shift_eq n) (Fin.natAdd (1 + n) j)

The element representing the 1 in Fin (1 + n + n). This is then casted to Fin (2 * n + 1).

def oddShiftZero : Fin (2 * n + 1) :=
  Fin.cast (odd_shift_eq n) (Fin.castAdd n (Fin.castAdd n 1))



lemma sum_oddShift (S : Fin (2 * n + 1) → ℚ) :
    ∑ i, S i = S oddShiftZero + ∑ i : Fin n, ((S ∘ oddShiftFst) i + (S ∘ oddShiftSnd) i) := byn:ℕS:Fin (2 * n + 1) → ℚ⊢ ∑ i, S i = S oddShiftZero + ∑ i, ((S ∘ oddShiftFst) i + (S ∘ oddShiftSnd) i)
  have h1 : ∑ i, S i = ∑ i : Fin ((1+n)+n), S (Fin.cast (odd_shift_eq n) i) :=
    (Equiv.sum_comp (finCongr (odd_shift_eq n)) S).symmn:ℕS:Fin (2 * n + 1) → ℚh1:∑ i, S i = ∑ i, S (Fin.cast ⋯ i)⊢ ∑ i, S i = S oddShiftZero + ∑ i, ((S ∘ oddShiftFst) i + (S ∘ oddShiftSnd) i)
  rw [h1,n:ℕS:Fin (2 * n + 1) → ℚh1:∑ i, S i = ∑ i, S (Fin.cast ⋯ i)⊢ ∑ i, S (Fin.cast ⋯ i) = S oddShiftZero + ∑ i, ((S ∘ oddShiftFst) i + (S ∘ oddShiftSnd) i)n:ℕS:Fin (2 * n + 1) → ℚh1:∑ i, S i = ∑ i, S (Fin.cast ⋯ i)⊢ ∑ i, S (Fin.cast ⋯ (Fin.castAdd n (Fin.castAdd n i))) + ∑ i, S (Fin.cast ⋯ (Fin.castAdd n (Fin.natAdd 1 i))) +
    ∑ i, S (Fin.cast ⋯ (Fin.natAdd (1 + n) i)) =
  S oddShiftZero + ∑ i, ((S ∘ oddShiftFst) i + (S ∘ oddShiftSnd) i) Fin.sum_univ_add,n:ℕS:Fin (2 * n + 1) → ℚh1:∑ i, S i = ∑ i, S (Fin.cast ⋯ i)⊢ ∑ i, S (Fin.cast ⋯ (Fin.castAdd n i)) + ∑ i, S (Fin.cast ⋯ (Fin.natAdd (1 + n) i)) =
  S oddShiftZero + ∑ i, ((S ∘ oddShiftFst) i + (S ∘ oddShiftSnd) i)n:ℕS:Fin (2 * n + 1) → ℚh1:∑ i, S i = ∑ i, S (Fin.cast ⋯ i)⊢ ∑ i, S (Fin.cast ⋯ (Fin.castAdd n (Fin.castAdd n i))) + ∑ i, S (Fin.cast ⋯ (Fin.castAdd n (Fin.natAdd 1 i))) +
    ∑ i, S (Fin.cast ⋯ (Fin.natAdd (1 + n) i)) =
  S oddShiftZero + ∑ i, ((S ∘ oddShiftFst) i + (S ∘ oddShiftSnd) i) Fin.sum_univ_addn:ℕS:Fin (2 * n + 1) → ℚh1:∑ i, S i = ∑ i, S (Fin.cast ⋯ i)⊢ ∑ i, S (Fin.cast ⋯ (Fin.castAdd n (Fin.castAdd n i))) + ∑ i, S (Fin.cast ⋯ (Fin.castAdd n (Fin.natAdd 1 i))) +
    ∑ i, S (Fin.cast ⋯ (Fin.natAdd (1 + n) i)) =
  S oddShiftZero + ∑ i, ((S ∘ oddShiftFst) i + (S ∘ oddShiftSnd) i)n:ℕS:Fin (2 * n + 1) → ℚh1:∑ i, S i = ∑ i, S (Fin.cast ⋯ i)⊢ ∑ i, S (Fin.cast ⋯ (Fin.castAdd n (Fin.castAdd n i))) + ∑ i, S (Fin.cast ⋯ (Fin.castAdd n (Fin.natAdd 1 i))) +
    ∑ i, S (Fin.cast ⋯ (Fin.natAdd (1 + n) i)) =
  S oddShiftZero + ∑ i, ((S ∘ oddShiftFst) i + (S ∘ oddShiftSnd) i)]n:ℕS:Fin (2 * n + 1) → ℚh1:∑ i, S i = ∑ i, S (Fin.cast ⋯ i)⊢ ∑ i, S (Fin.cast ⋯ (Fin.castAdd n (Fin.castAdd n i))) + ∑ i, S (Fin.cast ⋯ (Fin.castAdd n (Fin.natAdd 1 i))) +
    ∑ i, S (Fin.cast ⋯ (Fin.natAdd (1 + n) i)) =
  S oddShiftZero + ∑ i, ((S ∘ oddShiftFst) i + (S ∘ oddShiftSnd) i)
  simp only [univ_unique, Fin.default_eq_zero, Fin.isValue, sum_singleton, Function.comp_apply]n:ℕS:Fin (2 * n + 1) → ℚh1:∑ i, S i = ∑ i, S (Fin.cast ⋯ i)⊢ S (Fin.cast ⋯ (Fin.castAdd n (Fin.castAdd n 0))) + ∑ i, S (Fin.cast ⋯ (Fin.castAdd n (Fin.natAdd 1 i))) +
    ∑ i, S (Fin.cast ⋯ (Fin.natAdd (1 + n) i)) =
  S oddShiftZero + ∑ x, (S (oddShiftFst x) + S (oddShiftSnd x))
  rw [add_assoc,n:ℕS:Fin (2 * n + 1) → ℚh1:∑ i, S i = ∑ i, S (Fin.cast ⋯ i)⊢ S (Fin.cast ⋯ (Fin.castAdd n (Fin.castAdd n 0))) +
    (∑ i, S (Fin.cast ⋯ (Fin.castAdd n (Fin.natAdd 1 i))) + ∑ i, S (Fin.cast ⋯ (Fin.natAdd (1 + n) i))) =
  S oddShiftZero + ∑ x, (S (oddShiftFst x) + S (oddShiftSnd x))n:ℕS:Fin (2 * n + 1) → ℚh1:∑ i, S i = ∑ i, S (Fin.cast ⋯ i)⊢ S (Fin.cast ⋯ (Fin.castAdd n (Fin.castAdd n 0))) +
    (∑ i, S (Fin.cast ⋯ (Fin.castAdd n (Fin.natAdd 1 i))) + ∑ i, S (Fin.cast ⋯ (Fin.natAdd (1 + n) i))) =
  S oddShiftZero + (∑ x, S (oddShiftFst x) + ∑ x, S (oddShiftSnd x)) Finset.sum_add_distribn:ℕS:Fin (2 * n + 1) → ℚh1:∑ i, S i = ∑ i, S (Fin.cast ⋯ i)⊢ S (Fin.cast ⋯ (Fin.castAdd n (Fin.castAdd n 0))) +
    (∑ i, S (Fin.cast ⋯ (Fin.castAdd n (Fin.natAdd 1 i))) + ∑ i, S (Fin.cast ⋯ (Fin.natAdd (1 + n) i))) =
  S oddShiftZero + (∑ x, S (oddShiftFst x) + ∑ x, S (oddShiftSnd x))n:ℕS:Fin (2 * n + 1) → ℚh1:∑ i, S i = ∑ i, S (Fin.cast ⋯ i)⊢ S (Fin.cast ⋯ (Fin.castAdd n (Fin.castAdd n 0))) +
    (∑ i, S (Fin.cast ⋯ (Fin.castAdd n (Fin.natAdd 1 i))) + ∑ i, S (Fin.cast ⋯ (Fin.natAdd (1 + n) i))) =
  S oddShiftZero + (∑ x, S (oddShiftFst x) + ∑ x, S (oddShiftSnd x))]n:ℕS:Fin (2 * n + 1) → ℚh1:∑ i, S i = ∑ i, S (Fin.cast ⋯ i)⊢ S (Fin.cast ⋯ (Fin.castAdd n (Fin.castAdd n 0))) +
    (∑ i, S (Fin.cast ⋯ (Fin.castAdd n (Fin.natAdd 1 i))) + ∑ i, S (Fin.cast ⋯ (Fin.natAdd (1 + n) i))) =
  S oddShiftZero + (∑ x, S (oddShiftFst x) + ∑ x, S (oddShiftSnd x))
  rflAll goals completed! 🐙

A.3. The shifted shifted split: Spltting the charges up via `((1+n)+1) + n.succ`

lemma odd_shift_shift_eq (n : ℕ) : ((1+n)+1) + n.succ = 2 * n.succ + 1 := byn:ℕ⊢ 1 + n + 1 + n.succ = 2 * n.succ + 1
  omegaAll goals completed! 🐙

The element representing the first 1 in Fin (1 + n + 1 + n.succ) casted to Fin (2 * n.succ + 1).

def oddShiftShiftZero : Fin (2 * n.succ + 1) :=
  Fin.cast (odd_shift_shift_eq n) (Fin.castAdd n.succ (Fin.castAdd 1 (Fin.castAdd n 1)))

The inclusion of Fin n into Fin (1 + n + 1 + n.succ) via the first n and casted to Fin (2 * n.succ + 1).

def oddShiftShiftFst (j : Fin n) : Fin (2 * n.succ + 1) :=
  Fin.cast (odd_shift_shift_eq n) (Fin.castAdd n.succ (Fin.castAdd 1 (Fin.natAdd 1 j)))

The element representing the second 1 in Fin (1 + n + 1 + n.succ) casted to 2 * n.succ + 1.

def oddShiftShiftMid : Fin (2 * n.succ + 1) :=
  Fin.cast (odd_shift_shift_eq n) (Fin.castAdd n.succ (Fin.natAdd (1+n) 1))

The inclusion of Fin n.succ into Fin (1 + n + 1 + n.succ) via the n.succ and casted to Fin (2 * n.succ + 1).

def oddShiftShiftSnd (j : Fin n.succ) : Fin (2 * n.succ + 1) :=
  Fin.cast (odd_shift_shift_eq n) (Fin.natAdd ((1+n)+1) j)

A.4. Relating the splittings together

              lemma oddShiftShiftZero_eq_oddFst_zero : @oddShiftShiftZero n = oddFst 0 :=
  Fin.rev_inj.mp rfllemma oddShiftShiftZero_eq_oddShiftZero : @oddShiftShiftZero n = oddShiftZero := rfllemma oddShiftShiftFst_eq_oddFst_succ (j : Fin n) :
    oddShiftShiftFst j = oddFst j.succ := byn:ℕj:Fin n⊢ oddShiftShiftFst j = oddFst j.succ
  simp only [Fin.ext_iff, succ_eq_add_one, oddShiftShiftFst, Fin.val_cast, Fin.val_castAdd,
    Fin.val_natAdd, oddFst, Fin.val_succ]n:ℕj:Fin n⊢ 1 + ↑j = ↑j + 1
  omegaAll goals completed! 🐙lemma oddShiftShiftFst_eq_oddShiftFst_castSucc (j : Fin n) :
    oddShiftShiftFst j = oddShiftFst j.castSucc := byn:ℕj:Fin n⊢ oddShiftShiftFst j = oddShiftFst j.castSucc
  rflAll goals completed! 🐙lemma oddShiftShiftMid_eq_oddMid : @oddShiftShiftMid n = oddMid := byn:ℕ⊢ oddShiftShiftMid = oddMid
  simp only [Fin.ext_iff, succ_eq_add_one, oddShiftShiftMid, Fin.isValue, Fin.val_cast,
    Fin.val_castAdd, Fin.val_natAdd, Fin.val_eq_zero, add_zero, oddMid]n:ℕ⊢ 1 + n = n + 1
  omegaAll goals completed! 🐙lemma oddShiftShiftMid_eq_oddShiftFst_last : oddShiftShiftMid = oddShiftFst (Fin.last n) := byn:ℕ⊢ oddShiftShiftMid = oddShiftFst (Fin.last n)
  rflAll goals completed! 🐙lemma oddShiftShiftSnd_eq_oddSnd (j : Fin n.succ) : oddShiftShiftSnd j = oddSnd j := byn:ℕj:Fin n.succ⊢ oddShiftShiftSnd j = oddSnd j
  simp only [Fin.ext_iff, succ_eq_add_one, oddShiftShiftSnd, Fin.val_cast, Fin.val_natAdd, oddSnd,
    add_left_inj]n:ℕj:Fin n.succ⊢ 1 + n = n + 1
  omegaAll goals completed! 🐙

lemma oddShiftShiftSnd_eq_oddShiftSnd (j : Fin n.succ) : oddShiftShiftSnd j = oddShiftSnd j := byn:ℕj:Fin n.succ⊢ oddShiftShiftSnd j = oddShiftSnd j
  rw [Fin.ext_iffn:ℕj:Fin n.succ⊢ ↑(oddShiftShiftSnd j) = ↑(oddShiftSnd j)n:ℕj:Fin n.succ⊢ ↑(oddShiftShiftSnd j) = ↑(oddShiftSnd j)]n:ℕj:Fin n.succ⊢ ↑(oddShiftShiftSnd j) = ↑(oddShiftSnd j)
  rflAll goals completed! 🐙lemma oddSnd_eq_oddShiftSnd (j : Fin n) : oddSnd j = oddShiftSnd j := byn:ℕj:Fin n⊢ oddSnd j = oddShiftSnd j
  simp only [Fin.ext_iff, oddSnd, Fin.val_cast, Fin.val_natAdd, oddShiftSnd, add_left_inj]n:ℕj:Fin n⊢ n + 1 = 1 + n
  omegaAll goals completed! 🐙lemma oddShiftZero_eq_oddFst : oddShiftZero = oddFst (0 : Fin n.succ) := byn:ℕ⊢ oddShiftZero = oddFst 0
  simp [Fin.ext_iff, oddShiftZero, oddFst]All goals completed! 🐙lemma oddShiftFst_castSucc_eq_oddFst_succ (j : Fin n) :
    oddShiftFst j.castSucc = oddFst j.succ := byn:ℕj:Fin n⊢ oddShiftFst j.castSucc = oddFst j.succ
  simp only [Fin.ext_iff, oddShiftFst, Fin.val_cast, Fin.val_castAdd, Fin.val_natAdd, oddFst,
    Fin.val_succ, Fin.val_castSucc]n:ℕj:Fin n⊢ 1 + ↑j = ↑j + 1
  omegaAll goals completed! 🐙lemma oddShiftFst_last_eq_oddMid : oddShiftFst (Fin.last n) = oddMid := byn:ℕ⊢ oddShiftFst (Fin.last n) = oddMid
  simp only [Fin.ext_iff, oddShiftFst, Fin.val_cast, Fin.val_castAdd, Fin.val_natAdd, oddMid,
    Fin.val_last]n:ℕ⊢ 1 + n = n + 1 + ↑1
  omegaAll goals completed! 🐙lemma oddShiftSnd_eq_oddSnd (j : Fin n) : oddShiftSnd j = oddSnd j := byn:ℕj:Fin n⊢ oddShiftSnd j = oddSnd j
  simp only [Fin.ext_iff, oddShiftSnd, Fin.val_cast, Fin.val_natAdd, oddSnd, add_left_inj]n:ℕj:Fin n⊢ 1 + n = n + 1
  omegaAll goals completed! 🐙

B. The unshifted plane

B.1. The basis vectors of the unshifted plane as charges

The unshifted part of the basis as charge assignments.

def basisAsCharges (j : Fin n) : (PureU1 (2 * n + 1)).Charges :=
  fun i =>
  if i = oddFst j then
    1
  else
    if i = oddSnd j then
      - 1
    else
      0

B.2. Components of the basis vectors as charges

              lemma basis_on_oddFst_self (j : Fin n) : basisAsCharges j (oddFst j) = 1 := byn:ℕj:Fin n⊢ basisAsCharges j (oddFst j) = 1
  simp [basisAsCharges]All goals completed! 🐙set_option backward.isDefEq.respectTransparency false in
lemma basis_on_oddFst_other {k j : Fin n} (h : k ≠ j) :
    basisAsCharges k (oddFst j) = 0 := byn:ℕk:Fin nj:Fin nh:k ≠ j⊢ basisAsCharges k (oddFst j) = 0
  have hk : (k : ℕ) ≠ (j : ℕ) := fun he => h (Fin.ext he)n:ℕk:Fin nj:Fin nh:k ≠ jhk:↑k ≠ ↑j⊢ basisAsCharges k (oddFst j) = 0
  simp only [basisAsCharges, oddFst, oddSnd, Fin.ext_iff, Fin.val_cast, Fin.val_castAdd,
    Fin.val_natAdd]n:ℕk:Fin nj:Fin nh:k ≠ jhk:↑k ≠ ↑j⊢ (if ↑j = ↑k then 1 else if ↑j = n + 1 + ↑k then -1 else 0) = 0
  splitisTruen:ℕk:Fin nj:Fin nh:k ≠ jhk:↑k ≠ ↑jh✝:↑j = ↑k⊢ 1 = 0isFalsen:ℕk:Fin nj:Fin nh:k ≠ jhk:↑k ≠ ↑jh✝:¬↑j = ↑k⊢ (if ↑j = n + 1 + ↑k then -1 else 0) = 0
  ·isTruen:ℕk:Fin nj:Fin nh:k ≠ jhk:↑k ≠ ↑jh✝:↑j = ↑k⊢ 1 = 0 omegaAll goals completed! 🐙
  ·isFalsen:ℕk:Fin nj:Fin nh:k ≠ jhk:↑k ≠ ↑jh✝:¬↑j = ↑k⊢ (if ↑j = n + 1 + ↑k then -1 else 0) = 0 splitisFalse.isTruen:ℕk:Fin nj:Fin nh:k ≠ jhk:↑k ≠ ↑jh✝¹:¬↑j = ↑kh✝:↑j = n + 1 + ↑k⊢ -1 = 0isFalse.isFalsen:ℕk:Fin nj:Fin nh:k ≠ jhk:↑k ≠ ↑jh✝¹:¬↑j = ↑kh✝:¬↑j = n + 1 + ↑k⊢ 0 = 0
    ·isFalse.isTruen:ℕk:Fin nj:Fin nh:k ≠ jhk:↑k ≠ ↑jh✝¹:¬↑j = ↑kh✝:↑j = n + 1 + ↑k⊢ -1 = 0 omegaAll goals completed! 🐙
    ·isFalse.isFalsen:ℕk:Fin nj:Fin nh:k ≠ jhk:↑k ≠ ↑jh✝¹:¬↑j = ↑kh✝:¬↑j = n + 1 + ↑k⊢ 0 = 0 rflAll goals completed! 🐙set_option backward.isDefEq.respectTransparency false in
lemma basis_on_other {k : Fin n} {j : Fin (2 * n + 1)} (h1 : j ≠ oddFst k) (h2 : j ≠ oddSnd k) :
    basisAsCharges k j = 0 := byn:ℕk:Fin nj:Fin (2 * n + 1)h1:j ≠ oddFst kh2:j ≠ oddSnd k⊢ basisAsCharges k j = 0
  simp only [basisAsCharges, h1, h2, ↓reduceIte]All goals completed! 🐙set_option backward.isDefEq.respectTransparency false in
lemma basis_oddSnd_eq_minus_oddFst (j i : Fin n) :
    basisAsCharges j (oddSnd i) = - basisAsCharges j (oddFst i) := byn:ℕj:Fin ni:Fin n⊢ basisAsCharges j (oddSnd i) = -basisAsCharges j (oddFst i)
  simp only [basisAsCharges, oddSnd, oddFst, Fin.ext_iff, Fin.val_cast, Fin.val_castAdd,
    Fin.val_natAdd]n:ℕj:Fin ni:Fin n⊢ (if n + 1 + ↑i = ↑j then 1 else if n + 1 + ↑i = n + 1 + ↑j then -1 else 0) =
  -if ↑i = ↑j then 1 else if ↑i = n + 1 + ↑j then -1 else 0
  split_ifsposn:ℕj:Fin ni:Fin nh✝¹:n + 1 + ↑i = ↑jh✝:↑i = ↑j⊢ 1 = -1posn:ℕj:Fin ni:Fin nh✝²:n + 1 + ↑i = ↑jh✝¹:¬↑i = ↑jh✝:↑i = n + 1 + ↑j⊢ 1 = - -1negn:ℕj:Fin ni:Fin nh✝²:n + 1 + ↑i = ↑jh✝¹:¬↑i = ↑jh✝:¬↑i = n + 1 + ↑j⊢ 1 = -0posn:ℕj:Fin ni:Fin nh✝²:¬n + 1 + ↑i = ↑jh✝¹:n + 1 + ↑i = n + 1 + ↑jh✝:↑i = ↑j⊢ -1 = -1posn:ℕj:Fin ni:Fin nh✝³:¬n + 1 + ↑i = ↑jh✝²:n + 1 + ↑i = n + 1 + ↑jh✝¹:¬↑i = ↑jh✝:↑i = n + 1 + ↑j⊢ -1 = - -1negn:ℕj:Fin ni:Fin nh✝³:¬n + 1 + ↑i = ↑jh✝²:n + 1 + ↑i = n + 1 + ↑jh✝¹:¬↑i = ↑jh✝:¬↑i = n + 1 + ↑j⊢ -1 = -0posn:ℕj:Fin ni:Fin nh✝²:¬n + 1 + ↑i = ↑jh✝¹:¬n + 1 + ↑i = n + 1 + ↑jh✝:↑i = ↑j⊢ 0 = -1posn:ℕj:Fin ni:Fin nh✝³:¬n + 1 + ↑i = ↑jh✝²:¬n + 1 + ↑i = n + 1 + ↑jh✝¹:¬↑i = ↑jh✝:↑i = n + 1 + ↑j⊢ 0 = - -1negn:ℕj:Fin ni:Fin nh✝³:¬n + 1 + ↑i = ↑jh✝²:¬n + 1 + ↑i = n + 1 + ↑jh✝¹:¬↑i = ↑jh✝:¬↑i = n + 1 + ↑j⊢ 0 = -0 <;>posn:ℕj:Fin ni:Fin nh✝¹:n + 1 + ↑i = ↑jh✝:↑i = ↑j⊢ 1 = -1posn:ℕj:Fin ni:Fin nh✝²:n + 1 + ↑i = ↑jh✝¹:¬↑i = ↑jh✝:↑i = n + 1 + ↑j⊢ 1 = - -1negn:ℕj:Fin ni:Fin nh✝²:n + 1 + ↑i = ↑jh✝¹:¬↑i = ↑jh✝:¬↑i = n + 1 + ↑j⊢ 1 = -0posn:ℕj:Fin ni:Fin nh✝²:¬n + 1 + ↑i = ↑jh✝¹:n + 1 + ↑i = n + 1 + ↑jh✝:↑i = ↑j⊢ -1 = -1posn:ℕj:Fin ni:Fin nh✝³:¬n + 1 + ↑i = ↑jh✝²:n + 1 + ↑i = n + 1 + ↑jh✝¹:¬↑i = ↑jh✝:↑i = n + 1 + ↑j⊢ -1 = - -1negn:ℕj:Fin ni:Fin nh✝³:¬n + 1 + ↑i = ↑jh✝²:n + 1 + ↑i = n + 1 + ↑jh✝¹:¬↑i = ↑jh✝:¬↑i = n + 1 + ↑j⊢ -1 = -0posn:ℕj:Fin ni:Fin nh✝²:¬n + 1 + ↑i = ↑jh✝¹:¬n + 1 + ↑i = n + 1 + ↑jh✝:↑i = ↑j⊢ 0 = -1posn:ℕj:Fin ni:Fin nh✝³:¬n + 1 + ↑i = ↑jh✝²:¬n + 1 + ↑i = n + 1 + ↑jh✝¹:¬↑i = ↑jh✝:↑i = n + 1 + ↑j⊢ 0 = - -1negn:ℕj:Fin ni:Fin nh✝³:¬n + 1 + ↑i = ↑jh✝²:¬n + 1 + ↑i = n + 1 + ↑jh✝¹:¬↑i = ↑jh✝:¬↑i = n + 1 + ↑j⊢ 0 = -0 first | omegaAll goals completed! 🐙 | simpAll goals completed! 🐙

lemma basis_on_oddSnd_self (j : Fin n) : basisAsCharges j (oddSnd j) = - 1 := byn:ℕj:Fin n⊢ basisAsCharges j (oddSnd j) = -1
  rw [basis_oddSnd_eq_minus_oddFst,n:ℕj:Fin n⊢ -basisAsCharges j (oddFst j) = -1All goals completed! 🐙 basis_on_oddFst_selfn:ℕj:Fin n⊢ -1 = -1All goals completed! 🐙]All goals completed! 🐙

lemma basis_on_oddSnd_other {k j : Fin n} (h : k ≠ j) : basisAsCharges k (oddSnd j) = 0 := byn:ℕk:Fin nj:Fin nh:k ≠ j⊢ basisAsCharges k (oddSnd j) = 0
  rw [basis_oddSnd_eq_minus_oddFst,n:ℕk:Fin nj:Fin nh:k ≠ j⊢ -basisAsCharges k (oddFst j) = 0n:ℕk:Fin nj:Fin nh:k ≠ j⊢ -0 = 0 basis_on_oddFst_other hn:ℕk:Fin nj:Fin nh:k ≠ j⊢ -0 = 0n:ℕk:Fin nj:Fin nh:k ≠ j⊢ -0 = 0]n:ℕk:Fin nj:Fin nh:k ≠ j⊢ -0 = 0
  rflAll goals completed! 🐙set_option backward.isDefEq.respectTransparency false in
lemma basis_on_oddMid (j : Fin n) : basisAsCharges j oddMid = 0 := byn:ℕj:Fin n⊢ basisAsCharges j oddMid = 0
  simp only [basisAsCharges, oddMid, oddFst, oddSnd, Fin.isValue, Fin.val_cast, Fin.val_castAdd,
    Fin.val_natAdd, Fin.val_eq_zero, add_zero, Fin.ext_iff]n:ℕj:Fin n⊢ (if n = ↑j then 1 else if n = n + 1 + ↑j then -1 else 0) = 0
  splitisTruen:ℕj:Fin nh✝:n = ↑j⊢ 1 = 0isFalsen:ℕj:Fin nh✝:¬n = ↑j⊢ (if n = n + 1 + ↑j then -1 else 0) = 0
  ·isTruen:ℕj:Fin nh✝:n = ↑j⊢ 1 = 0 omegaAll goals completed! 🐙
  ·isFalsen:ℕj:Fin nh✝:¬n = ↑j⊢ (if n = n + 1 + ↑j then -1 else 0) = 0 splitisFalse.isTruen:ℕj:Fin nh✝¹:¬n = ↑jh✝:n = n + 1 + ↑j⊢ -1 = 0isFalse.isFalsen:ℕj:Fin nh✝¹:¬n = ↑jh✝:¬n = n + 1 + ↑j⊢ 0 = 0
    ·isFalse.isTruen:ℕj:Fin nh✝¹:¬n = ↑jh✝:n = n + 1 + ↑j⊢ -1 = 0 omegaAll goals completed! 🐙
    ·isFalse.isFalsen:ℕj:Fin nh✝¹:¬n = ↑jh✝:¬n = n + 1 + ↑j⊢ 0 = 0 rflAll goals completed! 🐙

B.3. The basis vectors satisfy the linear ACCs



lemma basis_linearACC (j : Fin n) : (accGrav (2 * n + 1)) (basisAsCharges j) = 0 := byn:ℕj:Fin n⊢ (accGrav (2 * n + 1)) (basisAsCharges j) = 0
  rw [accGravn:ℕj:Fin n⊢ { toFun := fun S => ∑ i, S i, map_add' := ⋯, map_smul' := ⋯ } (basisAsCharges j) = 0n:ℕj:Fin n⊢ { toFun := fun S => ∑ i, S i, map_add' := ⋯, map_smul' := ⋯ } (basisAsCharges j) = 0]n:ℕj:Fin n⊢ { toFun := fun S => ∑ i, S i, map_add' := ⋯, map_smul' := ⋯ } (basisAsCharges j) = 0
  simp [sum_odd, basis_oddSnd_eq_minus_oddFst, basis_on_oddMid]All goals completed! 🐙

B.4. The basis vectors as `LinSols`

The unshifted part of the basis as LinSols.

@[simps!]
def basis (j : Fin n) : (PureU1 (2 * n + 1)).LinSols :=
  ⟨basisAsCharges j, byn:ℕj:Fin n⊢ ∀ (i : Fin (PureU1 (2 * n + 1)).numberLinear), ((PureU1 (2 * n + 1)).linearACCs i) (basisAsCharges j) = 0
    intro in:ℕj:Fin ni:Fin (PureU1 (2 * n + 1)).numberLinear⊢ ((PureU1 (2 * n + 1)).linearACCs i) (basisAsCharges j) = 0
    match i with
    | ⟨0, _⟩ =>n:ℕj:Fin ni:Fin (PureU1 (2 * n + 1)).numberLinearisLt✝:0 < (PureU1 (2 * n + 1)).numberLinear⊢ ((PureU1 (2 * n + 1)).linearACCs ⟨0, isLt✝⟩) (basisAsCharges j) = 0 exact basis_linearACC jAll goals completed! 🐙⟩

B.5. The inclusion of the unshifted plane into charges

A point in the span of the unshifted part of the basis as a charge.

def planeCharges (f : Fin n → ℚ) : (PureU1 (2 * n + 1)).Charges := ∑ i, f i • basisAsCharges i

B.6. Components of the unshifted plane

              

lemma planeCharges_oddFst (f : Fin n → ℚ) (j : Fin n) : planeCharges f (oddFst j) = f j := byn:ℕf:Fin n → ℚj:Fin n⊢ planeCharges f (oddFst j) = f j
  rw [planeCharges,n:ℕf:Fin n → ℚj:Fin n⊢ (∑ i, f i • basisAsCharges i) (oddFst j) = f jn:ℕf:Fin n → ℚj:Fin n⊢ ∑ i, (f i • basisAsCharges i) (oddFst j) = f j sum_of_chargesn:ℕf:Fin n → ℚj:Fin n⊢ ∑ i, (f i • basisAsCharges i) (oddFst j) = f jn:ℕf:Fin n → ℚj:Fin n⊢ ∑ i, (f i • basisAsCharges i) (oddFst j) = f j]n:ℕf:Fin n → ℚj:Fin n⊢ ∑ i, (f i • basisAsCharges i) (oddFst j) = f j
  simp only [HSMul.hSMul, SMul.smul]n:ℕf:Fin n → ℚj:Fin n⊢ ∑ x, f x * basisAsCharges x (oddFst j) = f j
  rw [Fintype.sum_eq_single jn:ℕf:Fin n → ℚj:Fin n⊢ f j * basisAsCharges j (oddFst j) = f jn:ℕf:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n), x ≠ j → f x * basisAsCharges x (oddFst j) = 0n:ℕf:Fin n → ℚj:Fin n⊢ f j * basisAsCharges j (oddFst j) = f jn:ℕf:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n), x ≠ j → f x * basisAsCharges x (oddFst j) = 0]n:ℕf:Fin n → ℚj:Fin n⊢ f j * basisAsCharges j (oddFst j) = f jn:ℕf:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n), x ≠ j → f x * basisAsCharges x (oddFst j) = 0
  ·n:ℕf:Fin n → ℚj:Fin n⊢ f j * basisAsCharges j (oddFst j) = f j simp [basis_on_oddFst_self]All goals completed! 🐙
  ·n:ℕf:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n), x ≠ j → f x * basisAsCharges x (oddFst j) = 0 intro k hkjn:ℕf:Fin n → ℚj:Fin nk:Fin nhkj:k ≠ j⊢ f k * basisAsCharges k (oddFst j) = 0
    exact mul_eq_zero_of_right (f k) (basis_on_oddFst_other hkj)All goals completed! 🐙

lemma planeCharges_oddSnd (f : Fin n → ℚ) (j : Fin n) : planeCharges f (oddSnd j) = - f j := byn:ℕf:Fin n → ℚj:Fin n⊢ planeCharges f (oddSnd j) = -f j
  rw [planeCharges,n:ℕf:Fin n → ℚj:Fin n⊢ (∑ i, f i • basisAsCharges i) (oddSnd j) = -f jn:ℕf:Fin n → ℚj:Fin n⊢ ∑ i, (f i • basisAsCharges i) (oddSnd j) = -f j sum_of_chargesn:ℕf:Fin n → ℚj:Fin n⊢ ∑ i, (f i • basisAsCharges i) (oddSnd j) = -f jn:ℕf:Fin n → ℚj:Fin n⊢ ∑ i, (f i • basisAsCharges i) (oddSnd j) = -f j]n:ℕf:Fin n → ℚj:Fin n⊢ ∑ i, (f i • basisAsCharges i) (oddSnd j) = -f j
  simp only [HSMul.hSMul, SMul.smul]n:ℕf:Fin n → ℚj:Fin n⊢ ∑ x, f x * basisAsCharges x (oddSnd j) = -f j
  rw [Fintype.sum_eq_single jn:ℕf:Fin n → ℚj:Fin n⊢ f j * basisAsCharges j (oddSnd j) = -f jn:ℕf:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n), x ≠ j → f x * basisAsCharges x (oddSnd j) = 0n:ℕf:Fin n → ℚj:Fin n⊢ f j * basisAsCharges j (oddSnd j) = -f jn:ℕf:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n), x ≠ j → f x * basisAsCharges x (oddSnd j) = 0]n:ℕf:Fin n → ℚj:Fin n⊢ f j * basisAsCharges j (oddSnd j) = -f jn:ℕf:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n), x ≠ j → f x * basisAsCharges x (oddSnd j) = 0
  ·n:ℕf:Fin n → ℚj:Fin n⊢ f j * basisAsCharges j (oddSnd j) = -f j simp [basis_on_oddSnd_self]All goals completed! 🐙
  ·n:ℕf:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n), x ≠ j → f x * basisAsCharges x (oddSnd j) = 0 intro k hkjn:ℕf:Fin n → ℚj:Fin nk:Fin nhkj:k ≠ j⊢ f k * basisAsCharges k (oddSnd j) = 0
    exact mul_eq_zero_of_right (f k) (basis_on_oddSnd_other hkj)All goals completed! 🐙

lemma planeCharges_oddMid (f : Fin n → ℚ) : planeCharges f oddMid = 0 := byn:ℕf:Fin n → ℚ⊢ planeCharges f oddMid = 0
  rw [planeCharges,n:ℕf:Fin n → ℚ⊢ (∑ i, f i • basisAsCharges i) oddMid = 0n:ℕf:Fin n → ℚ⊢ ∑ i, (f i • basisAsCharges i) oddMid = 0 sum_of_chargesn:ℕf:Fin n → ℚ⊢ ∑ i, (f i • basisAsCharges i) oddMid = 0n:ℕf:Fin n → ℚ⊢ ∑ i, (f i • basisAsCharges i) oddMid = 0]n:ℕf:Fin n → ℚ⊢ ∑ i, (f i • basisAsCharges i) oddMid = 0
  simp [HSMul.hSMul, SMul.smul, basis_on_oddMid]All goals completed! 🐙

B.7. Points on the unshifted plane satisfies the ACCs



lemma planeCharges_linearACC (f : Fin n → ℚ) : (accGrav (2 * n + 1)) (planeCharges f) = 0 := byn:ℕf:Fin n → ℚ⊢ (accGrav (2 * n + 1)) (planeCharges f) = 0
  rw [accGravn:ℕf:Fin n → ℚ⊢ { toFun := fun S => ∑ i, S i, map_add' := ⋯, map_smul' := ⋯ } (planeCharges f) = 0n:ℕf:Fin n → ℚ⊢ { toFun := fun S => ∑ i, S i, map_add' := ⋯, map_smul' := ⋯ } (planeCharges f) = 0]n:ℕf:Fin n → ℚ⊢ { toFun := fun S => ∑ i, S i, map_add' := ⋯, map_smul' := ⋯ } (planeCharges f) = 0
  simp [sum_odd, planeCharges_oddSnd, planeCharges_oddFst, planeCharges_oddMid]All goals completed! 🐙



lemma planeCharges_accCube (f : Fin n → ℚ) : accCube (2 * n +1) (planeCharges f) = 0 := byn:ℕf:Fin n → ℚ⊢ (accCube (2 * n + 1)) (planeCharges f) = 0
  rw [accCube_explicit,n:ℕf:Fin n → ℚ⊢ ∑ i, planeCharges f i ^ 3 = 0n:ℕf:Fin n → ℚ⊢ 0 ^ 3 + ∑ i, (((fun i => planeCharges f i ^ 3) ∘ oddFst) i + ((fun i => planeCharges f i ^ 3) ∘ oddSnd) i) = 0 sum_odd,n:ℕf:Fin n → ℚ⊢ planeCharges f oddMid ^ 3 +
    ∑ i, (((fun i => planeCharges f i ^ 3) ∘ oddFst) i + ((fun i => planeCharges f i ^ 3) ∘ oddSnd) i) =
  0n:ℕf:Fin n → ℚ⊢ 0 ^ 3 + ∑ i, (((fun i => planeCharges f i ^ 3) ∘ oddFst) i + ((fun i => planeCharges f i ^ 3) ∘ oddSnd) i) = 0 planeCharges_oddMidn:ℕf:Fin n → ℚ⊢ 0 ^ 3 + ∑ i, (((fun i => planeCharges f i ^ 3) ∘ oddFst) i + ((fun i => planeCharges f i ^ 3) ∘ oddSnd) i) = 0n:ℕf:Fin n → ℚ⊢ 0 ^ 3 + ∑ i, (((fun i => planeCharges f i ^ 3) ∘ oddFst) i + ((fun i => planeCharges f i ^ 3) ∘ oddSnd) i) = 0]n:ℕf:Fin n → ℚ⊢ 0 ^ 3 + ∑ i, (((fun i => planeCharges f i ^ 3) ∘ oddFst) i + ((fun i => planeCharges f i ^ 3) ∘ oddSnd) i) = 0
  simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, Function.comp_apply, zero_add]n:ℕf:Fin n → ℚ⊢ ∑ x, (planeCharges f (oddFst x) ^ 3 + planeCharges f (oddSnd x) ^ 3) = 0
  refine Finset.sum_eq_zero fun i _ => ?_n:ℕf:Fin n → ℚi:Fin nx✝:i ∈ univ⊢ planeCharges f (oddFst i) ^ 3 + planeCharges f (oddSnd i) ^ 3 = 0
  simp only [planeCharges_oddFst, planeCharges_oddSnd]n:ℕf:Fin n → ℚi:Fin nx✝:i ∈ univ⊢ f i ^ 3 + (-f i) ^ 3 = 0
  ringAll goals completed! 🐙

B.8. Kernel of the inclusion into charges

lemma planeCharges_zero (f : Fin n → ℚ) (h : planeCharges f = 0) : ∀ i, f i = 0 :=
  fun i => (planeCharges_oddFst f i).symm.trans (congr_fun h (oddFst i))

A point in the span of the unshifted part of the basis.

def planeLinSols (f : Fin n → ℚ) : (PureU1 (2 * n + 1)).LinSols := ∑ i, f i • basis i



lemma planeLinSols_val (f : Fin n → ℚ) : (planeLinSols f).val = planeCharges f := byn:ℕf:Fin n → ℚ⊢ (planeLinSols f).val = planeCharges f
  simp only [planeLinSols, planeCharges]n:ℕf:Fin n → ℚ⊢ (∑ i, f i • basis i).val = ∑ i, f i • basisAsCharges i
  funext in:ℕf:Fin n → ℚi:Fin (PureU1 (2 * n + 1)).numberCharges⊢ (∑ i, f i • basis i).val i = (∑ i, f i • basisAsCharges i) i
  rw [sum_of_anomaly_free_linear,n:ℕf:Fin n → ℚi:Fin (PureU1 (2 * n + 1)).numberCharges⊢ ∑ i_1, (f i_1 • basis i_1).val i = (∑ i, f i • basisAsCharges i) in:ℕf:Fin n → ℚi:Fin (PureU1 (2 * n + 1)).numberCharges⊢ ∑ i_1, (f i_1 • basis i_1).val i = ∑ i_1, (f i_1 • basisAsCharges i_1) i sum_of_chargesn:ℕf:Fin n → ℚi:Fin (PureU1 (2 * n + 1)).numberCharges⊢ ∑ i_1, (f i_1 • basis i_1).val i = ∑ i_1, (f i_1 • basisAsCharges i_1) in:ℕf:Fin n → ℚi:Fin (PureU1 (2 * n + 1)).numberCharges⊢ ∑ i_1, (f i_1 • basis i_1).val i = ∑ i_1, (f i_1 • basisAsCharges i_1) i]n:ℕf:Fin n → ℚi:Fin (PureU1 (2 * n + 1)).numberCharges⊢ ∑ i_1, (f i_1 • basis i_1).val i = ∑ i_1, (f i_1 • basisAsCharges i_1) i
  rflAll goals completed! 🐙

B.9. The basis vectors are linearly independent

theorem basis_linear_independent : LinearIndependent ℚ (@basis n) := byn:ℕ⊢ LinearIndependent ℚ basis
  apply Fintype.linearIndependent_iff.mprn:ℕ⊢ ∀ (g : Fin n → ℚ), ∑ i, g i • basis i = 0 → ∀ (i : Fin n), g i = 0
  intro f hn:ℕf:Fin n → ℚh:∑ i, f i • basis i = 0⊢ ∀ (i : Fin n), f i = 0
  change planeLinSols f = 0 at hn:ℕf:Fin n → ℚh:planeLinSols f = 0⊢ ∀ (i : Fin n), f i = 0
  exact planeCharges_zero f (planeLinSols_val f ▸ congrArg ACCSystemLinear.LinSols.val h)All goals completed! 🐙

C. The shifted plane

C.1. The basis vectors of the shifted plane as charges

The shifted part of the basis as charge assignments.

def basisAsCharges (j : Fin n) : (PureU1 (2 * n + 1)).Charges :=
  fun i =>
  if i = oddShiftFst j then
    1
  else
    if i = oddShiftSnd j then
      - 1
    else
      0

C.2. Components of the basis vectors as charges

              lemma basis_on_oddShiftFst_self (j : Fin n) : basisAsCharges j (oddShiftFst j) = 1 := byn:ℕj:Fin n⊢ basisAsCharges j (oddShiftFst j) = 1
  simp [basisAsCharges]All goals completed! 🐙set_option backward.isDefEq.respectTransparency false in
lemma basis_on_oddShiftFst_other {k j : Fin n} (h : k ≠ j) :
    basisAsCharges k (oddShiftFst j) = 0 := byn:ℕk:Fin nj:Fin nh:k ≠ j⊢ basisAsCharges k (oddShiftFst j) = 0
  have hk : (k : ℕ) ≠ (j : ℕ) := fun he => h (Fin.ext he)n:ℕk:Fin nj:Fin nh:k ≠ jhk:↑k ≠ ↑j⊢ basisAsCharges k (oddShiftFst j) = 0
  simp only [basisAsCharges, oddShiftFst, oddShiftSnd, Fin.ext_iff, Fin.val_cast, Fin.val_castAdd,
    Fin.val_natAdd]n:ℕk:Fin nj:Fin nh:k ≠ jhk:↑k ≠ ↑j⊢ (if 1 + ↑j = 1 + ↑k then 1 else if 1 + ↑j = 1 + n + ↑k then -1 else 0) = 0
  splitisTruen:ℕk:Fin nj:Fin nh:k ≠ jhk:↑k ≠ ↑jh✝:1 + ↑j = 1 + ↑k⊢ 1 = 0isFalsen:ℕk:Fin nj:Fin nh:k ≠ jhk:↑k ≠ ↑jh✝:¬1 + ↑j = 1 + ↑k⊢ (if 1 + ↑j = 1 + n + ↑k then -1 else 0) = 0
  ·isTruen:ℕk:Fin nj:Fin nh:k ≠ jhk:↑k ≠ ↑jh✝:1 + ↑j = 1 + ↑k⊢ 1 = 0 omegaAll goals completed! 🐙
  ·isFalsen:ℕk:Fin nj:Fin nh:k ≠ jhk:↑k ≠ ↑jh✝:¬1 + ↑j = 1 + ↑k⊢ (if 1 + ↑j = 1 + n + ↑k then -1 else 0) = 0 splitisFalse.isTruen:ℕk:Fin nj:Fin nh:k ≠ jhk:↑k ≠ ↑jh✝¹:¬1 + ↑j = 1 + ↑kh✝:1 + ↑j = 1 + n + ↑k⊢ -1 = 0isFalse.isFalsen:ℕk:Fin nj:Fin nh:k ≠ jhk:↑k ≠ ↑jh✝¹:¬1 + ↑j = 1 + ↑kh✝:¬1 + ↑j = 1 + n + ↑k⊢ 0 = 0
    ·isFalse.isTruen:ℕk:Fin nj:Fin nh:k ≠ jhk:↑k ≠ ↑jh✝¹:¬1 + ↑j = 1 + ↑kh✝:1 + ↑j = 1 + n + ↑k⊢ -1 = 0 omegaAll goals completed! 🐙
    ·isFalse.isFalsen:ℕk:Fin nj:Fin nh:k ≠ jhk:↑k ≠ ↑jh✝¹:¬1 + ↑j = 1 + ↑kh✝:¬1 + ↑j = 1 + n + ↑k⊢ 0 = 0 rflAll goals completed! 🐙set_option backward.isDefEq.respectTransparency false in
lemma basis_on_other {k : Fin n} {j : Fin (2 * n + 1)}
    (h1 : j ≠ oddShiftFst k) (h2 : j ≠ oddShiftSnd k) :
    basisAsCharges k j = 0 := byn:ℕk:Fin nj:Fin (2 * n + 1)h1:j ≠ oddShiftFst kh2:j ≠ oddShiftSnd k⊢ basisAsCharges k j = 0
  simp only [basisAsCharges, h1, h2, ↓reduceIte]All goals completed! 🐙set_option backward.isDefEq.respectTransparency false in
lemma basis_oddShiftSnd_eq_minus_oddShiftFst (j i : Fin n) :
    basisAsCharges j (oddShiftSnd i) = - basisAsCharges j (oddShiftFst i) := byn:ℕj:Fin ni:Fin n⊢ basisAsCharges j (oddShiftSnd i) = -basisAsCharges j (oddShiftFst i)
  simp only [basisAsCharges, oddShiftSnd, oddShiftFst, Fin.ext_iff, Fin.val_cast, Fin.val_castAdd,
    Fin.val_natAdd]n:ℕj:Fin ni:Fin n⊢ (if 1 + n + ↑i = 1 + ↑j then 1 else if 1 + n + ↑i = 1 + n + ↑j then -1 else 0) =
  -if 1 + ↑i = 1 + ↑j then 1 else if 1 + ↑i = 1 + n + ↑j then -1 else 0
  split_ifsposn:ℕj:Fin ni:Fin nh✝¹:1 + n + ↑i = 1 + ↑jh✝:1 + ↑i = 1 + ↑j⊢ 1 = -1posn:ℕj:Fin ni:Fin nh✝²:1 + n + ↑i = 1 + ↑jh✝¹:¬1 + ↑i = 1 + ↑jh✝:1 + ↑i = 1 + n + ↑j⊢ 1 = - -1negn:ℕj:Fin ni:Fin nh✝²:1 + n + ↑i = 1 + ↑jh✝¹:¬1 + ↑i = 1 + ↑jh✝:¬1 + ↑i = 1 + n + ↑j⊢ 1 = -0posn:ℕj:Fin ni:Fin nh✝²:¬1 + n + ↑i = 1 + ↑jh✝¹:1 + n + ↑i = 1 + n + ↑jh✝:1 + ↑i = 1 + ↑j⊢ -1 = -1posn:ℕj:Fin ni:Fin nh✝³:¬1 + n + ↑i = 1 + ↑jh✝²:1 + n + ↑i = 1 + n + ↑jh✝¹:¬1 + ↑i = 1 + ↑jh✝:1 + ↑i = 1 + n + ↑j⊢ -1 = - -1negn:ℕj:Fin ni:Fin nh✝³:¬1 + n + ↑i = 1 + ↑jh✝²:1 + n + ↑i = 1 + n + ↑jh✝¹:¬1 + ↑i = 1 + ↑jh✝:¬1 + ↑i = 1 + n + ↑j⊢ -1 = -0posn:ℕj:Fin ni:Fin nh✝²:¬1 + n + ↑i = 1 + ↑jh✝¹:¬1 + n + ↑i = 1 + n + ↑jh✝:1 + ↑i = 1 + ↑j⊢ 0 = -1posn:ℕj:Fin ni:Fin nh✝³:¬1 + n + ↑i = 1 + ↑jh✝²:¬1 + n + ↑i = 1 + n + ↑jh✝¹:¬1 + ↑i = 1 + ↑jh✝:1 + ↑i = 1 + n + ↑j⊢ 0 = - -1negn:ℕj:Fin ni:Fin nh✝³:¬1 + n + ↑i = 1 + ↑jh✝²:¬1 + n + ↑i = 1 + n + ↑jh✝¹:¬1 + ↑i = 1 + ↑jh✝:¬1 + ↑i = 1 + n + ↑j⊢ 0 = -0 <;>posn:ℕj:Fin ni:Fin nh✝¹:1 + n + ↑i = 1 + ↑jh✝:1 + ↑i = 1 + ↑j⊢ 1 = -1posn:ℕj:Fin ni:Fin nh✝²:1 + n + ↑i = 1 + ↑jh✝¹:¬1 + ↑i = 1 + ↑jh✝:1 + ↑i = 1 + n + ↑j⊢ 1 = - -1negn:ℕj:Fin ni:Fin nh✝²:1 + n + ↑i = 1 + ↑jh✝¹:¬1 + ↑i = 1 + ↑jh✝:¬1 + ↑i = 1 + n + ↑j⊢ 1 = -0posn:ℕj:Fin ni:Fin nh✝²:¬1 + n + ↑i = 1 + ↑jh✝¹:1 + n + ↑i = 1 + n + ↑jh✝:1 + ↑i = 1 + ↑j⊢ -1 = -1posn:ℕj:Fin ni:Fin nh✝³:¬1 + n + ↑i = 1 + ↑jh✝²:1 + n + ↑i = 1 + n + ↑jh✝¹:¬1 + ↑i = 1 + ↑jh✝:1 + ↑i = 1 + n + ↑j⊢ -1 = - -1negn:ℕj:Fin ni:Fin nh✝³:¬1 + n + ↑i = 1 + ↑jh✝²:1 + n + ↑i = 1 + n + ↑jh✝¹:¬1 + ↑i = 1 + ↑jh✝:¬1 + ↑i = 1 + n + ↑j⊢ -1 = -0posn:ℕj:Fin ni:Fin nh✝²:¬1 + n + ↑i = 1 + ↑jh✝¹:¬1 + n + ↑i = 1 + n + ↑jh✝:1 + ↑i = 1 + ↑j⊢ 0 = -1posn:ℕj:Fin ni:Fin nh✝³:¬1 + n + ↑i = 1 + ↑jh✝²:¬1 + n + ↑i = 1 + n + ↑jh✝¹:¬1 + ↑i = 1 + ↑jh✝:1 + ↑i = 1 + n + ↑j⊢ 0 = - -1negn:ℕj:Fin ni:Fin nh✝³:¬1 + n + ↑i = 1 + ↑jh✝²:¬1 + n + ↑i = 1 + n + ↑jh✝¹:¬1 + ↑i = 1 + ↑jh✝:¬1 + ↑i = 1 + n + ↑j⊢ 0 = -0 first | omegaAll goals completed! 🐙 | simpAll goals completed! 🐙

lemma basis_on_oddShiftSnd_self (j : Fin n) : basisAsCharges j (oddShiftSnd j) = - 1 := byn:ℕj:Fin n⊢ basisAsCharges j (oddShiftSnd j) = -1
  rw [basis_oddShiftSnd_eq_minus_oddShiftFst,n:ℕj:Fin n⊢ -basisAsCharges j (oddShiftFst j) = -1All goals completed! 🐙 basis_on_oddShiftFst_selfn:ℕj:Fin n⊢ -1 = -1All goals completed! 🐙]All goals completed! 🐙

lemma basis_on_oddShiftSnd_other {k j : Fin n} (h : k ≠ j) :
    basisAsCharges k (oddShiftSnd j) = 0 := byn:ℕk:Fin nj:Fin nh:k ≠ j⊢ basisAsCharges k (oddShiftSnd j) = 0
  rw [basis_oddShiftSnd_eq_minus_oddShiftFst,n:ℕk:Fin nj:Fin nh:k ≠ j⊢ -basisAsCharges k (oddShiftFst j) = 0n:ℕk:Fin nj:Fin nh:k ≠ j⊢ -0 = 0 basis_on_oddShiftFst_other hn:ℕk:Fin nj:Fin nh:k ≠ j⊢ -0 = 0n:ℕk:Fin nj:Fin nh:k ≠ j⊢ -0 = 0]n:ℕk:Fin nj:Fin nh:k ≠ j⊢ -0 = 0
  rflAll goals completed! 🐙set_option backward.isDefEq.respectTransparency false in
lemma basis_on_oddShiftZero (j : Fin n) : basisAsCharges j oddShiftZero = 0 := byn:ℕj:Fin n⊢ basisAsCharges j oddShiftZero = 0
  simp only [basisAsCharges, oddShiftZero, oddShiftFst, oddShiftSnd, Fin.isValue, Fin.val_cast,
    Fin.val_castAdd, Fin.val_eq_zero, Fin.val_natAdd, Fin.ext_iff]n:ℕj:Fin n⊢ (if 0 = 1 + ↑j then 1 else if 0 = 1 + n + ↑j then -1 else 0) = 0
  splitisTruen:ℕj:Fin nh✝:0 = 1 + ↑j⊢ 1 = 0isFalsen:ℕj:Fin nh✝:¬0 = 1 + ↑j⊢ (if 0 = 1 + n + ↑j then -1 else 0) = 0
  ·isTruen:ℕj:Fin nh✝:0 = 1 + ↑j⊢ 1 = 0 omegaAll goals completed! 🐙
  ·isFalsen:ℕj:Fin nh✝:¬0 = 1 + ↑j⊢ (if 0 = 1 + n + ↑j then -1 else 0) = 0 splitisFalse.isTruen:ℕj:Fin nh✝¹:¬0 = 1 + ↑jh✝:0 = 1 + n + ↑j⊢ -1 = 0isFalse.isFalsen:ℕj:Fin nh✝¹:¬0 = 1 + ↑jh✝:¬0 = 1 + n + ↑j⊢ 0 = 0
    ·isFalse.isTruen:ℕj:Fin nh✝¹:¬0 = 1 + ↑jh✝:0 = 1 + n + ↑j⊢ -1 = 0 omegaAll goals completed! 🐙
    ·isFalse.isFalsen:ℕj:Fin nh✝¹:¬0 = 1 + ↑jh✝:¬0 = 1 + n + ↑j⊢ 0 = 0 rflAll goals completed! 🐙

C.3. The basis vectors satisfy the linear ACCs



lemma basis_linearACC (j : Fin n) : (accGrav (2 * n + 1)) (basisAsCharges j) = 0 := byn:ℕj:Fin n⊢ (accGrav (2 * n + 1)) (basisAsCharges j) = 0
  rw [accGravn:ℕj:Fin n⊢ { toFun := fun S => ∑ i, S i, map_add' := ⋯, map_smul' := ⋯ } (basisAsCharges j) = 0n:ℕj:Fin n⊢ { toFun := fun S => ∑ i, S i, map_add' := ⋯, map_smul' := ⋯ } (basisAsCharges j) = 0]n:ℕj:Fin n⊢ { toFun := fun S => ∑ i, S i, map_add' := ⋯, map_smul' := ⋯ } (basisAsCharges j) = 0
  simp [sum_oddShift, basis_on_oddShiftZero, basis_oddShiftSnd_eq_minus_oddShiftFst]All goals completed! 🐙

C.4. The basis vectors as `LinSols`

The shifted part of the basis as LinSols.

@[simps!]
def basis (j : Fin n) : (PureU1 (2 * n + 1)).LinSols :=
  ⟨basisAsCharges j, byn:ℕj:Fin n⊢ ∀ (i : Fin (PureU1 (2 * n + 1)).numberLinear), ((PureU1 (2 * n + 1)).linearACCs i) (basisAsCharges j) = 0
    intro in:ℕj:Fin ni:Fin (PureU1 (2 * n + 1)).numberLinear⊢ ((PureU1 (2 * n + 1)).linearACCs i) (basisAsCharges j) = 0
    match i with
    | ⟨0, _⟩ =>n:ℕj:Fin ni:Fin (PureU1 (2 * n + 1)).numberLinearisLt✝:0 < (PureU1 (2 * n + 1)).numberLinear⊢ ((PureU1 (2 * n + 1)).linearACCs ⟨0, isLt✝⟩) (basisAsCharges j) = 0 exact basis_linearACC jAll goals completed! 🐙⟩

C.5. Permutations equal adding basis vectors

Swapping the elements oddShiftFst j and oddShiftSnd j is equivalent to adding a vector basisAsCharges j.


lemma swap_as_add {S S' : (PureU1 (2 * n + 1)).LinSols} (j : Fin n)
    (hS : ((FamilyPermutations (2 * n + 1)).linSolRep
    (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S') :
    S'.val = S.val + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basisAsCharges j := byn:ℕS:(PureU1 (2 * n + 1)).LinSolsS':(PureU1 (2 * n + 1)).LinSolsj:Fin nhS:((FamilyPermutations (2 * n + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'⊢ S'.val = S.val + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basisAsCharges j
  funext in:ℕS:(PureU1 (2 * n + 1)).LinSolsS':(PureU1 (2 * n + 1)).LinSolsj:Fin nhS:((FamilyPermutations (2 * n + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'i:Fin (PureU1 (2 * n + 1)).numberCharges⊢ S'.val i = (S.val + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basisAsCharges j) i
  rw [← hS,n:ℕS:(PureU1 (2 * n + 1)).LinSolsS':(PureU1 (2 * n + 1)).LinSolsj:Fin nhS:((FamilyPermutations (2 * n + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'i:Fin (PureU1 (2 * n + 1)).numberCharges⊢ (((FamilyPermutations (2 * n + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S).val i =
  (S.val + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basisAsCharges j) in:ℕS:(PureU1 (2 * n + 1)).LinSolsS':(PureU1 (2 * n + 1)).LinSolsj:Fin nhS:((FamilyPermutations (2 * n + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'i:Fin (PureU1 (2 * n + 1)).numberCharges⊢ S.val ((Equiv.swap (oddShiftFst j) (oddShiftSnd j)).invFun i) =
  (S.val + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basisAsCharges j) i FamilyPermutations_anomalyFreeLinear_applyn:ℕS:(PureU1 (2 * n + 1)).LinSolsS':(PureU1 (2 * n + 1)).LinSolsj:Fin nhS:((FamilyPermutations (2 * n + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'i:Fin (PureU1 (2 * n + 1)).numberCharges⊢ S.val ((Equiv.swap (oddShiftFst j) (oddShiftSnd j)).invFun i) =
  (S.val + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basisAsCharges j) in:ℕS:(PureU1 (2 * n + 1)).LinSolsS':(PureU1 (2 * n + 1)).LinSolsj:Fin nhS:((FamilyPermutations (2 * n + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'i:Fin (PureU1 (2 * n + 1)).numberCharges⊢ S.val ((Equiv.swap (oddShiftFst j) (oddShiftSnd j)).invFun i) =
  (S.val + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basisAsCharges j) i]n:ℕS:(PureU1 (2 * n + 1)).LinSolsS':(PureU1 (2 * n + 1)).LinSolsj:Fin nhS:((FamilyPermutations (2 * n + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'i:Fin (PureU1 (2 * n + 1)).numberCharges⊢ S.val ((Equiv.swap (oddShiftFst j) (oddShiftSnd j)).invFun i) =
  (S.val + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basisAsCharges j) i
  by_cases hi : i = oddShiftFst jposn:ℕS:(PureU1 (2 * n + 1)).LinSolsS':(PureU1 (2 * n + 1)).LinSolsj:Fin nhS:((FamilyPermutations (2 * n + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'i:Fin (PureU1 (2 * n + 1)).numberChargeshi:i = oddShiftFst j⊢ S.val ((Equiv.swap (oddShiftFst j) (oddShiftSnd j)).invFun i) =
  (S.val + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basisAsCharges j) inegn:ℕS:(PureU1 (2 * n + 1)).LinSolsS':(PureU1 (2 * n + 1)).LinSolsj:Fin nhS:((FamilyPermutations (2 * n + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'i:Fin (PureU1 (2 * n + 1)).numberChargeshi:¬i = oddShiftFst j⊢ S.val ((Equiv.swap (oddShiftFst j) (oddShiftSnd j)).invFun i) =
  (S.val + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basisAsCharges j) i
  ·posn:ℕS:(PureU1 (2 * n + 1)).LinSolsS':(PureU1 (2 * n + 1)).LinSolsj:Fin nhS:((FamilyPermutations (2 * n + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'i:Fin (PureU1 (2 * n + 1)).numberChargeshi:i = oddShiftFst j⊢ S.val ((Equiv.swap (oddShiftFst j) (oddShiftSnd j)).invFun i) =
  (S.val + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basisAsCharges j) i subst hiposn:ℕS:(PureU1 (2 * n + 1)).LinSolsS':(PureU1 (2 * n + 1)).LinSolsj:Fin nhS:((FamilyPermutations (2 * n + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'⊢ S.val ((Equiv.swap (oddShiftFst j) (oddShiftSnd j)).invFun (oddShiftFst j)) =
  (S.val + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basisAsCharges j) (oddShiftFst j)
    simp [HSMul.hSMul, basis_on_oddShiftFst_self, Equiv.swap_apply_left]All goals completed! 🐙
  ·negn:ℕS:(PureU1 (2 * n + 1)).LinSolsS':(PureU1 (2 * n + 1)).LinSolsj:Fin nhS:((FamilyPermutations (2 * n + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'i:Fin (PureU1 (2 * n + 1)).numberChargeshi:¬i = oddShiftFst j⊢ S.val ((Equiv.swap (oddShiftFst j) (oddShiftSnd j)).invFun i) =
  (S.val + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basisAsCharges j) i by_cases hi2 : i = oddShiftSnd jposn:ℕS:(PureU1 (2 * n + 1)).LinSolsS':(PureU1 (2 * n + 1)).LinSolsj:Fin nhS:((FamilyPermutations (2 * n + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'i:Fin (PureU1 (2 * n + 1)).numberChargeshi:¬i = oddShiftFst jhi2:i = oddShiftSnd j⊢ S.val ((Equiv.swap (oddShiftFst j) (oddShiftSnd j)).invFun i) =
  (S.val + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basisAsCharges j) inegn:ℕS:(PureU1 (2 * n + 1)).LinSolsS':(PureU1 (2 * n + 1)).LinSolsj:Fin nhS:((FamilyPermutations (2 * n + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'i:Fin (PureU1 (2 * n + 1)).numberChargeshi:¬i = oddShiftFst jhi2:¬i = oddShiftSnd j⊢ S.val ((Equiv.swap (oddShiftFst j) (oddShiftSnd j)).invFun i) =
  (S.val + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basisAsCharges j) i
    ·posn:ℕS:(PureU1 (2 * n + 1)).LinSolsS':(PureU1 (2 * n + 1)).LinSolsj:Fin nhS:((FamilyPermutations (2 * n + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'i:Fin (PureU1 (2 * n + 1)).numberChargeshi:¬i = oddShiftFst jhi2:i = oddShiftSnd j⊢ S.val ((Equiv.swap (oddShiftFst j) (oddShiftSnd j)).invFun i) =
  (S.val + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basisAsCharges j) i subst hi2posn:ℕS:(PureU1 (2 * n + 1)).LinSolsS':(PureU1 (2 * n + 1)).LinSolsj:Fin nhS:((FamilyPermutations (2 * n + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'hi:¬oddShiftSnd j = oddShiftFst j⊢ S.val ((Equiv.swap (oddShiftFst j) (oddShiftSnd j)).invFun (oddShiftSnd j)) =
  (S.val + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basisAsCharges j) (oddShiftSnd j)
      simp [HSMul.hSMul,basis_on_oddShiftSnd_self, Equiv.swap_apply_right]All goals completed! 🐙
    ·negn:ℕS:(PureU1 (2 * n + 1)).LinSolsS':(PureU1 (2 * n + 1)).LinSolsj:Fin nhS:((FamilyPermutations (2 * n + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'i:Fin (PureU1 (2 * n + 1)).numberChargeshi:¬i = oddShiftFst jhi2:¬i = oddShiftSnd j⊢ S.val ((Equiv.swap (oddShiftFst j) (oddShiftSnd j)).invFun i) =
  (S.val + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basisAsCharges j) i simp only [Equiv.invFun_as_coe, HSMul.hSMul, ACCSystemCharges.chargesAddCommMonoid_add,
      ACCSystemCharges.chargesModule_smul]negn:ℕS:(PureU1 (2 * n + 1)).LinSolsS':(PureU1 (2 * n + 1)).LinSolsj:Fin nhS:((FamilyPermutations (2 * n + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'i:Fin (PureU1 (2 * n + 1)).numberChargeshi:¬i = oddShiftFst jhi2:¬i = oddShiftSnd j⊢ S.val ((Equiv.symm (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) i) =
  S.val i + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) * basisAsCharges j i
      rw [basis_on_other hi hi2negn:ℕS:(PureU1 (2 * n + 1)).LinSolsS':(PureU1 (2 * n + 1)).LinSolsj:Fin nhS:((FamilyPermutations (2 * n + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'i:Fin (PureU1 (2 * n + 1)).numberChargeshi:¬i = oddShiftFst jhi2:¬i = oddShiftSnd j⊢ S.val ((Equiv.symm (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) i) =
  S.val i + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) * 0negn:ℕS:(PureU1 (2 * n + 1)).LinSolsS':(PureU1 (2 * n + 1)).LinSolsj:Fin nhS:((FamilyPermutations (2 * n + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'i:Fin (PureU1 (2 * n + 1)).numberChargeshi:¬i = oddShiftFst jhi2:¬i = oddShiftSnd j⊢ S.val ((Equiv.symm (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) i) =
  S.val i + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) * 0]negn:ℕS:(PureU1 (2 * n + 1)).LinSolsS':(PureU1 (2 * n + 1)).LinSolsj:Fin nhS:((FamilyPermutations (2 * n + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'i:Fin (PureU1 (2 * n + 1)).numberChargeshi:¬i = oddShiftFst jhi2:¬i = oddShiftSnd j⊢ S.val ((Equiv.symm (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) i) =
  S.val i + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) * 0
      aesopAll goals completed! 🐙

C.6. The inclusion of the shifted plane into charges

A point in the span of the shifted part of the basis as a charge.

def planeCharges (f : Fin n → ℚ) : (PureU1 (2 * n + 1)).Charges := ∑ i, f i • basisAsCharges i

C.7. Components of the shifted plane

              

lemma planeCharges_oddShiftFst (f : Fin n → ℚ) (j : Fin n) :
    planeCharges f (oddShiftFst j) = f j := byn:ℕf:Fin n → ℚj:Fin n⊢ planeCharges f (oddShiftFst j) = f j
  rw [planeCharges,n:ℕf:Fin n → ℚj:Fin n⊢ (∑ i, f i • basisAsCharges i) (oddShiftFst j) = f jn:ℕf:Fin n → ℚj:Fin n⊢ ∑ i, (f i • basisAsCharges i) (oddShiftFst j) = f j sum_of_chargesn:ℕf:Fin n → ℚj:Fin n⊢ ∑ i, (f i • basisAsCharges i) (oddShiftFst j) = f jn:ℕf:Fin n → ℚj:Fin n⊢ ∑ i, (f i • basisAsCharges i) (oddShiftFst j) = f j]n:ℕf:Fin n → ℚj:Fin n⊢ ∑ i, (f i • basisAsCharges i) (oddShiftFst j) = f j
  simp only [HSMul.hSMul, SMul.smul]n:ℕf:Fin n → ℚj:Fin n⊢ ∑ x, f x * basisAsCharges x (oddShiftFst j) = f j
  rw [Fintype.sum_eq_single jn:ℕf:Fin n → ℚj:Fin n⊢ f j * basisAsCharges j (oddShiftFst j) = f jn:ℕf:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n), x ≠ j → f x * basisAsCharges x (oddShiftFst j) = 0n:ℕf:Fin n → ℚj:Fin n⊢ f j * basisAsCharges j (oddShiftFst j) = f jn:ℕf:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n), x ≠ j → f x * basisAsCharges x (oddShiftFst j) = 0]n:ℕf:Fin n → ℚj:Fin n⊢ f j * basisAsCharges j (oddShiftFst j) = f jn:ℕf:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n), x ≠ j → f x * basisAsCharges x (oddShiftFst j) = 0
  ·n:ℕf:Fin n → ℚj:Fin n⊢ f j * basisAsCharges j (oddShiftFst j) = f j simp [basis_on_oddShiftFst_self]All goals completed! 🐙
  ·n:ℕf:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n), x ≠ j → f x * basisAsCharges x (oddShiftFst j) = 0 intro k hkjn:ℕf:Fin n → ℚj:Fin nk:Fin nhkj:k ≠ j⊢ f k * basisAsCharges k (oddShiftFst j) = 0
    exact mul_eq_zero_of_right (f k) (basis_on_oddShiftFst_other hkj)All goals completed! 🐙

lemma planeCharges_oddShiftSnd (f : Fin n → ℚ) (j : Fin n) :
    planeCharges f (oddShiftSnd j) = - f j := byn:ℕf:Fin n → ℚj:Fin n⊢ planeCharges f (oddShiftSnd j) = -f j
  rw [planeCharges,n:ℕf:Fin n → ℚj:Fin n⊢ (∑ i, f i • basisAsCharges i) (oddShiftSnd j) = -f jn:ℕf:Fin n → ℚj:Fin n⊢ ∑ i, (f i • basisAsCharges i) (oddShiftSnd j) = -f j sum_of_chargesn:ℕf:Fin n → ℚj:Fin n⊢ ∑ i, (f i • basisAsCharges i) (oddShiftSnd j) = -f jn:ℕf:Fin n → ℚj:Fin n⊢ ∑ i, (f i • basisAsCharges i) (oddShiftSnd j) = -f j]n:ℕf:Fin n → ℚj:Fin n⊢ ∑ i, (f i • basisAsCharges i) (oddShiftSnd j) = -f j
  simp only [HSMul.hSMul, SMul.smul]n:ℕf:Fin n → ℚj:Fin n⊢ ∑ x, f x * basisAsCharges x (oddShiftSnd j) = -f j
  rw [Fintype.sum_eq_single jn:ℕf:Fin n → ℚj:Fin n⊢ f j * basisAsCharges j (oddShiftSnd j) = -f jn:ℕf:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n), x ≠ j → f x * basisAsCharges x (oddShiftSnd j) = 0n:ℕf:Fin n → ℚj:Fin n⊢ f j * basisAsCharges j (oddShiftSnd j) = -f jn:ℕf:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n), x ≠ j → f x * basisAsCharges x (oddShiftSnd j) = 0]n:ℕf:Fin n → ℚj:Fin n⊢ f j * basisAsCharges j (oddShiftSnd j) = -f jn:ℕf:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n), x ≠ j → f x * basisAsCharges x (oddShiftSnd j) = 0
  ·n:ℕf:Fin n → ℚj:Fin n⊢ f j * basisAsCharges j (oddShiftSnd j) = -f j simp [basis_on_oddShiftSnd_self]All goals completed! 🐙
  ·n:ℕf:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n), x ≠ j → f x * basisAsCharges x (oddShiftSnd j) = 0 intro k hkjn:ℕf:Fin n → ℚj:Fin nk:Fin nhkj:k ≠ j⊢ f k * basisAsCharges k (oddShiftSnd j) = 0
    exact mul_eq_zero_of_right (f k) (basis_on_oddShiftSnd_other hkj)All goals completed! 🐙

lemma planeCharges_oddShiftZero (f : Fin n → ℚ) : planeCharges f oddShiftZero = 0 := byn:ℕf:Fin n → ℚ⊢ planeCharges f oddShiftZero = 0
  rw [planeCharges,n:ℕf:Fin n → ℚ⊢ (∑ i, f i • basisAsCharges i) oddShiftZero = 0n:ℕf:Fin n → ℚ⊢ ∑ i, (f i • basisAsCharges i) oddShiftZero = 0 sum_of_chargesn:ℕf:Fin n → ℚ⊢ ∑ i, (f i • basisAsCharges i) oddShiftZero = 0n:ℕf:Fin n → ℚ⊢ ∑ i, (f i • basisAsCharges i) oddShiftZero = 0]n:ℕf:Fin n → ℚ⊢ ∑ i, (f i • basisAsCharges i) oddShiftZero = 0
  simp [HSMul.hSMul, SMul.smul, basis_on_oddShiftZero]All goals completed! 🐙

C.8. Points on the shifted plane satisfies the ACCs



lemma planeCharges_linearACC (f : Fin n → ℚ) : (accGrav (2 * n + 1)) (planeCharges f) = 0 := byn:ℕf:Fin n → ℚ⊢ (accGrav (2 * n + 1)) (planeCharges f) = 0
  rw [accGravn:ℕf:Fin n → ℚ⊢ { toFun := fun S => ∑ i, S i, map_add' := ⋯, map_smul' := ⋯ } (planeCharges f) = 0n:ℕf:Fin n → ℚ⊢ { toFun := fun S => ∑ i, S i, map_add' := ⋯, map_smul' := ⋯ } (planeCharges f) = 0]n:ℕf:Fin n → ℚ⊢ { toFun := fun S => ∑ i, S i, map_add' := ⋯, map_smul' := ⋯ } (planeCharges f) = 0
  simp [sum_oddShift, planeCharges_oddShiftSnd, planeCharges_oddShiftFst, planeCharges_oddShiftZero]All goals completed! 🐙



lemma planeCharges_accCube (f : Fin n → ℚ) : accCube (2 * n +1) (planeCharges f) = 0 := byn:ℕf:Fin n → ℚ⊢ (accCube (2 * n + 1)) (planeCharges f) = 0
  rw [accCube_explicit,n:ℕf:Fin n → ℚ⊢ ∑ i, planeCharges f i ^ 3 = 0n:ℕf:Fin n → ℚ⊢ 0 ^ 3 + ∑ i, (((fun i => planeCharges f i ^ 3) ∘ oddShiftFst) i + ((fun i => planeCharges f i ^ 3) ∘ oddShiftSnd) i) = 0 sum_oddShift,n:ℕf:Fin n → ℚ⊢ planeCharges f oddShiftZero ^ 3 +
    ∑ i, (((fun i => planeCharges f i ^ 3) ∘ oddShiftFst) i + ((fun i => planeCharges f i ^ 3) ∘ oddShiftSnd) i) =
  0n:ℕf:Fin n → ℚ⊢ 0 ^ 3 + ∑ i, (((fun i => planeCharges f i ^ 3) ∘ oddShiftFst) i + ((fun i => planeCharges f i ^ 3) ∘ oddShiftSnd) i) = 0 planeCharges_oddShiftZeron:ℕf:Fin n → ℚ⊢ 0 ^ 3 + ∑ i, (((fun i => planeCharges f i ^ 3) ∘ oddShiftFst) i + ((fun i => planeCharges f i ^ 3) ∘ oddShiftSnd) i) = 0n:ℕf:Fin n → ℚ⊢ 0 ^ 3 + ∑ i, (((fun i => planeCharges f i ^ 3) ∘ oddShiftFst) i + ((fun i => planeCharges f i ^ 3) ∘ oddShiftSnd) i) = 0]n:ℕf:Fin n → ℚ⊢ 0 ^ 3 + ∑ i, (((fun i => planeCharges f i ^ 3) ∘ oddShiftFst) i + ((fun i => planeCharges f i ^ 3) ∘ oddShiftSnd) i) = 0
  simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, Function.comp_apply, zero_add]n:ℕf:Fin n → ℚ⊢ ∑ x, (planeCharges f (oddShiftFst x) ^ 3 + planeCharges f (oddShiftSnd x) ^ 3) = 0
  refine Finset.sum_eq_zero fun i _ => ?_n:ℕf:Fin n → ℚi:Fin nx✝:i ∈ univ⊢ planeCharges f (oddShiftFst i) ^ 3 + planeCharges f (oddShiftSnd i) ^ 3 = 0
  simp only [planeCharges_oddShiftFst, planeCharges_oddShiftSnd]n:ℕf:Fin n → ℚi:Fin nx✝:i ∈ univ⊢ f i ^ 3 + (-f i) ^ 3 = 0
  ringAll goals completed! 🐙

C.9. Kernel of the inclusion into charges

lemma planeCharges_zero (f : Fin n → ℚ) (h : planeCharges f = 0) : ∀ i, f i = 0 :=
  fun i => (planeCharges_oddShiftFst f i).symm.trans (congr_fun h (oddShiftFst i))

C.10. The inclusion of the shifted plane into LinSols

A point in the span of the shifted part of the basis.

def planeLinSols (f : Fin n → ℚ) : (PureU1 (2 * n + 1)).LinSols := ∑ i, f i • basis i



lemma planeLinSols_val (f : Fin n → ℚ) : (planeLinSols f).val = planeCharges f := byn:ℕf:Fin n → ℚ⊢ (planeLinSols f).val = planeCharges f
  simp only [planeLinSols, planeCharges]n:ℕf:Fin n → ℚ⊢ (∑ i, f i • basis i).val = ∑ i, f i • basisAsCharges i
  funext in:ℕf:Fin n → ℚi:Fin (PureU1 (2 * n + 1)).numberCharges⊢ (∑ i, f i • basis i).val i = (∑ i, f i • basisAsCharges i) i
  rw [sum_of_anomaly_free_linear,n:ℕf:Fin n → ℚi:Fin (PureU1 (2 * n + 1)).numberCharges⊢ ∑ i_1, (f i_1 • basis i_1).val i = (∑ i, f i • basisAsCharges i) in:ℕf:Fin n → ℚi:Fin (PureU1 (2 * n + 1)).numberCharges⊢ ∑ i_1, (f i_1 • basis i_1).val i = ∑ i_1, (f i_1 • basisAsCharges i_1) i sum_of_chargesn:ℕf:Fin n → ℚi:Fin (PureU1 (2 * n + 1)).numberCharges⊢ ∑ i_1, (f i_1 • basis i_1).val i = ∑ i_1, (f i_1 • basisAsCharges i_1) in:ℕf:Fin n → ℚi:Fin (PureU1 (2 * n + 1)).numberCharges⊢ ∑ i_1, (f i_1 • basis i_1).val i = ∑ i_1, (f i_1 • basisAsCharges i_1) i]n:ℕf:Fin n → ℚi:Fin (PureU1 (2 * n + 1)).numberCharges⊢ ∑ i_1, (f i_1 • basis i_1).val i = ∑ i_1, (f i_1 • basisAsCharges i_1) i
  rflAll goals completed! 🐙

C.11. The basis vectors are linearly independent

theorem basis_linear_independent : LinearIndependent ℚ (@basis n) := byn:ℕ⊢ LinearIndependent ℚ basis
  apply Fintype.linearIndependent_iff.mprn:ℕ⊢ ∀ (g : Fin n → ℚ), ∑ i, g i • basis i = 0 → ∀ (i : Fin n), g i = 0
  intro f hn:ℕf:Fin n → ℚh:∑ i, f i • basis i = 0⊢ ∀ (i : Fin n), f i = 0
  change planeLinSols f = 0 at hn:ℕf:Fin n → ℚh:planeLinSols f = 0⊢ ∀ (i : Fin n), f i = 0
  exact planeCharges_zero f (planeLinSols_val f ▸ congrArg ACCSystemLinear.LinSols.val h)All goals completed! 🐙

D. The mixed cubic ACC from points in both planes



lemma P_P_P!_accCube (g : Fin n → ℚ) (j : Fin n) :
    accCubeTriLinSymm (Unshifted.planeCharges g) (Unshifted.planeCharges g)
      (Shifted.basisAsCharges j)
    = (Unshifted.planeCharges g (oddShiftFst j))^2 - (g j)^2 := byn:ℕg:Fin n → ℚj:Fin n⊢ ((accCubeTriLinSymm (Unshifted.planeCharges g)) (Unshifted.planeCharges g)) (Shifted.basisAsCharges j) =
  Unshifted.planeCharges g (oddShiftFst j) ^ 2 - g j ^ 2
  simp only [accCubeTriLinSymm, TriLinearSymm.mk₃_toFun_apply_apply]n:ℕg:Fin n → ℚj:Fin n⊢ ∑ x, Unshifted.planeCharges g x * Unshifted.planeCharges g x * Shifted.basisAsCharges j x =
  Unshifted.planeCharges g (oddShiftFst j) ^ 2 - g j ^ 2
  erw [sum_oddShift,n:ℕg:Fin n → ℚj:Fin n⊢ Unshifted.planeCharges g oddShiftZero * Unshifted.planeCharges g oddShiftZero * Shifted.basisAsCharges j oddShiftZero +
    ∑ i,
      (((fun x => Unshifted.planeCharges g x * Unshifted.planeCharges g x * Shifted.basisAsCharges j x) ∘ oddShiftFst)
          i +
        ((fun x => Unshifted.planeCharges g x * Unshifted.planeCharges g x * Shifted.basisAsCharges j x) ∘ oddShiftSnd)
          i) =
  Unshifted.planeCharges g (oddShiftFst j) ^ 2 - g j ^ 2 Shifted.basis_on_oddShiftZeron:ℕg:Fin n → ℚj:Fin n⊢ Unshifted.planeCharges g oddShiftZero * Unshifted.planeCharges g oddShiftZero * 0 +
    ∑ i,
      (((fun x => Unshifted.planeCharges g x * Unshifted.planeCharges g x * Shifted.basisAsCharges j x) ∘ oddShiftFst)
          i +
        ((fun x => Unshifted.planeCharges g x * Unshifted.planeCharges g x * Shifted.basisAsCharges j x) ∘ oddShiftSnd)
          i) =
  Unshifted.planeCharges g (oddShiftFst j) ^ 2 - g j ^ 2]n:ℕg:Fin n → ℚj:Fin n⊢ Unshifted.planeCharges g oddShiftZero * Unshifted.planeCharges g oddShiftZero * 0 +
    ∑ i,
      (((fun x => Unshifted.planeCharges g x * Unshifted.planeCharges g x * Shifted.basisAsCharges j x) ∘ oddShiftFst)
          i +
        ((fun x => Unshifted.planeCharges g x * Unshifted.planeCharges g x * Shifted.basisAsCharges j x) ∘ oddShiftSnd)
          i) =
  Unshifted.planeCharges g (oddShiftFst j) ^ 2 - g j ^ 2
  simp only [mul_zero, Function.comp_apply, zero_add]n:ℕg:Fin n → ℚj:Fin n⊢ ∑ x,
    (Unshifted.planeCharges g (oddShiftFst x) * Unshifted.planeCharges g (oddShiftFst x) *
        Shifted.basisAsCharges j (oddShiftFst x) +
      Unshifted.planeCharges g (oddShiftSnd x) * Unshifted.planeCharges g (oddShiftSnd x) *
        Shifted.basisAsCharges j (oddShiftSnd x)) =
  Unshifted.planeCharges g (oddShiftFst j) ^ 2 - g j ^ 2
  rw [Fintype.sum_eq_single j,n:ℕg:Fin n → ℚj:Fin n⊢ Unshifted.planeCharges g (oddShiftFst j) * Unshifted.planeCharges g (oddShiftFst j) *
      Shifted.basisAsCharges j (oddShiftFst j) +
    Unshifted.planeCharges g (oddShiftSnd j) * Unshifted.planeCharges g (oddShiftSnd j) *
      Shifted.basisAsCharges j (oddShiftSnd j) =
  Unshifted.planeCharges g (oddShiftFst j) ^ 2 - g j ^ 2n:ℕg:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n),
  x ≠ j →
    Unshifted.planeCharges g (oddShiftFst x) * Unshifted.planeCharges g (oddShiftFst x) *
          Shifted.basisAsCharges j (oddShiftFst x) +
        Unshifted.planeCharges g (oddShiftSnd x) * Unshifted.planeCharges g (oddShiftSnd x) *
          Shifted.basisAsCharges j (oddShiftSnd x) =
      0n:ℕg:Fin n → ℚj:Fin n⊢ Unshifted.planeCharges g (oddShiftFst j) * Unshifted.planeCharges g (oddShiftFst j) * 1 +
    Unshifted.planeCharges g (oddShiftSnd j) * Unshifted.planeCharges g (oddShiftSnd j) * -1 =
  Unshifted.planeCharges g (oddShiftFst j) ^ 2 - g j ^ 2n:ℕg:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n),
  x ≠ j →
    Unshifted.planeCharges g (oddShiftFst x) * Unshifted.planeCharges g (oddShiftFst x) *
          Shifted.basisAsCharges j (oddShiftFst x) +
        Unshifted.planeCharges g (oddShiftSnd x) * Unshifted.planeCharges g (oddShiftSnd x) *
          Shifted.basisAsCharges j (oddShiftSnd x) =
      0 Shifted.basis_on_oddShiftFst_self,n:ℕg:Fin n → ℚj:Fin n⊢ Unshifted.planeCharges g (oddShiftFst j) * Unshifted.planeCharges g (oddShiftFst j) * 1 +
    Unshifted.planeCharges g (oddShiftSnd j) * Unshifted.planeCharges g (oddShiftSnd j) *
      Shifted.basisAsCharges j (oddShiftSnd j) =
  Unshifted.planeCharges g (oddShiftFst j) ^ 2 - g j ^ 2n:ℕg:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n),
  x ≠ j →
    Unshifted.planeCharges g (oddShiftFst x) * Unshifted.planeCharges g (oddShiftFst x) *
          Shifted.basisAsCharges j (oddShiftFst x) +
        Unshifted.planeCharges g (oddShiftSnd x) * Unshifted.planeCharges g (oddShiftSnd x) *
          Shifted.basisAsCharges j (oddShiftSnd x) =
      0n:ℕg:Fin n → ℚj:Fin n⊢ Unshifted.planeCharges g (oddShiftFst j) * Unshifted.planeCharges g (oddShiftFst j) * 1 +
    Unshifted.planeCharges g (oddShiftSnd j) * Unshifted.planeCharges g (oddShiftSnd j) * -1 =
  Unshifted.planeCharges g (oddShiftFst j) ^ 2 - g j ^ 2n:ℕg:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n),
  x ≠ j →
    Unshifted.planeCharges g (oddShiftFst x) * Unshifted.planeCharges g (oddShiftFst x) *
          Shifted.basisAsCharges j (oddShiftFst x) +
        Unshifted.planeCharges g (oddShiftSnd x) * Unshifted.planeCharges g (oddShiftSnd x) *
          Shifted.basisAsCharges j (oddShiftSnd x) =
      0 Shifted.basis_on_oddShiftSnd_selfn:ℕg:Fin n → ℚj:Fin n⊢ Unshifted.planeCharges g (oddShiftFst j) * Unshifted.planeCharges g (oddShiftFst j) * 1 +
    Unshifted.planeCharges g (oddShiftSnd j) * Unshifted.planeCharges g (oddShiftSnd j) * -1 =
  Unshifted.planeCharges g (oddShiftFst j) ^ 2 - g j ^ 2n:ℕg:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n),
  x ≠ j →
    Unshifted.planeCharges g (oddShiftFst x) * Unshifted.planeCharges g (oddShiftFst x) *
          Shifted.basisAsCharges j (oddShiftFst x) +
        Unshifted.planeCharges g (oddShiftSnd x) * Unshifted.planeCharges g (oddShiftSnd x) *
          Shifted.basisAsCharges j (oddShiftSnd x) =
      0n:ℕg:Fin n → ℚj:Fin n⊢ Unshifted.planeCharges g (oddShiftFst j) * Unshifted.planeCharges g (oddShiftFst j) * 1 +
    Unshifted.planeCharges g (oddShiftSnd j) * Unshifted.planeCharges g (oddShiftSnd j) * -1 =
  Unshifted.planeCharges g (oddShiftFst j) ^ 2 - g j ^ 2n:ℕg:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n),
  x ≠ j →
    Unshifted.planeCharges g (oddShiftFst x) * Unshifted.planeCharges g (oddShiftFst x) *
          Shifted.basisAsCharges j (oddShiftFst x) +
        Unshifted.planeCharges g (oddShiftSnd x) * Unshifted.planeCharges g (oddShiftSnd x) *
          Shifted.basisAsCharges j (oddShiftSnd x) =
      0]n:ℕg:Fin n → ℚj:Fin n⊢ Unshifted.planeCharges g (oddShiftFst j) * Unshifted.planeCharges g (oddShiftFst j) * 1 +
    Unshifted.planeCharges g (oddShiftSnd j) * Unshifted.planeCharges g (oddShiftSnd j) * -1 =
  Unshifted.planeCharges g (oddShiftFst j) ^ 2 - g j ^ 2n:ℕg:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n),
  x ≠ j →
    Unshifted.planeCharges g (oddShiftFst x) * Unshifted.planeCharges g (oddShiftFst x) *
          Shifted.basisAsCharges j (oddShiftFst x) +
        Unshifted.planeCharges g (oddShiftSnd x) * Unshifted.planeCharges g (oddShiftSnd x) *
          Shifted.basisAsCharges j (oddShiftSnd x) =
      0
  ·n:ℕg:Fin n → ℚj:Fin n⊢ Unshifted.planeCharges g (oddShiftFst j) * Unshifted.planeCharges g (oddShiftFst j) * 1 +
    Unshifted.planeCharges g (oddShiftSnd j) * Unshifted.planeCharges g (oddShiftSnd j) * -1 =
  Unshifted.planeCharges g (oddShiftFst j) ^ 2 - g j ^ 2 rw [← oddSnd_eq_oddShiftSnd,n:ℕg:Fin n → ℚj:Fin n⊢ Unshifted.planeCharges g (oddShiftFst j) * Unshifted.planeCharges g (oddShiftFst j) * 1 +
    Unshifted.planeCharges g (oddSnd j) * Unshifted.planeCharges g (oddSnd j) * -1 =
  Unshifted.planeCharges g (oddShiftFst j) ^ 2 - g j ^ 2n:ℕg:Fin n → ℚj:Fin n⊢ Unshifted.planeCharges g (oddShiftFst j) * Unshifted.planeCharges g (oddShiftFst j) * 1 + -g j * -g j * -1 =
  Unshifted.planeCharges g (oddShiftFst j) ^ 2 - g j ^ 2 Unshifted.planeCharges_oddSndn:ℕg:Fin n → ℚj:Fin n⊢ Unshifted.planeCharges g (oddShiftFst j) * Unshifted.planeCharges g (oddShiftFst j) * 1 + -g j * -g j * -1 =
  Unshifted.planeCharges g (oddShiftFst j) ^ 2 - g j ^ 2n:ℕg:Fin n → ℚj:Fin n⊢ Unshifted.planeCharges g (oddShiftFst j) * Unshifted.planeCharges g (oddShiftFst j) * 1 + -g j * -g j * -1 =
  Unshifted.planeCharges g (oddShiftFst j) ^ 2 - g j ^ 2]n:ℕg:Fin n → ℚj:Fin n⊢ Unshifted.planeCharges g (oddShiftFst j) * Unshifted.planeCharges g (oddShiftFst j) * 1 + -g j * -g j * -1 =
  Unshifted.planeCharges g (oddShiftFst j) ^ 2 - g j ^ 2
    ringAll goals completed! 🐙
  ·n:ℕg:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n),
  x ≠ j →
    Unshifted.planeCharges g (oddShiftFst x) * Unshifted.planeCharges g (oddShiftFst x) *
          Shifted.basisAsCharges j (oddShiftFst x) +
        Unshifted.planeCharges g (oddShiftSnd x) * Unshifted.planeCharges g (oddShiftSnd x) *
          Shifted.basisAsCharges j (oddShiftSnd x) =
      0 intro k hkjn:ℕg:Fin n → ℚj:Fin nk:Fin nhkj:k ≠ j⊢ Unshifted.planeCharges g (oddShiftFst k) * Unshifted.planeCharges g (oddShiftFst k) *
      Shifted.basisAsCharges j (oddShiftFst k) +
    Unshifted.planeCharges g (oddShiftSnd k) * Unshifted.planeCharges g (oddShiftSnd k) *
      Shifted.basisAsCharges j (oddShiftSnd k) =
  0
    erw [Shifted.basis_on_oddShiftFst_other hkj.symm,n:ℕg:Fin n → ℚj:Fin nk:Fin nhkj:k ≠ j⊢ Unshifted.planeCharges g (oddShiftFst k) * Unshifted.planeCharges g (oddShiftFst k) * 0 +
    Unshifted.planeCharges g (oddShiftSnd k) * Unshifted.planeCharges g (oddShiftSnd k) *
      Shifted.basisAsCharges j (oddShiftSnd k) =
  0 Shifted.basis_on_oddShiftSnd_other hkj.symmn:ℕg:Fin n → ℚj:Fin nk:Fin nhkj:k ≠ j⊢ Unshifted.planeCharges g (oddShiftFst k) * Unshifted.planeCharges g (oddShiftFst k) * 0 +
    Unshifted.planeCharges g (oddShiftSnd k) * Unshifted.planeCharges g (oddShiftSnd k) * 0 =
  0]n:ℕg:Fin n → ℚj:Fin nk:Fin nhkj:k ≠ j⊢ Unshifted.planeCharges g (oddShiftFst k) * Unshifted.planeCharges g (oddShiftFst k) * 0 +
    Unshifted.planeCharges g (oddShiftSnd k) * Unshifted.planeCharges g (oddShiftSnd k) * 0 =
  0
    simp only [mul_zero, add_zero]All goals completed! 🐙

E. The combined Unshifted.basis

E.1. The combined Unshifted.basis as `LinSols`

The whole Unshifted.basis as LinSols.

def basisa : Fin n ⊕ Fin n → (PureU1 (2 * n + 1)).LinSols := fun i =>
  match i with
  | .inl i => Unshifted.basis i
  | .inr i => Shifted.basis i

E.2. The inclusion of the span of the combined Unshifted.basis into charges

A point in the span of the Unshifted.basis as a charge.

def Pa (f : Fin n → ℚ) (g : Fin n → ℚ) : (PureU1 (2 * n + 1)).Charges :=
  Unshifted.planeCharges f + Shifted.planeCharges g

E.3. Components of the inclusion

              

lemma Pa_oddShiftShiftZero (f g : Fin n.succ → ℚ) : Pa f g oddShiftShiftZero = f 0 := byn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ Pa f g oddShiftShiftZero = f 0
  rw [Pan:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ (Unshifted.planeCharges f + Shifted.planeCharges g) oddShiftShiftZero = f 0n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ (Unshifted.planeCharges f + Shifted.planeCharges g) oddShiftShiftZero = f 0]n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ (Unshifted.planeCharges f + Shifted.planeCharges g) oddShiftShiftZero = f 0
  simp only [ACCSystemCharges.chargesAddCommMonoid_add]n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ Unshifted.planeCharges f oddShiftShiftZero + Shifted.planeCharges g oddShiftShiftZero = f 0
  nth_rewrite 1 [oddShiftShiftZero_eq_oddFst_zero]n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ Unshifted.planeCharges f oddShiftShiftZero + Shifted.planeCharges g oddShiftShiftZero = f 0
  rw [oddShiftShiftZero_eq_oddShiftZeron:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ Unshifted.planeCharges f oddShiftZero + Shifted.planeCharges g oddShiftZero = f 0n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ Unshifted.planeCharges f oddShiftZero + Shifted.planeCharges g oddShiftZero = f 0]n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ Unshifted.planeCharges f oddShiftZero + Shifted.planeCharges g oddShiftZero = f 0
  rw [Shifted.planeCharges_oddShiftZero,n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ Unshifted.planeCharges f oddShiftZero + 0 = f 0All goals completed! 🐙 oddShiftZero_eq_oddFst,n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ Unshifted.planeCharges f (oddFst 0) + 0 = f 0All goals completed! 🐙
    Unshifted.planeCharges_oddFst,n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ f 0 + 0 = f 0All goals completed! 🐙 add_zeron:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ f 0 = f 0All goals completed! 🐙]All goals completed! 🐙

lemma Pa_oddShiftShiftFst (f g : Fin n.succ → ℚ) (j : Fin n) :
    Pa f g (oddShiftShiftFst j) = f j.succ + g j.castSucc := byn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n⊢ Pa f g (oddShiftShiftFst j) = f j.succ + g j.castSucc
  rw [Pan:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n⊢ (Unshifted.planeCharges f + Shifted.planeCharges g) (oddShiftShiftFst j) = f j.succ + g j.castSuccn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n⊢ (Unshifted.planeCharges f + Shifted.planeCharges g) (oddShiftShiftFst j) = f j.succ + g j.castSucc]n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n⊢ (Unshifted.planeCharges f + Shifted.planeCharges g) (oddShiftShiftFst j) = f j.succ + g j.castSucc
  simp only [ACCSystemCharges.chargesAddCommMonoid_add]n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n⊢ Unshifted.planeCharges f (oddShiftShiftFst j) + Shifted.planeCharges g (oddShiftShiftFst j) = f j.succ + g j.castSucc
  nth_rewrite 1 [oddShiftShiftFst_eq_oddFst_succ]n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n⊢ Unshifted.planeCharges f (oddShiftShiftFst j) + Shifted.planeCharges g (oddShiftShiftFst j) = f j.succ + g j.castSucc
  rw [oddShiftShiftFst_eq_oddShiftFst_castSuccn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n⊢ Unshifted.planeCharges f (oddShiftFst j.castSucc) + Shifted.planeCharges g (oddShiftFst j.castSucc) =
  f j.succ + g j.castSuccn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n⊢ Unshifted.planeCharges f (oddShiftFst j.castSucc) + Shifted.planeCharges g (oddShiftFst j.castSucc) =
  f j.succ + g j.castSucc]n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n⊢ Unshifted.planeCharges f (oddShiftFst j.castSucc) + Shifted.planeCharges g (oddShiftFst j.castSucc) =
  f j.succ + g j.castSucc
  rw [Shifted.planeCharges_oddShiftFst,n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n⊢ Unshifted.planeCharges f (oddShiftFst j.castSucc) + g j.castSucc = f j.succ + g j.castSuccAll goals completed! 🐙 oddShiftFst_castSucc_eq_oddFst_succ,n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n⊢ Unshifted.planeCharges f (oddFst j.succ) + g j.castSucc = f j.succ + g j.castSuccAll goals completed! 🐙
    Unshifted.planeCharges_oddFstn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n⊢ f j.succ + g j.castSucc = f j.succ + g j.castSuccAll goals completed! 🐙]All goals completed! 🐙

lemma Pa_oddShiftShiftMid (f g : Fin n.succ → ℚ) : Pa f g oddShiftShiftMid = g (Fin.last n) := byn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ Pa f g oddShiftShiftMid = g (Fin.last n)
  rw [Pan:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ (Unshifted.planeCharges f + Shifted.planeCharges g) oddShiftShiftMid = g (Fin.last n)n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ (Unshifted.planeCharges f + Shifted.planeCharges g) oddShiftShiftMid = g (Fin.last n)]n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ (Unshifted.planeCharges f + Shifted.planeCharges g) oddShiftShiftMid = g (Fin.last n)
  simp only [ACCSystemCharges.chargesAddCommMonoid_add]n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ Unshifted.planeCharges f oddShiftShiftMid + Shifted.planeCharges g oddShiftShiftMid = g (Fin.last n)
  nth_rewrite 1 [oddShiftShiftMid_eq_oddMid]n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ Unshifted.planeCharges f oddShiftShiftMid + Shifted.planeCharges g oddShiftShiftMid = g (Fin.last n)
  rw [oddShiftShiftMid_eq_oddShiftFst_lastn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ Unshifted.planeCharges f (oddShiftFst (Fin.last n)) + Shifted.planeCharges g (oddShiftFst (Fin.last n)) = g (Fin.last n)n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ Unshifted.planeCharges f (oddShiftFst (Fin.last n)) + Shifted.planeCharges g (oddShiftFst (Fin.last n)) = g (Fin.last n)]n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ Unshifted.planeCharges f (oddShiftFst (Fin.last n)) + Shifted.planeCharges g (oddShiftFst (Fin.last n)) = g (Fin.last n)
  rw [Shifted.planeCharges_oddShiftFst,n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ Unshifted.planeCharges f (oddShiftFst (Fin.last n)) + g (Fin.last n) = g (Fin.last n)All goals completed! 🐙 oddShiftFst_last_eq_oddMid,n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ Unshifted.planeCharges f oddMid + g (Fin.last n) = g (Fin.last n)All goals completed! 🐙
    Unshifted.planeCharges_oddMid,n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ 0 + g (Fin.last n) = g (Fin.last n)All goals completed! 🐙 zero_addn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ g (Fin.last n) = g (Fin.last n)All goals completed! 🐙]All goals completed! 🐙

lemma Pa_oddShiftShiftSnd (f g : Fin n.succ → ℚ) (j : Fin n.succ) :
    Pa f g (oddShiftShiftSnd j) = - f j - g j := byn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n.succ⊢ Pa f g (oddShiftShiftSnd j) = -f j - g j
  rw [Pan:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n.succ⊢ (Unshifted.planeCharges f + Shifted.planeCharges g) (oddShiftShiftSnd j) = -f j - g jn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n.succ⊢ (Unshifted.planeCharges f + Shifted.planeCharges g) (oddShiftShiftSnd j) = -f j - g j]n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n.succ⊢ (Unshifted.planeCharges f + Shifted.planeCharges g) (oddShiftShiftSnd j) = -f j - g j
  simp only [ACCSystemCharges.chargesAddCommMonoid_add]n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n.succ⊢ Unshifted.planeCharges f (oddShiftShiftSnd j) + Shifted.planeCharges g (oddShiftShiftSnd j) = -f j - g j
  nth_rewrite 1 [oddShiftShiftSnd_eq_oddSnd]n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n.succ⊢ Unshifted.planeCharges f (oddShiftShiftSnd j) + Shifted.planeCharges g (oddShiftShiftSnd j) = -f j - g j
  rw [oddShiftShiftSnd_eq_oddShiftSndn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n.succ⊢ Unshifted.planeCharges f (oddShiftSnd j) + Shifted.planeCharges g (oddShiftSnd j) = -f j - g jn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n.succ⊢ Unshifted.planeCharges f (oddShiftSnd j) + Shifted.planeCharges g (oddShiftSnd j) = -f j - g j]n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n.succ⊢ Unshifted.planeCharges f (oddShiftSnd j) + Shifted.planeCharges g (oddShiftSnd j) = -f j - g j
  rw [Shifted.planeCharges_oddShiftSnd,n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n.succ⊢ Unshifted.planeCharges f (oddShiftSnd j) + -g j = -f j - g jn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n.succ⊢ -f j + -g j = -f j - g j oddShiftSnd_eq_oddSnd,n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n.succ⊢ Unshifted.planeCharges f (oddSnd j) + -g j = -f j - g jn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n.succ⊢ -f j + -g j = -f j - g j Unshifted.planeCharges_oddSndn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n.succ⊢ -f j + -g j = -f j - g jn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n.succ⊢ -f j + -g j = -f j - g j]n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n.succ⊢ -f j + -g j = -f j - g j
  ringAll goals completed! 🐙

E.4. Kernel of the inclusion into charges



lemma Pa_zero (f g : Fin n.succ → ℚ) (h : Pa f g = 0) :
    ∀ i, f i = 0 := byn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0⊢ ∀ (i : Fin n.succ), f i = 0
  have h₃ := Pa_oddShiftShiftZero f gn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:Pa f g oddShiftShiftZero = f 0⊢ ∀ (i : Fin n.succ), f i = 0
  rw [hn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 oddShiftShiftZero = f 0⊢ ∀ (i : Fin n.succ), f i = 0n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 oddShiftShiftZero = f 0⊢ ∀ (i : Fin n.succ), f i = 0] at h₃n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 oddShiftShiftZero = f 0⊢ ∀ (i : Fin n.succ), f i = 0
  change 0 = _ at h₃n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 = f 0⊢ ∀ (i : Fin n.succ), f i = 0
  intro in:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 = f 0i:Fin n.succ⊢ f i = 0
  have hinduc (iv : ℕ) (hiv : iv < n.succ) : f ⟨iv, hiv⟩ = 0 := byn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0⊢ ∀ (i : Fin n.succ), f i = 0n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 = f 0i:Fin n.succhinduc:∀ (iv : ℕ) (hiv : iv < n.succ), f ⟨iv, hiv⟩ = 0⊢ f i = 0
    induction ivzeron:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 = f 0i:Fin n.succhiv:0 < n.succ⊢ f ⟨0, hiv⟩ = 0succn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 = f 0i:Fin n.succn✝:ℕa✝:∀ (hiv : n✝ < n.succ), f ⟨n✝, hiv⟩ = 0hiv:n✝ + 1 < n.succ⊢ f ⟨n✝ + 1, hiv⟩ = 0n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 = f 0i:Fin n.succhinduc:∀ (iv : ℕ) (hiv : iv < n.succ), f ⟨iv, hiv⟩ = 0⊢ f i = 0
    exact h₃.symmsuccn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 = f 0i:Fin n.succn✝:ℕa✝:∀ (hiv : n✝ < n.succ), f ⟨n✝, hiv⟩ = 0hiv:n✝ + 1 < n.succ⊢ f ⟨n✝ + 1, hiv⟩ = 0n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 = f 0i:Fin n.succhinduc:∀ (iv : ℕ) (hiv : iv < n.succ), f ⟨iv, hiv⟩ = 0⊢ f i = 0
    rename_i iv hisuccn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 = f 0i:Fin n.succiv:ℕhi:∀ (hiv : n✝ < n.succ), f ⟨n✝, hiv⟩ = 0hiv:n✝ + 1 < n.succ⊢ f ⟨n✝ + 1, hiv⟩ = 0n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 = f 0i:Fin n.succhinduc:∀ (iv : ℕ) (hiv : iv < n.succ), f ⟨iv, hiv⟩ = 0⊢ f i = 0
    have hivi : iv < n.succ := lt_of_succ_lt hivsuccn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 = f 0i:Fin n.succiv:ℕhi:∀ (hiv : n✝ < n.succ), f ⟨n✝, hiv⟩ = 0hiv:n✝ + 1 < n.succhivi:iv < n.succ⊢ f ⟨iv + 1, hiv⟩ = 0n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 = f 0i:Fin n.succhinduc:∀ (iv : ℕ) (hiv : iv < n.succ), f ⟨iv, hiv⟩ = 0⊢ f i = 0
    have hi2 := hi hivisuccn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 = f 0i:Fin n.succiv:ℕhi:∀ (hiv : n✝ < n.succ), f ⟨n✝, hiv⟩ = 0hiv:n✝ + 1 < n.succhivi:iv < n.succhi2:f ⟨iv, hivi⟩ = 0⊢ f ⟨iv + 1, hiv⟩ = 0n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 = f 0i:Fin n.succhinduc:∀ (iv : ℕ) (hiv : iv < n.succ), f ⟨iv, hiv⟩ = 0⊢ f i = 0
    have h1 := Pa_oddShiftShiftSnd f g ⟨iv, hivi⟩succn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 = f 0i:Fin n.succiv:ℕhi:∀ (hiv : n✝ < n.succ), f ⟨n✝, hiv⟩ = 0hiv:n✝ + 1 < n.succhivi:iv < n.succhi2:f ⟨iv, hivi⟩ = 0h1:Pa f g (oddShiftShiftSnd ⟨iv, hivi⟩) = -f ⟨iv, hivi⟩ - g ⟨iv, hivi⟩⊢ f ⟨iv + 1, hiv⟩ = 0n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 = f 0i:Fin n.succhinduc:∀ (iv : ℕ) (hiv : iv < n.succ), f ⟨iv, hiv⟩ = 0⊢ f i = 0
    rw [h,succn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 = f 0i:Fin n.succiv:ℕhi:∀ (hiv : n✝ < n.succ), f ⟨n✝, hiv⟩ = 0hiv:n✝ + 1 < n.succhivi:iv < n.succhi2:f ⟨iv, hivi⟩ = 0h1:0 (oddShiftShiftSnd ⟨iv, hivi⟩) = -f ⟨iv, hivi⟩ - g ⟨iv, hivi⟩⊢ f ⟨iv + 1, hiv⟩ = 0succn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 = f 0i:Fin n.succiv:ℕhi:∀ (hiv : n✝ < n.succ), f ⟨n✝, hiv⟩ = 0hiv:n✝ + 1 < n.succhivi:iv < n.succhi2:f ⟨iv, hivi⟩ = 0h1:0 (oddShiftShiftSnd ⟨iv, hivi⟩) = -0 - g ⟨iv, hivi⟩⊢ f ⟨iv + 1, hiv⟩ = 0n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 = f 0i:Fin n.succhinduc:∀ (iv : ℕ) (hiv : iv < n.succ), f ⟨iv, hiv⟩ = 0⊢ f i = 0 hi2succn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 = f 0i:Fin n.succiv:ℕhi:∀ (hiv : n✝ < n.succ), f ⟨n✝, hiv⟩ = 0hiv:n✝ + 1 < n.succhivi:iv < n.succhi2:f ⟨iv, hivi⟩ = 0h1:0 (oddShiftShiftSnd ⟨iv, hivi⟩) = -0 - g ⟨iv, hivi⟩⊢ f ⟨iv + 1, hiv⟩ = 0succn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 = f 0i:Fin n.succiv:ℕhi:∀ (hiv : n✝ < n.succ), f ⟨n✝, hiv⟩ = 0hiv:n✝ + 1 < n.succhivi:iv < n.succhi2:f ⟨iv, hivi⟩ = 0h1:0 (oddShiftShiftSnd ⟨iv, hivi⟩) = -0 - g ⟨iv, hivi⟩⊢ f ⟨iv + 1, hiv⟩ = 0n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 = f 0i:Fin n.succhinduc:∀ (iv : ℕ) (hiv : iv < n.succ), f ⟨iv, hiv⟩ = 0⊢ f i = 0] at h1succn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 = f 0i:Fin n.succiv:ℕhi:∀ (hiv : n✝ < n.succ), f ⟨n✝, hiv⟩ = 0hiv:n✝ + 1 < n.succhivi:iv < n.succhi2:f ⟨iv, hivi⟩ = 0h1:0 (oddShiftShiftSnd ⟨iv, hivi⟩) = -0 - g ⟨iv, hivi⟩⊢ f ⟨iv + 1, hiv⟩ = 0n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 = f 0i:Fin n.succhinduc:∀ (iv : ℕ) (hiv : iv < n.succ), f ⟨iv, hiv⟩ = 0⊢ f i = 0
    change 0 = _ at h1succn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 = f 0i:Fin n.succiv:ℕhi:∀ (hiv : n✝ < n.succ), f ⟨n✝, hiv⟩ = 0hiv:n✝ + 1 < n.succhivi:iv < n.succhi2:f ⟨iv, hivi⟩ = 0h1:0 = -0 - g ⟨iv, hivi⟩⊢ f ⟨iv + 1, hiv⟩ = 0n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 = f 0i:Fin n.succhinduc:∀ (iv : ℕ) (hiv : iv < n.succ), f ⟨iv, hiv⟩ = 0⊢ f i = 0
    simp only [neg_zero, succ_eq_add_one, zero_sub, zero_eq_neg] at h1succn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 = f 0i:Fin n.succiv:ℕhi:∀ (hiv : n✝ < n.succ), f ⟨n✝, hiv⟩ = 0hiv:n✝ + 1 < n.succhivi:iv < n.succhi2:f ⟨iv, hivi⟩ = 0h1:g ⟨iv, hivi⟩ = 0⊢ f ⟨iv + 1, hiv⟩ = 0n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 = f 0i:Fin n.succhinduc:∀ (iv : ℕ) (hiv : iv < n.succ), f ⟨iv, hiv⟩ = 0⊢ f i = 0
    have h2 := Pa_oddShiftShiftFst f g ⟨iv, succ_lt_succ_iff.mp hiv⟩succn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 = f 0i:Fin n.succiv:ℕhi:∀ (hiv : n✝ < n.succ), f ⟨n✝, hiv⟩ = 0hiv:n✝ + 1 < n.succhivi:iv < n.succhi2:f ⟨iv, hivi⟩ = 0h1:g ⟨iv, hivi⟩ = 0h2:Pa f g (oddShiftShiftFst ⟨iv, ⋯⟩) = f ⟨iv, ⋯⟩.succ + g ⟨iv, ⋯⟩.castSucc⊢ f ⟨iv + 1, hiv⟩ = 0n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 = f 0i:Fin n.succhinduc:∀ (iv : ℕ) (hiv : iv < n.succ), f ⟨iv, hiv⟩ = 0⊢ f i = 0
    simp only [succ_eq_add_one, h, Fin.succ_mk, Fin.castSucc_mk, h1, add_zero] at h2succn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 = f 0i:Fin n.succiv:ℕhi:∀ (hiv : n✝ < n.succ), f ⟨n✝, hiv⟩ = 0hiv:n✝ + 1 < n.succhivi:iv < n.succhi2:f ⟨iv, hivi⟩ = 0h1:g ⟨iv, hivi⟩ = 0h2:0 (oddShiftShiftFst ⟨iv, ⋯⟩) = f ⟨iv + 1, ⋯⟩⊢ f ⟨iv + 1, hiv⟩ = 0n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 = f 0i:Fin n.succhinduc:∀ (iv : ℕ) (hiv : iv < n.succ), f ⟨iv, hiv⟩ = 0⊢ f i = 0
    exact h2.symmn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 = f 0i:Fin n.succhinduc:∀ (iv : ℕ) (hiv : iv < n.succ), f ⟨iv, hiv⟩ = 0⊢ f i = 0n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0h₃:0 = f 0i:Fin n.succhinduc:∀ (iv : ℕ) (hiv : iv < n.succ), f ⟨iv, hiv⟩ = 0⊢ f i = 0
  exact hinduc i.val i.propAll goals completed! 🐙



lemma Pa_zero! (f g : Fin n.succ → ℚ) (h : Pa f g = 0) :
    ∀ i, g i = 0 := byn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0⊢ ∀ (i : Fin n.succ), g i = 0
  have hf := Pa_zero f g hn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Pa f g = 0hf:∀ (i : Fin n.succ), f i = 0⊢ ∀ (i : Fin n.succ), g i = 0
  rw [Pa,n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:Unshifted.planeCharges f + Shifted.planeCharges g = 0hf:∀ (i : Fin n.succ), f i = 0⊢ ∀ (i : Fin n.succ), g i = 0n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:∑ i, f i • Unshifted.basisAsCharges i + Shifted.planeCharges g = 0hf:∀ (i : Fin n.succ), f i = 0⊢ ∀ (i : Fin n.succ), g i = 0 Unshifted.planeChargesn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:∑ i, f i • Unshifted.basisAsCharges i + Shifted.planeCharges g = 0hf:∀ (i : Fin n.succ), f i = 0⊢ ∀ (i : Fin n.succ), g i = 0n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:∑ i, f i • Unshifted.basisAsCharges i + Shifted.planeCharges g = 0hf:∀ (i : Fin n.succ), f i = 0⊢ ∀ (i : Fin n.succ), g i = 0] at hn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:∑ i, f i • Unshifted.basisAsCharges i + Shifted.planeCharges g = 0hf:∀ (i : Fin n.succ), f i = 0⊢ ∀ (i : Fin n.succ), g i = 0
  simp only [succ_eq_add_one, hf, zero_smul, sum_const_zero, zero_add] at hn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚhf:∀ (i : Fin n.succ), f i = 0h:Shifted.planeCharges g = 0⊢ ∀ (i : Fin n.succ), g i = 0
  exact Shifted.planeCharges_zero g hAll goals completed! 🐙

E.5. The inclusion of the span of the combined Unshifted.basis into LinSols

A point in the span of the whole Unshifted.basis.

def Pa' (f : (Fin n) ⊕ (Fin n) → ℚ) : (PureU1 (2 * n + 1)).LinSols :=
    ∑ i, f i • basisa i

lemma Pa'_P'_P!' (f : (Fin n) ⊕ (Fin n) → ℚ) :
    Pa' f = Unshifted.planeLinSols (f ∘ Sum.inl) + Shifted.planeLinSols (f ∘ Sum.inr) := byn:ℕf:Fin n ⊕ Fin n → ℚ⊢ Pa' f = Unshifted.planeLinSols (f ∘ Sum.inl) + Shifted.planeLinSols (f ∘ Sum.inr)
  exact Fintype.sum_sum_type _All goals completed! 🐙

E.6. The combined Unshifted.basis vectors are linearly independent



theorem basisa_linear_independent : LinearIndependent ℚ (@basisa n.succ) := byn:ℕ⊢ LinearIndependent ℚ basisa
  apply Fintype.linearIndependent_iff.mprn:ℕ⊢ ∀ (g : Fin n.succ ⊕ Fin n.succ → ℚ), ∑ i, g i • basisa i = 0 → ∀ (i : Fin n.succ ⊕ Fin n.succ), g i = 0
  intro f hn:ℕf:Fin n.succ ⊕ Fin n.succ → ℚh:∑ i, f i • basisa i = 0⊢ ∀ (i : Fin n.succ ⊕ Fin n.succ), f i = 0
  change Pa' f = 0 at hn:ℕf:Fin n.succ ⊕ Fin n.succ → ℚh:Pa' f = 0⊢ ∀ (i : Fin n.succ ⊕ Fin n.succ), f i = 0
  have h1 : (Pa' f).val = 0 := congrArg ACCSystemLinear.LinSols.val hn:ℕf:Fin n.succ ⊕ Fin n.succ → ℚh:Pa' f = 0h1:(Pa' f).val = 0⊢ ∀ (i : Fin n.succ ⊕ Fin n.succ), f i = 0
  rw [Pa'_P'_P!'n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚh:Pa' f = 0h1:(Unshifted.planeLinSols (f ∘ Sum.inl) + Shifted.planeLinSols (f ∘ Sum.inr)).val = 0⊢ ∀ (i : Fin n.succ ⊕ Fin n.succ), f i = 0n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚh:Pa' f = 0h1:(Unshifted.planeLinSols (f ∘ Sum.inl) + Shifted.planeLinSols (f ∘ Sum.inr)).val = 0⊢ ∀ (i : Fin n.succ ⊕ Fin n.succ), f i = 0] at h1n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚh:Pa' f = 0h1:(Unshifted.planeLinSols (f ∘ Sum.inl) + Shifted.planeLinSols (f ∘ Sum.inr)).val = 0⊢ ∀ (i : Fin n.succ ⊕ Fin n.succ), f i = 0
  change (Unshifted.planeLinSols (f ∘ Sum.inl)).val +
      (Shifted.planeLinSols (f ∘ Sum.inr)).val = 0 at h1n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚh:Pa' f = 0h1:(Unshifted.planeLinSols (f ∘ Sum.inl)).val + (Shifted.planeLinSols (f ∘ Sum.inr)).val = 0⊢ ∀ (i : Fin n.succ ⊕ Fin n.succ), f i = 0
  rw [Shifted.planeLinSols_val,n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚh:Pa' f = 0h1:(Unshifted.planeLinSols (f ∘ Sum.inl)).val + Shifted.planeCharges (f ∘ Sum.inr) = 0⊢ ∀ (i : Fin n.succ ⊕ Fin n.succ), f i = 0n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚh:Pa' f = 0h1:Unshifted.planeCharges (f ∘ Sum.inl) + Shifted.planeCharges (f ∘ Sum.inr) = 0⊢ ∀ (i : Fin n.succ ⊕ Fin n.succ), f i = 0 Unshifted.planeLinSols_valn:ℕf:Fin n.succ ⊕ Fin n.succ → ℚh:Pa' f = 0h1:Unshifted.planeCharges (f ∘ Sum.inl) + Shifted.planeCharges (f ∘ Sum.inr) = 0⊢ ∀ (i : Fin n.succ ⊕ Fin n.succ), f i = 0n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚh:Pa' f = 0h1:Unshifted.planeCharges (f ∘ Sum.inl) + Shifted.planeCharges (f ∘ Sum.inr) = 0⊢ ∀ (i : Fin n.succ ⊕ Fin n.succ), f i = 0] at h1n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚh:Pa' f = 0h1:Unshifted.planeCharges (f ∘ Sum.inl) + Shifted.planeCharges (f ∘ Sum.inr) = 0⊢ ∀ (i : Fin n.succ ⊕ Fin n.succ), f i = 0
  change Pa (f ∘ Sum.inl) (f ∘ Sum.inr) = 0 at h1n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚh:Pa' f = 0h1:Pa (f ∘ Sum.inl) (f ∘ Sum.inr) = 0⊢ ∀ (i : Fin n.succ ⊕ Fin n.succ), f i = 0
  have hf := Pa_zero (f ∘ Sum.inl) (f ∘ Sum.inr) h1n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚh:Pa' f = 0h1:Pa (f ∘ Sum.inl) (f ∘ Sum.inr) = 0hf:∀ (i : Fin n.succ), (f ∘ Sum.inl) i = 0⊢ ∀ (i : Fin n.succ ⊕ Fin n.succ), f i = 0
  have hg := Pa_zero! (f ∘ Sum.inl) (f ∘ Sum.inr) h1n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚh:Pa' f = 0h1:Pa (f ∘ Sum.inl) (f ∘ Sum.inr) = 0hf:∀ (i : Fin n.succ), (f ∘ Sum.inl) i = 0hg:∀ (i : Fin n.succ), (f ∘ Sum.inr) i = 0⊢ ∀ (i : Fin n.succ ⊕ Fin n.succ), f i = 0
  intro in:ℕf:Fin n.succ ⊕ Fin n.succ → ℚh:Pa' f = 0h1:Pa (f ∘ Sum.inl) (f ∘ Sum.inr) = 0hf:∀ (i : Fin n.succ), (f ∘ Sum.inl) i = 0hg:∀ (i : Fin n.succ), (f ∘ Sum.inr) i = 0i:Fin n.succ ⊕ Fin n.succ⊢ f i = 0
  simp_all only [succ_eq_add_one, Function.comp_apply]n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚi:Fin n.succ ⊕ Fin n.succh:Pa' f = 0h1:Pa (f ∘ Sum.inl) (f ∘ Sum.inr) = 0hf:∀ (i : Fin (n + 1)), f (Sum.inl i) = 0hg:∀ (i : Fin (n + 1)), f (Sum.inr i) = 0⊢ f i = 0
  cases iinln:ℕf:Fin n.succ ⊕ Fin n.succ → ℚh:Pa' f = 0h1:Pa (f ∘ Sum.inl) (f ∘ Sum.inr) = 0hf:∀ (i : Fin (n + 1)), f (Sum.inl i) = 0hg:∀ (i : Fin (n + 1)), f (Sum.inr i) = 0val✝:Fin n.succ⊢ f (Sum.inl val✝) = 0inrn:ℕf:Fin n.succ ⊕ Fin n.succ → ℚh:Pa' f = 0h1:Pa (f ∘ Sum.inl) (f ∘ Sum.inr) = 0hf:∀ (i : Fin (n + 1)), f (Sum.inl i) = 0hg:∀ (i : Fin (n + 1)), f (Sum.inr i) = 0val✝:Fin n.succ⊢ f (Sum.inr val✝) = 0 <;>inln:ℕf:Fin n.succ ⊕ Fin n.succ → ℚh:Pa' f = 0h1:Pa (f ∘ Sum.inl) (f ∘ Sum.inr) = 0hf:∀ (i : Fin (n + 1)), f (Sum.inl i) = 0hg:∀ (i : Fin (n + 1)), f (Sum.inr i) = 0val✝:Fin n.succ⊢ f (Sum.inl val✝) = 0inrn:ℕf:Fin n.succ ⊕ Fin n.succ → ℚh:Pa' f = 0h1:Pa (f ∘ Sum.inl) (f ∘ Sum.inr) = 0hf:∀ (i : Fin (n + 1)), f (Sum.inl i) = 0hg:∀ (i : Fin (n + 1)), f (Sum.inr i) = 0val✝:Fin n.succ⊢ f (Sum.inr val✝) = 0 simp_allAll goals completed! 🐙

E.7. Injectivity of the inclusion into linear solutions

              

lemma Pa'_eq (f f' : (Fin n.succ) ⊕ (Fin n.succ) → ℚ) : Pa' f = Pa' f' ↔ f = f' := byn:ℕf:Fin n.succ ⊕ Fin n.succ → ℚf':Fin n.succ ⊕ Fin n.succ → ℚ⊢ Pa' f = Pa' f' ↔ f = f'
  refine Iff.intro (fun h => ?_) (fun h => ?_)refine_1n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚf':Fin n.succ ⊕ Fin n.succ → ℚh:Pa' f = Pa' f'⊢ f = f'refine_2n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚf':Fin n.succ ⊕ Fin n.succ → ℚh:f = f'⊢ Pa' f = Pa' f'
  ·refine_1n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚf':Fin n.succ ⊕ Fin n.succ → ℚh:Pa' f = Pa' f'⊢ f = f' funext irefine_1n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚf':Fin n.succ ⊕ Fin n.succ → ℚh:Pa' f = Pa' f'i:Fin n.succ ⊕ Fin n.succ⊢ f i = f' i
    rw [Pa',refine_1n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚf':Fin n.succ ⊕ Fin n.succ → ℚh:∑ i, f i • basisa i = Pa' f'i:Fin n.succ ⊕ Fin n.succ⊢ f i = f' irefine_1n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚf':Fin n.succ ⊕ Fin n.succ → ℚh:∑ i, f i • basisa i = ∑ i, f' i • basisa ii:Fin n.succ ⊕ Fin n.succ⊢ f i = f' i Pa'refine_1n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚf':Fin n.succ ⊕ Fin n.succ → ℚh:∑ i, f i • basisa i = ∑ i, f' i • basisa ii:Fin n.succ ⊕ Fin n.succ⊢ f i = f' irefine_1n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚf':Fin n.succ ⊕ Fin n.succ → ℚh:∑ i, f i • basisa i = ∑ i, f' i • basisa ii:Fin n.succ ⊕ Fin n.succ⊢ f i = f' i] at hrefine_1n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚf':Fin n.succ ⊕ Fin n.succ → ℚh:∑ i, f i • basisa i = ∑ i, f' i • basisa ii:Fin n.succ ⊕ Fin n.succ⊢ f i = f' i
    have h1 : ∑ i : Fin n.succ ⊕ Fin n.succ, (f i + (- f' i)) • basisa i = 0 := byn:ℕf:Fin n.succ ⊕ Fin n.succ → ℚf':Fin n.succ ⊕ Fin n.succ → ℚ⊢ Pa' f = Pa' f' ↔ f = f'refine_1n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚf':Fin n.succ ⊕ Fin n.succ → ℚh:∑ i, f i • basisa i = ∑ i, f' i • basisa ii:Fin n.succ ⊕ Fin n.succh1:∑ i, (f i + -f' i) • basisa i = 0⊢ f i = f' i
      simp only [add_smul, neg_smul]n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚf':Fin n.succ ⊕ Fin n.succ → ℚh:∑ i, f i • basisa i = ∑ i, f' i • basisa ii:Fin n.succ ⊕ Fin n.succ⊢ ∑ x, (f x • basisa x + -(f' x • basisa x)) = 0refine_1n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚf':Fin n.succ ⊕ Fin n.succ → ℚh:∑ i, f i • basisa i = ∑ i, f' i • basisa ii:Fin n.succ ⊕ Fin n.succh1:∑ i, (f i + -f' i) • basisa i = 0⊢ f i = f' i
      rw [Finset.sum_add_distrib,n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚf':Fin n.succ ⊕ Fin n.succ → ℚh:∑ i, f i • basisa i = ∑ i, f' i • basisa ii:Fin n.succ ⊕ Fin n.succ⊢ ∑ x, f x • basisa x + ∑ x, -(f' x • basisa x) = 0n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚf':Fin n.succ ⊕ Fin n.succ → ℚh:∑ i, f i • basisa i = ∑ i, f' i • basisa ii:Fin n.succ ⊕ Fin n.succ⊢ ∑ x, (f' x • basisa x + -(f' x • basisa x)) = 0refine_1n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚf':Fin n.succ ⊕ Fin n.succ → ℚh:∑ i, f i • basisa i = ∑ i, f' i • basisa ii:Fin n.succ ⊕ Fin n.succh1:∑ i, (f i + -f' i) • basisa i = 0⊢ f i = f' i h,n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚf':Fin n.succ ⊕ Fin n.succ → ℚh:∑ i, f i • basisa i = ∑ i, f' i • basisa ii:Fin n.succ ⊕ Fin n.succ⊢ ∑ i, f' i • basisa i + ∑ x, -(f' x • basisa x) = 0n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚf':Fin n.succ ⊕ Fin n.succ → ℚh:∑ i, f i • basisa i = ∑ i, f' i • basisa ii:Fin n.succ ⊕ Fin n.succ⊢ ∑ x, (f' x • basisa x + -(f' x • basisa x)) = 0refine_1n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚf':Fin n.succ ⊕ Fin n.succ → ℚh:∑ i, f i • basisa i = ∑ i, f' i • basisa ii:Fin n.succ ⊕ Fin n.succh1:∑ i, (f i + -f' i) • basisa i = 0⊢ f i = f' i ← Finset.sum_add_distribn:ℕf:Fin n.succ ⊕ Fin n.succ → ℚf':Fin n.succ ⊕ Fin n.succ → ℚh:∑ i, f i • basisa i = ∑ i, f' i • basisa ii:Fin n.succ ⊕ Fin n.succ⊢ ∑ x, (f' x • basisa x + -(f' x • basisa x)) = 0n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚf':Fin n.succ ⊕ Fin n.succ → ℚh:∑ i, f i • basisa i = ∑ i, f' i • basisa ii:Fin n.succ ⊕ Fin n.succ⊢ ∑ x, (f' x • basisa x + -(f' x • basisa x)) = 0refine_1n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚf':Fin n.succ ⊕ Fin n.succ → ℚh:∑ i, f i • basisa i = ∑ i, f' i • basisa ii:Fin n.succ ⊕ Fin n.succh1:∑ i, (f i + -f' i) • basisa i = 0⊢ f i = f' i]n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚf':Fin n.succ ⊕ Fin n.succ → ℚh:∑ i, f i • basisa i = ∑ i, f' i • basisa ii:Fin n.succ ⊕ Fin n.succ⊢ ∑ x, (f' x • basisa x + -(f' x • basisa x)) = 0refine_1n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚf':Fin n.succ ⊕ Fin n.succ → ℚh:∑ i, f i • basisa i = ∑ i, f' i • basisa ii:Fin n.succ ⊕ Fin n.succh1:∑ i, (f i + -f' i) • basisa i = 0⊢ f i = f' i
      simprefine_1n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚf':Fin n.succ ⊕ Fin n.succ → ℚh:∑ i, f i • basisa i = ∑ i, f' i • basisa ii:Fin n.succ ⊕ Fin n.succh1:∑ i, (f i + -f' i) • basisa i = 0⊢ f i = f' irefine_1n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚf':Fin n.succ ⊕ Fin n.succ → ℚh:∑ i, f i • basisa i = ∑ i, f' i • basisa ii:Fin n.succ ⊕ Fin n.succh1:∑ i, (f i + -f' i) • basisa i = 0⊢ f i = f' i
    have h2 : ∀ i, (f i + (- f' i)) = 0 :=
      Fintype.linearIndependent_iff.mp (@basisa_linear_independent n) (fun i => f i + -f' i) h1refine_1n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚf':Fin n.succ ⊕ Fin n.succ → ℚh:∑ i, f i • basisa i = ∑ i, f' i • basisa ii:Fin n.succ ⊕ Fin n.succh1:∑ i, (f i + -f' i) • basisa i = 0h2:∀ (i : Fin n.succ ⊕ Fin n.succ), f i + -f' i = 0⊢ f i = f' i
    linarith [h2 i]All goals completed! 🐙
  ·refine_2n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚf':Fin n.succ ⊕ Fin n.succ → ℚh:f = f'⊢ Pa' f = Pa' f' rw [hrefine_2n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚf':Fin n.succ ⊕ Fin n.succ → ℚh:f = f'⊢ Pa' f' = Pa' f'All goals completed! 🐙]All goals completed! 🐙

lemma Pa'_elim_eq_iff (g g' : Fin n.succ → ℚ) (f f' : Fin n.succ → ℚ) :
    Pa' (Sum.elim g f) = Pa' (Sum.elim g' f') ↔ Pa g f = Pa g' f' := byn:ℕg:Fin n.succ → ℚg':Fin n.succ → ℚf:Fin n.succ → ℚf':Fin n.succ → ℚ⊢ Pa' (Sum.elim g f) = Pa' (Sum.elim g' f') ↔ Pa g f = Pa g' f'
  refine Iff.intro (fun h => ?_) (fun h => ?_)refine_1n:ℕg:Fin n.succ → ℚg':Fin n.succ → ℚf:Fin n.succ → ℚf':Fin n.succ → ℚh:Pa' (Sum.elim g f) = Pa' (Sum.elim g' f')⊢ Pa g f = Pa g' f'refine_2n:ℕg:Fin n.succ → ℚg':Fin n.succ → ℚf:Fin n.succ → ℚf':Fin n.succ → ℚh:Pa g f = Pa g' f'⊢ Pa' (Sum.elim g f) = Pa' (Sum.elim g' f')
  ·refine_1n:ℕg:Fin n.succ → ℚg':Fin n.succ → ℚf:Fin n.succ → ℚf':Fin n.succ → ℚh:Pa' (Sum.elim g f) = Pa' (Sum.elim g' f')⊢ Pa g f = Pa g' f' rw [Pa'_eq,refine_1n:ℕg:Fin n.succ → ℚg':Fin n.succ → ℚf:Fin n.succ → ℚf':Fin n.succ → ℚh:Sum.elim g f = Sum.elim g' f'⊢ Pa g f = Pa g' f'refine_1n:ℕg:Fin n.succ → ℚg':Fin n.succ → ℚf:Fin n.succ → ℚf':Fin n.succ → ℚh:g = g' ∧ f = f'⊢ Pa g f = Pa g' f' Sum.elim_eq_iffrefine_1n:ℕg:Fin n.succ → ℚg':Fin n.succ → ℚf:Fin n.succ → ℚf':Fin n.succ → ℚh:g = g' ∧ f = f'⊢ Pa g f = Pa g' f'refine_1n:ℕg:Fin n.succ → ℚg':Fin n.succ → ℚf:Fin n.succ → ℚf':Fin n.succ → ℚh:g = g' ∧ f = f'⊢ Pa g f = Pa g' f'] at hrefine_1n:ℕg:Fin n.succ → ℚg':Fin n.succ → ℚf:Fin n.succ → ℚf':Fin n.succ → ℚh:g = g' ∧ f = f'⊢ Pa g f = Pa g' f'
    rw [h.left,refine_1n:ℕg:Fin n.succ → ℚg':Fin n.succ → ℚf:Fin n.succ → ℚf':Fin n.succ → ℚh:g = g' ∧ f = f'⊢ Pa g' f = Pa g' f'All goals completed! 🐙 h.rightrefine_1n:ℕg:Fin n.succ → ℚg':Fin n.succ → ℚf:Fin n.succ → ℚf':Fin n.succ → ℚh:g = g' ∧ f = f'⊢ Pa g' f' = Pa g' f'All goals completed! 🐙]All goals completed! 🐙
  ·refine_2n:ℕg:Fin n.succ → ℚg':Fin n.succ → ℚf:Fin n.succ → ℚf':Fin n.succ → ℚh:Pa g f = Pa g' f'⊢ Pa' (Sum.elim g f) = Pa' (Sum.elim g' f') apply ACCSystemLinear.LinSols.extrefine_2n:ℕg:Fin n.succ → ℚg':Fin n.succ → ℚf:Fin n.succ → ℚf':Fin n.succ → ℚh:Pa g f = Pa g' f'⊢ (Pa' (Sum.elim g f)).val = (Pa' (Sum.elim g' f')).val
    rw [Pa'_P'_P!',refine_2n:ℕg:Fin n.succ → ℚg':Fin n.succ → ℚf:Fin n.succ → ℚf':Fin n.succ → ℚh:Pa g f = Pa g' f'⊢ (Unshifted.planeLinSols (Sum.elim g f ∘ Sum.inl) + Shifted.planeLinSols (Sum.elim g f ∘ Sum.inr)).val =
  (Pa' (Sum.elim g' f')).valrefine_2n:ℕg:Fin n.succ → ℚg':Fin n.succ → ℚf:Fin n.succ → ℚf':Fin n.succ → ℚh:Pa g f = Pa g' f'⊢ (Unshifted.planeLinSols (Sum.elim g f ∘ Sum.inl) + Shifted.planeLinSols (Sum.elim g f ∘ Sum.inr)).val =
  (Unshifted.planeLinSols (Sum.elim g' f' ∘ Sum.inl) + Shifted.planeLinSols (Sum.elim g' f' ∘ Sum.inr)).val Pa'_P'_P!'refine_2n:ℕg:Fin n.succ → ℚg':Fin n.succ → ℚf:Fin n.succ → ℚf':Fin n.succ → ℚh:Pa g f = Pa g' f'⊢ (Unshifted.planeLinSols (Sum.elim g f ∘ Sum.inl) + Shifted.planeLinSols (Sum.elim g f ∘ Sum.inr)).val =
  (Unshifted.planeLinSols (Sum.elim g' f' ∘ Sum.inl) + Shifted.planeLinSols (Sum.elim g' f' ∘ Sum.inr)).valrefine_2n:ℕg:Fin n.succ → ℚg':Fin n.succ → ℚf:Fin n.succ → ℚf':Fin n.succ → ℚh:Pa g f = Pa g' f'⊢ (Unshifted.planeLinSols (Sum.elim g f ∘ Sum.inl) + Shifted.planeLinSols (Sum.elim g f ∘ Sum.inr)).val =
  (Unshifted.planeLinSols (Sum.elim g' f' ∘ Sum.inl) + Shifted.planeLinSols (Sum.elim g' f' ∘ Sum.inr)).val]refine_2n:ℕg:Fin n.succ → ℚg':Fin n.succ → ℚf:Fin n.succ → ℚf':Fin n.succ → ℚh:Pa g f = Pa g' f'⊢ (Unshifted.planeLinSols (Sum.elim g f ∘ Sum.inl) + Shifted.planeLinSols (Sum.elim g f ∘ Sum.inr)).val =
  (Unshifted.planeLinSols (Sum.elim g' f' ∘ Sum.inl) + Shifted.planeLinSols (Sum.elim g' f' ∘ Sum.inr)).val
    simp only [succ_eq_add_one, ACCSystemLinear.linSolsAddCommMonoid_add_val,
      Unshifted.planeLinSols_val, Shifted.planeLinSols_val]refine_2n:ℕg:Fin n.succ → ℚg':Fin n.succ → ℚf:Fin n.succ → ℚf':Fin n.succ → ℚh:Pa g f = Pa g' f'⊢ Unshifted.planeCharges (Sum.elim g f ∘ Sum.inl) + Shifted.planeCharges (Sum.elim g f ∘ Sum.inr) =
  Unshifted.planeCharges (Sum.elim g' f' ∘ Sum.inl) + Shifted.planeCharges (Sum.elim g' f' ∘ Sum.inr)
    exact hAll goals completed! 🐙

lemma Pa_eq (g g' : Fin n.succ → ℚ) (f f' : Fin n.succ → ℚ) :
    Pa g f = Pa g' f' ↔ g = g' ∧ f = f' := byn:ℕg:Fin n.succ → ℚg':Fin n.succ → ℚf:Fin n.succ → ℚf':Fin n.succ → ℚ⊢ Pa g f = Pa g' f' ↔ g = g' ∧ f = f'
  rw [← Pa'_elim_eq_iffn:ℕg:Fin n.succ → ℚg':Fin n.succ → ℚf:Fin n.succ → ℚf':Fin n.succ → ℚ⊢ Pa' (Sum.elim g f) = Pa' (Sum.elim g' f') ↔ g = g' ∧ f = f'n:ℕg:Fin n.succ → ℚg':Fin n.succ → ℚf:Fin n.succ → ℚf':Fin n.succ → ℚ⊢ Pa' (Sum.elim g f) = Pa' (Sum.elim g' f') ↔ g = g' ∧ f = f']n:ℕg:Fin n.succ → ℚg':Fin n.succ → ℚf:Fin n.succ → ℚf':Fin n.succ → ℚ⊢ Pa' (Sum.elim g f) = Pa' (Sum.elim g' f') ↔ g = g' ∧ f = f'
  rw [← Sum.elim_eq_iffn:ℕg:Fin n.succ → ℚg':Fin n.succ → ℚf:Fin n.succ → ℚf':Fin n.succ → ℚ⊢ Pa' (Sum.elim g f) = Pa' (Sum.elim g' f') ↔ Sum.elim g f = Sum.elim g' f'n:ℕg:Fin n.succ → ℚg':Fin n.succ → ℚf:Fin n.succ → ℚf':Fin n.succ → ℚ⊢ Pa' (Sum.elim g f) = Pa' (Sum.elim g' f') ↔ Sum.elim g f = Sum.elim g' f']n:ℕg:Fin n.succ → ℚg':Fin n.succ → ℚf:Fin n.succ → ℚf':Fin n.succ → ℚ⊢ Pa' (Sum.elim g f) = Pa' (Sum.elim g' f') ↔ Sum.elim g f = Sum.elim g' f'
  exact Pa'_eq _ _All goals completed! 🐙

E.8. Cardinality of the Unshifted.basis

lemma basisa_card : Fintype.card ((Fin n.succ) ⊕ (Fin n.succ)) =
    Module.finrank ℚ (PureU1 (2 * n.succ + 1)).LinSols := byn:ℕ⊢ Fintype.card (Fin n.succ ⊕ Fin n.succ) = finrank ℚ (PureU1 (2 * n.succ + 1)).LinSols
  erw [BasisLinear.finrank_AnomalyFreeLinearn:ℕ⊢ Fintype.card (Fin n.succ ⊕ Fin n.succ) = 2 * n.succ]n:ℕ⊢ Fintype.card (Fin n.succ ⊕ Fin n.succ) = 2 * n.succ
  simp [Fintype.card_sum, Fintype.card_fin, two_mul]All goals completed! 🐙

E.9. The Unshifted.basis vectors as a Unshifted.basis

F. Every Lienar solution is the sum of a point from each plane



lemma span_basis (S : (PureU1 (2 * n.succ + 1)).LinSols) :
    ∃ (g f : Fin n.succ → ℚ), S.val = Unshifted.planeCharges g + Shifted.planeCharges f := byn:ℕS:(PureU1 (2 * n.succ + 1)).LinSols⊢ ∃ g f, S.val = Unshifted.planeCharges g + Shifted.planeCharges f
  obtain ⟨f, hf⟩ :=
    (Submodule.mem_span_range_iff_exists_fun ℚ).mp (Basis.mem_span basisaAsBasis S)n:ℕS:(PureU1 (2 * n.succ + 1)).LinSolsf:Fin n.succ ⊕ Fin n.succ → ℚhf:∑ i, f i • basisaAsBasis i = S⊢ ∃ g f, S.val = Unshifted.planeCharges g + Shifted.planeCharges f
  simp only [succ_eq_add_one, basisaAsBasis, coe_basisOfLinearIndependentOfCardEqFinrank,
    Fintype.sum_sum_type] at hfn:ℕS:(PureU1 (2 * n.succ + 1)).LinSolsf:Fin n.succ ⊕ Fin n.succ → ℚhf:∑ a₁, f (Sum.inl a₁) • basisa (Sum.inl a₁) + ∑ a₂, f (Sum.inr a₂) • basisa (Sum.inr a₂) = S⊢ ∃ g f, S.val = Unshifted.planeCharges g + Shifted.planeCharges f
  change Unshifted.planeLinSols _ + Shifted.planeLinSols _ = S at hfn:ℕS:(PureU1 (2 * n.succ + 1)).LinSolsf:Fin n.succ ⊕ Fin n.succ → ℚhf:((Unshifted.planeLinSols fun i => f (Sum.inl i)) + Shifted.planeLinSols fun i => f (Sum.inr i)) = S⊢ ∃ g f, S.val = Unshifted.planeCharges g + Shifted.planeCharges f
  refine ⟨f ∘ Sum.inl, f ∘ Sum.inr, ?_⟩n:ℕS:(PureU1 (2 * n.succ + 1)).LinSolsf:Fin n.succ ⊕ Fin n.succ → ℚhf:((Unshifted.planeLinSols fun i => f (Sum.inl i)) + Shifted.planeLinSols fun i => f (Sum.inr i)) = S⊢ S.val = Unshifted.planeCharges (f ∘ Sum.inl) + Shifted.planeCharges (f ∘ Sum.inr)
  rw [← hfn:ℕS:(PureU1 (2 * n.succ + 1)).LinSolsf:Fin n.succ ⊕ Fin n.succ → ℚhf:((Unshifted.planeLinSols fun i => f (Sum.inl i)) + Shifted.planeLinSols fun i => f (Sum.inr i)) = S⊢ ((Unshifted.planeLinSols fun i => f (Sum.inl i)) + Shifted.planeLinSols fun i => f (Sum.inr i)).val =
  Unshifted.planeCharges (f ∘ Sum.inl) + Shifted.planeCharges (f ∘ Sum.inr)n:ℕS:(PureU1 (2 * n.succ + 1)).LinSolsf:Fin n.succ ⊕ Fin n.succ → ℚhf:((Unshifted.planeLinSols fun i => f (Sum.inl i)) + Shifted.planeLinSols fun i => f (Sum.inr i)) = S⊢ ((Unshifted.planeLinSols fun i => f (Sum.inl i)) + Shifted.planeLinSols fun i => f (Sum.inr i)).val =
  Unshifted.planeCharges (f ∘ Sum.inl) + Shifted.planeCharges (f ∘ Sum.inr)]n:ℕS:(PureU1 (2 * n.succ + 1)).LinSolsf:Fin n.succ ⊕ Fin n.succ → ℚhf:((Unshifted.planeLinSols fun i => f (Sum.inl i)) + Shifted.planeLinSols fun i => f (Sum.inr i)) = S⊢ ((Unshifted.planeLinSols fun i => f (Sum.inl i)) + Shifted.planeLinSols fun i => f (Sum.inr i)).val =
  Unshifted.planeCharges (f ∘ Sum.inl) + Shifted.planeCharges (f ∘ Sum.inr)
  simp only [succ_eq_add_one, ACCSystemLinear.linSolsAddCommMonoid_add_val,
    Unshifted.planeLinSols_val, Shifted.planeLinSols_val]n:ℕS:(PureU1 (2 * n.succ + 1)).LinSolsf:Fin n.succ ⊕ Fin n.succ → ℚhf:((Unshifted.planeLinSols fun i => f (Sum.inl i)) + Shifted.planeLinSols fun i => f (Sum.inr i)) = S⊢ ((Unshifted.planeCharges fun i => f (Sum.inl i)) + Shifted.planeCharges fun i => f (Sum.inr i)) =
  Unshifted.planeCharges (f ∘ Sum.inl) + Shifted.planeCharges (f ∘ Sum.inr)
  rflAll goals completed! 🐙

F.1. Relation under permutations



lemma span_basis_swap! {S : (PureU1 (2 * n.succ + 1)).LinSols} (j : Fin n.succ)
    (hS : ((FamilyPermutations (2 * n.succ + 1)).linSolRep
    (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S') (g f : Fin n.succ → ℚ)
    (hS1 : S.val = Unshifted.planeCharges g + Shifted.planeCharges f) : ∃ (g' f' : Fin n.succ → ℚ),
    S'.val = Unshifted.planeCharges g' + Shifted.planeCharges f' ∧
    Shifted.planeCharges f' = Shifted.planeCharges f +
    (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges j ∧ g' = g := byn:ℕS':(PureU1 (2 * n.succ + 1)).LinSolsS:(PureU1 (2 * n.succ + 1)).LinSolsj:Fin n.succhS:((FamilyPermutations (2 * n.succ + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'g:Fin n.succ → ℚf:Fin n.succ → ℚhS1:S.val = Unshifted.planeCharges g + Shifted.planeCharges f⊢ ∃ g' f',
  S'.val = Unshifted.planeCharges g' + Shifted.planeCharges f' ∧
    Shifted.planeCharges f' =
        Shifted.planeCharges f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges j ∧
      g' = g
  let X := Shifted.planeCharges f +
    (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges jn:ℕS':(PureU1 (2 * n.succ + 1)).LinSolsS:(PureU1 (2 * n.succ + 1)).LinSolsj:Fin n.succhS:((FamilyPermutations (2 * n.succ + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'g:Fin n.succ → ℚf:Fin n.succ → ℚhS1:S.val = Unshifted.planeCharges g + Shifted.planeCharges fX:(PureU1 (2 * n.succ + 1)).Charges := Shifted.planeCharges f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges j⊢ ∃ g' f',
  S'.val = Unshifted.planeCharges g' + Shifted.planeCharges f' ∧
    Shifted.planeCharges f' =
        Shifted.planeCharges f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges j ∧
      g' = g
  have hf : Shifted.planeCharges f ∈ Submodule.span ℚ (Set.range Shifted.basisAsCharges) :=
    (Submodule.mem_span_range_iff_exists_fun ℚ).mpr ⟨f, rfl⟩n:ℕS':(PureU1 (2 * n.succ + 1)).LinSolsS:(PureU1 (2 * n.succ + 1)).LinSolsj:Fin n.succhS:((FamilyPermutations (2 * n.succ + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'g:Fin n.succ → ℚf:Fin n.succ → ℚhS1:S.val = Unshifted.planeCharges g + Shifted.planeCharges fX:(PureU1 (2 * n.succ + 1)).Charges := Shifted.planeCharges f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges jhf:Shifted.planeCharges f ∈ Submodule.span ℚ (Set.range Shifted.basisAsCharges)⊢ ∃ g' f',
  S'.val = Unshifted.planeCharges g' + Shifted.planeCharges f' ∧
    Shifted.planeCharges f' =
        Shifted.planeCharges f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges j ∧
      g' = g
  have hP : (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges j ∈
      Submodule.span ℚ (Set.range Shifted.basisAsCharges) :=
    Submodule.smul_mem _ _ (Submodule.subset_span ⟨j, rfl⟩)n:ℕS':(PureU1 (2 * n.succ + 1)).LinSolsS:(PureU1 (2 * n.succ + 1)).LinSolsj:Fin n.succhS:((FamilyPermutations (2 * n.succ + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'g:Fin n.succ → ℚf:Fin n.succ → ℚhS1:S.val = Unshifted.planeCharges g + Shifted.planeCharges fX:(PureU1 (2 * n.succ + 1)).Charges := Shifted.planeCharges f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges jhf:Shifted.planeCharges f ∈ Submodule.span ℚ (Set.range Shifted.basisAsCharges)hP:(S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges j ∈
  Submodule.span ℚ (Set.range Shifted.basisAsCharges)⊢ ∃ g' f',
  S'.val = Unshifted.planeCharges g' + Shifted.planeCharges f' ∧
    Shifted.planeCharges f' =
        Shifted.planeCharges f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges j ∧
      g' = g
  have hX : X ∈ Submodule.span ℚ (Set.range (Shifted.basisAsCharges)) :=
    Submodule.add_mem _ hf hPn:ℕS':(PureU1 (2 * n.succ + 1)).LinSolsS:(PureU1 (2 * n.succ + 1)).LinSolsj:Fin n.succhS:((FamilyPermutations (2 * n.succ + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'g:Fin n.succ → ℚf:Fin n.succ → ℚhS1:S.val = Unshifted.planeCharges g + Shifted.planeCharges fX:(PureU1 (2 * n.succ + 1)).Charges := Shifted.planeCharges f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges jhf:Shifted.planeCharges f ∈ Submodule.span ℚ (Set.range Shifted.basisAsCharges)hP:(S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges j ∈
  Submodule.span ℚ (Set.range Shifted.basisAsCharges)hX:X ∈ Submodule.span ℚ (Set.range Shifted.basisAsCharges)⊢ ∃ g' f',
  S'.val = Unshifted.planeCharges g' + Shifted.planeCharges f' ∧
    Shifted.planeCharges f' =
        Shifted.planeCharges f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges j ∧
      g' = g
  obtain ⟨f', hf'⟩ := (Submodule.mem_span_range_iff_exists_fun ℚ).mp hXn:ℕS':(PureU1 (2 * n.succ + 1)).LinSolsS:(PureU1 (2 * n.succ + 1)).LinSolsj:Fin n.succhS:((FamilyPermutations (2 * n.succ + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'g:Fin n.succ → ℚf:Fin n.succ → ℚhS1:S.val = Unshifted.planeCharges g + Shifted.planeCharges fX:(PureU1 (2 * n.succ + 1)).Charges := Shifted.planeCharges f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges jhf:Shifted.planeCharges f ∈ Submodule.span ℚ (Set.range Shifted.basisAsCharges)hP:(S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges j ∈
  Submodule.span ℚ (Set.range Shifted.basisAsCharges)hX:X ∈ Submodule.span ℚ (Set.range Shifted.basisAsCharges)f':Fin n.succ → ℚhf':∑ i, f' i • Shifted.basisAsCharges i = X⊢ ∃ g' f',
  S'.val = Unshifted.planeCharges g' + Shifted.planeCharges f' ∧
    Shifted.planeCharges f' =
        Shifted.planeCharges f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges j ∧
      g' = g
  use g, f'hn:ℕS':(PureU1 (2 * n.succ + 1)).LinSolsS:(PureU1 (2 * n.succ + 1)).LinSolsj:Fin n.succhS:((FamilyPermutations (2 * n.succ + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'g:Fin n.succ → ℚf:Fin n.succ → ℚhS1:S.val = Unshifted.planeCharges g + Shifted.planeCharges fX:(PureU1 (2 * n.succ + 1)).Charges := Shifted.planeCharges f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges jhf:Shifted.planeCharges f ∈ Submodule.span ℚ (Set.range Shifted.basisAsCharges)hP:(S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges j ∈
  Submodule.span ℚ (Set.range Shifted.basisAsCharges)hX:X ∈ Submodule.span ℚ (Set.range Shifted.basisAsCharges)f':Fin n.succ → ℚhf':∑ i, f' i • Shifted.basisAsCharges i = X⊢ S'.val = Unshifted.planeCharges g + Shifted.planeCharges f' ∧
  Shifted.planeCharges f' =
      Shifted.planeCharges f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges j ∧
    g = g
  change Shifted.planeCharges f' = _ at hf'hn:ℕS':(PureU1 (2 * n.succ + 1)).LinSolsS:(PureU1 (2 * n.succ + 1)).LinSolsj:Fin n.succhS:((FamilyPermutations (2 * n.succ + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'g:Fin n.succ → ℚf:Fin n.succ → ℚhS1:S.val = Unshifted.planeCharges g + Shifted.planeCharges fX:(PureU1 (2 * n.succ + 1)).Charges := Shifted.planeCharges f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges jhf:Shifted.planeCharges f ∈ Submodule.span ℚ (Set.range Shifted.basisAsCharges)hP:(S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges j ∈
  Submodule.span ℚ (Set.range Shifted.basisAsCharges)hX:X ∈ Submodule.span ℚ (Set.range Shifted.basisAsCharges)f':Fin n.succ → ℚhf':Shifted.planeCharges f' = X⊢ S'.val = Unshifted.planeCharges g + Shifted.planeCharges f' ∧
  Shifted.planeCharges f' =
      Shifted.planeCharges f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges j ∧
    g = g
  erw [hf'hn:ℕS':(PureU1 (2 * n.succ + 1)).LinSolsS:(PureU1 (2 * n.succ + 1)).LinSolsj:Fin n.succhS:((FamilyPermutations (2 * n.succ + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'g:Fin n.succ → ℚf:Fin n.succ → ℚhS1:S.val = Unshifted.planeCharges g + Shifted.planeCharges fX:(PureU1 (2 * n.succ + 1)).Charges := Shifted.planeCharges f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges jhf:Shifted.planeCharges f ∈ Submodule.span ℚ (Set.range Shifted.basisAsCharges)hP:(S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges j ∈
  Submodule.span ℚ (Set.range Shifted.basisAsCharges)hX:X ∈ Submodule.span ℚ (Set.range Shifted.basisAsCharges)f':Fin n.succ → ℚhf':Shifted.planeCharges f' = X⊢ S'.val = Unshifted.planeCharges g + X ∧
  X = Shifted.planeCharges f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges j ∧ g = g]hn:ℕS':(PureU1 (2 * n.succ + 1)).LinSolsS:(PureU1 (2 * n.succ + 1)).LinSolsj:Fin n.succhS:((FamilyPermutations (2 * n.succ + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'g:Fin n.succ → ℚf:Fin n.succ → ℚhS1:S.val = Unshifted.planeCharges g + Shifted.planeCharges fX:(PureU1 (2 * n.succ + 1)).Charges := Shifted.planeCharges f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges jhf:Shifted.planeCharges f ∈ Submodule.span ℚ (Set.range Shifted.basisAsCharges)hP:(S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges j ∈
  Submodule.span ℚ (Set.range Shifted.basisAsCharges)hX:X ∈ Submodule.span ℚ (Set.range Shifted.basisAsCharges)f':Fin n.succ → ℚhf':Shifted.planeCharges f' = X⊢ S'.val = Unshifted.planeCharges g + X ∧
  X = Shifted.planeCharges f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges j ∧ g = g
  simp only [and_self, and_true, X]hn:ℕS':(PureU1 (2 * n.succ + 1)).LinSolsS:(PureU1 (2 * n.succ + 1)).LinSolsj:Fin n.succhS:((FamilyPermutations (2 * n.succ + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'g:Fin n.succ → ℚf:Fin n.succ → ℚhS1:S.val = Unshifted.planeCharges g + Shifted.planeCharges fX:(PureU1 (2 * n.succ + 1)).Charges := Shifted.planeCharges f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges jhf:Shifted.planeCharges f ∈ Submodule.span ℚ (Set.range Shifted.basisAsCharges)hP:(S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges j ∈
  Submodule.span ℚ (Set.range Shifted.basisAsCharges)hX:X ∈ Submodule.span ℚ (Set.range Shifted.basisAsCharges)f':Fin n.succ → ℚhf':Shifted.planeCharges f' = X⊢ S'.val =
  Unshifted.planeCharges g +
    (Shifted.planeCharges f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges j)
  rw [← add_assoc,hn:ℕS':(PureU1 (2 * n.succ + 1)).LinSolsS:(PureU1 (2 * n.succ + 1)).LinSolsj:Fin n.succhS:((FamilyPermutations (2 * n.succ + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'g:Fin n.succ → ℚf:Fin n.succ → ℚhS1:S.val = Unshifted.planeCharges g + Shifted.planeCharges fX:(PureU1 (2 * n.succ + 1)).Charges := Shifted.planeCharges f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges jhf:Shifted.planeCharges f ∈ Submodule.span ℚ (Set.range Shifted.basisAsCharges)hP:(S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges j ∈
  Submodule.span ℚ (Set.range Shifted.basisAsCharges)hX:X ∈ Submodule.span ℚ (Set.range Shifted.basisAsCharges)f':Fin n.succ → ℚhf':Shifted.planeCharges f' = X⊢ S'.val =
  Unshifted.planeCharges g + Shifted.planeCharges f +
    (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges jhn:ℕS':(PureU1 (2 * n.succ + 1)).LinSolsS:(PureU1 (2 * n.succ + 1)).LinSolsj:Fin n.succhS:((FamilyPermutations (2 * n.succ + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'g:Fin n.succ → ℚf:Fin n.succ → ℚhS1:S.val = Unshifted.planeCharges g + Shifted.planeCharges fX:(PureU1 (2 * n.succ + 1)).Charges := Shifted.planeCharges f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges jhf:Shifted.planeCharges f ∈ Submodule.span ℚ (Set.range Shifted.basisAsCharges)hP:(S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges j ∈
  Submodule.span ℚ (Set.range Shifted.basisAsCharges)hX:X ∈ Submodule.span ℚ (Set.range Shifted.basisAsCharges)f':Fin n.succ → ℚhf':Shifted.planeCharges f' = X⊢ S'.val = S.val + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges j ← hS1hn:ℕS':(PureU1 (2 * n.succ + 1)).LinSolsS:(PureU1 (2 * n.succ + 1)).LinSolsj:Fin n.succhS:((FamilyPermutations (2 * n.succ + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'g:Fin n.succ → ℚf:Fin n.succ → ℚhS1:S.val = Unshifted.planeCharges g + Shifted.planeCharges fX:(PureU1 (2 * n.succ + 1)).Charges := Shifted.planeCharges f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges jhf:Shifted.planeCharges f ∈ Submodule.span ℚ (Set.range Shifted.basisAsCharges)hP:(S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges j ∈
  Submodule.span ℚ (Set.range Shifted.basisAsCharges)hX:X ∈ Submodule.span ℚ (Set.range Shifted.basisAsCharges)f':Fin n.succ → ℚhf':Shifted.planeCharges f' = X⊢ S'.val = S.val + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges jhn:ℕS':(PureU1 (2 * n.succ + 1)).LinSolsS:(PureU1 (2 * n.succ + 1)).LinSolsj:Fin n.succhS:((FamilyPermutations (2 * n.succ + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'g:Fin n.succ → ℚf:Fin n.succ → ℚhS1:S.val = Unshifted.planeCharges g + Shifted.planeCharges fX:(PureU1 (2 * n.succ + 1)).Charges := Shifted.planeCharges f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges jhf:Shifted.planeCharges f ∈ Submodule.span ℚ (Set.range Shifted.basisAsCharges)hP:(S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges j ∈
  Submodule.span ℚ (Set.range Shifted.basisAsCharges)hX:X ∈ Submodule.span ℚ (Set.range Shifted.basisAsCharges)f':Fin n.succ → ℚhf':Shifted.planeCharges f' = X⊢ S'.val = S.val + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges j]hn:ℕS':(PureU1 (2 * n.succ + 1)).LinSolsS:(PureU1 (2 * n.succ + 1)).LinSolsj:Fin n.succhS:((FamilyPermutations (2 * n.succ + 1)).linSolRep (Equiv.swap (oddShiftFst j) (oddShiftSnd j))) S = S'g:Fin n.succ → ℚf:Fin n.succ → ℚhS1:S.val = Unshifted.planeCharges g + Shifted.planeCharges fX:(PureU1 (2 * n.succ + 1)).Charges := Shifted.planeCharges f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges jhf:Shifted.planeCharges f ∈ Submodule.span ℚ (Set.range Shifted.basisAsCharges)hP:(S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges j ∈
  Submodule.span ℚ (Set.range Shifted.basisAsCharges)hX:X ∈ Submodule.span ℚ (Set.range Shifted.basisAsCharges)f':Fin n.succ → ℚhf':Shifted.planeCharges f' = X⊢ S'.val = S.val + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges j
  apply Shifted.swap_as_add at hShn:ℕS':(PureU1 (2 * n.succ + 1)).LinSolsS:(PureU1 (2 * n.succ + 1)).LinSolsj:Fin n.succg:Fin n.succ → ℚf:Fin n.succ → ℚhS1:S.val = Unshifted.planeCharges g + Shifted.planeCharges fX:(PureU1 (2 * n.succ + 1)).Charges := Shifted.planeCharges f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges jhf:Shifted.planeCharges f ∈ Submodule.span ℚ (Set.range Shifted.basisAsCharges)hP:(S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges j ∈
  Submodule.span ℚ (Set.range Shifted.basisAsCharges)hX:X ∈ Submodule.span ℚ (Set.range Shifted.basisAsCharges)f':Fin n.succ → ℚhf':Shifted.planeCharges f' = XhS:S'.val = S.val + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges j⊢ S'.val = S.val + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • Shifted.basisAsCharges j
  exact hSAll goals completed! 🐙

Splitting the linear solutions in the odd case into two ACC-satisfying planes

i. Overview

ii. Key results

iii. Table of contents

iv. References

A. Splitting the charges up into groups

A.1. The symmetric split: Spltting the charges up via (n + 1) + 1

A.2. The shifted split: Spltting the charges up via 1 + n + n

A.3. The shifted shifted split: Spltting the charges up via ((1+n)+1) + n.succ

A.4. Relating the splittings together

B. The unshifted plane

B.1. The basis vectors of the unshifted plane as charges

B.2. Components of the basis vectors as charges

B.3. The basis vectors satisfy the linear ACCs

B.4. The basis vectors as LinSols

B.5. The inclusion of the unshifted plane into charges

B.6. Components of the unshifted plane

B.7. Points on the unshifted plane satisfies the ACCs

B.8. Kernel of the inclusion into charges

B.9. The basis vectors are linearly independent

C. The shifted plane

C.1. The basis vectors of the shifted plane as charges

C.2. Components of the basis vectors as charges

C.3. The basis vectors satisfy the linear ACCs

C.4. The basis vectors as LinSols

C.5. Permutations equal adding basis vectors

C.6. The inclusion of the shifted plane into charges

C.7. Components of the shifted plane

C.8. Points on the shifted plane satisfies the ACCs

C.9. Kernel of the inclusion into charges

C.10. The inclusion of the shifted plane into LinSols

C.11. The basis vectors are linearly independent

D. The mixed cubic ACC from points in both planes

E. The combined Unshifted.basis

E.1. The combined Unshifted.basis as LinSols

E.2. The inclusion of the span of the combined Unshifted.basis into charges

E.3. Components of the inclusion

E.4. Kernel of the inclusion into charges

E.5. The inclusion of the span of the combined Unshifted.basis into LinSols

E.6. The combined Unshifted.basis vectors are linearly independent

E.7. Injectivity of the inclusion into linear solutions

E.8. Cardinality of the Unshifted.basis

E.9. The Unshifted.basis vectors as a Unshifted.basis

F. Every Lienar solution is the sum of a point from each plane

F.1. Relation under permutations

A.1. The symmetric split: Spltting the charges up via `(n + 1) + 1`

A.2. The shifted split: Spltting the charges up via `1 + n + n`

A.3. The shifted shifted split: Spltting the charges up via `((1+n)+1) + n.succ`

B.4. The basis vectors as `LinSols`

C.4. The basis vectors as `LinSols`

E.1. The combined Unshifted.basis as `LinSols`