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

P' : The inclusion of the first plane into linear solutions

P_accCube : The statement that chares from the first plane satisfy the cubic ACC

P!' : The inclusion of the second plane.

P!_accCube : The statement that charges from the second 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 first plane

B.1. The basis vectors of the first 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 first plane into charges

B.6. Components of the first plane

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

B.8. Kernel of the inclusion into charges

B.9. The basis vectors are linearly independent

C. The second plane

C.1. The basis vectors of the second 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 second plane into charges

C.7. Components of the second plane

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

C.9. Kernel of the inclusion into charges

C.10. The inclusion of the second 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 first plane

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

The first 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 first 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 first plane into charges

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

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

B.6. Components of the first plane

              

lemma P_oddFst (f : Fin n → ℚ) (j : Fin n) : P f (oddFst j) = f j := byn:ℕf:Fin n → ℚj:Fin n⊢ P f (oddFst j) = f j
  rw [P,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 P_oddSnd (f : Fin n → ℚ) (j : Fin n) : P f (oddSnd j) = - f j := byn:ℕf:Fin n → ℚj:Fin n⊢ P f (oddSnd j) = -f j
  rw [P,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 P_oddMid (f : Fin n → ℚ) : P f oddMid = 0 := byn:ℕf:Fin n → ℚ⊢ P f oddMid = 0
  rw [P,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 first plane satisfies the ACCs



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



lemma P_accCube (f : Fin n → ℚ) : accCube (2 * n +1) (P f) = 0 := byn:ℕf:Fin n → ℚ⊢ (accCube (2 * n + 1)) (P f) = 0
  rw [accCube_explicit,n:ℕf:Fin n → ℚ⊢ ∑ i, P f i ^ 3 = 0n:ℕf:Fin n → ℚ⊢ 0 ^ 3 + ∑ i, (((fun i => P f i ^ 3) ∘ oddFst) i + ((fun i => P f i ^ 3) ∘ oddSnd) i) = 0 sum_odd,n:ℕf:Fin n → ℚ⊢ P f oddMid ^ 3 + ∑ i, (((fun i => P f i ^ 3) ∘ oddFst) i + ((fun i => P f i ^ 3) ∘ oddSnd) i) = 0n:ℕf:Fin n → ℚ⊢ 0 ^ 3 + ∑ i, (((fun i => P f i ^ 3) ∘ oddFst) i + ((fun i => P f i ^ 3) ∘ oddSnd) i) = 0 P_oddMidn:ℕf:Fin n → ℚ⊢ 0 ^ 3 + ∑ i, (((fun i => P f i ^ 3) ∘ oddFst) i + ((fun i => P f i ^ 3) ∘ oddSnd) i) = 0n:ℕf:Fin n → ℚ⊢ 0 ^ 3 + ∑ i, (((fun i => P f i ^ 3) ∘ oddFst) i + ((fun i => P f i ^ 3) ∘ oddSnd) i) = 0]n:ℕf:Fin n → ℚ⊢ 0 ^ 3 + ∑ i, (((fun i => P f i ^ 3) ∘ oddFst) i + ((fun i => P 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, (P f (oddFst x) ^ 3 + P f (oddSnd x) ^ 3) = 0
  refine Finset.sum_eq_zero fun i _ => ?_n:ℕf:Fin n → ℚi:Fin nx✝:i ∈ univ⊢ P f (oddFst i) ^ 3 + P f (oddSnd i) ^ 3 = 0
  simp only [P_oddFst, P_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 P_zero (f : Fin n → ℚ) (h : P f = 0) : ∀ i, f i = 0 :=
  fun i => (P_oddFst f i).symm.trans (congr_fun h (oddFst i))

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

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



lemma P'_val (f : Fin n → ℚ) : (P' f).val = P f := byn:ℕf:Fin n → ℚ⊢ (P' f).val = P f
  simp only [P', P]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 P' f = 0 at hn:ℕf:Fin n → ℚh:P' f = 0⊢ ∀ (i : Fin n), f i = 0
  exact P_zero f (P'_val f ▸ congrArg ACCSystemLinear.LinSols.val h)All goals completed! 🐙

C. The second plane

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

The second part of the basis as charge assignments.

def basis!AsCharges (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) : basis!AsCharges j (oddShiftFst j) = 1 := byn:ℕj:Fin n⊢ basis!AsCharges j (oddShiftFst j) = 1
  simp [basis!AsCharges]All goals completed! 🐙set_option backward.isDefEq.respectTransparency false in
lemma basis!_on_oddShiftFst_other {k j : Fin n} (h : k ≠ j) :
    basis!AsCharges k (oddShiftFst j) = 0 := byn:ℕk:Fin nj:Fin nh:k ≠ j⊢ basis!AsCharges k (oddShiftFst j) = 0
  have hk : (k : ℕ) ≠ (j : ℕ) := fun he => h (Fin.ext he)n:ℕk:Fin nj:Fin nh:k ≠ jhk:↑k ≠ ↑j⊢ basis!AsCharges k (oddShiftFst j) = 0
  simp only [basis!AsCharges, 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) :
    basis!AsCharges k j = 0 := byn:ℕk:Fin nj:Fin (2 * n + 1)h1:j ≠ oddShiftFst kh2:j ≠ oddShiftSnd k⊢ basis!AsCharges k j = 0
  simp only [basis!AsCharges, h1, h2, ↓reduceIte]All goals completed! 🐙set_option backward.isDefEq.respectTransparency false in
lemma basis!_oddShiftSnd_eq_minus_oddShiftFst (j i : Fin n) :
    basis!AsCharges j (oddShiftSnd i) = - basis!AsCharges j (oddShiftFst i) := byn:ℕj:Fin ni:Fin n⊢ basis!AsCharges j (oddShiftSnd i) = -basis!AsCharges j (oddShiftFst i)
  simp only [basis!AsCharges, 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) : basis!AsCharges j (oddShiftSnd j) = - 1 := byn:ℕj:Fin n⊢ basis!AsCharges j (oddShiftSnd j) = -1
  rw [basis!_oddShiftSnd_eq_minus_oddShiftFst,n:ℕj:Fin n⊢ -basis!AsCharges 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) :
    basis!AsCharges k (oddShiftSnd j) = 0 := byn:ℕk:Fin nj:Fin nh:k ≠ j⊢ basis!AsCharges k (oddShiftSnd j) = 0
  rw [basis!_oddShiftSnd_eq_minus_oddShiftFst,n:ℕk:Fin nj:Fin nh:k ≠ j⊢ -basis!AsCharges 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) : basis!AsCharges j oddShiftZero = 0 := byn:ℕj:Fin n⊢ basis!AsCharges j oddShiftZero = 0
  simp only [basis!AsCharges, 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)) (basis!AsCharges j) = 0 := byn:ℕj:Fin n⊢ (accGrav (2 * n + 1)) (basis!AsCharges j) = 0
  rw [accGravn:ℕj:Fin n⊢ { toFun := fun S => ∑ i, S i, map_add' := ⋯, map_smul' := ⋯ } (basis!AsCharges j) = 0n:ℕj:Fin n⊢ { toFun := fun S => ∑ i, S i, map_add' := ⋯, map_smul' := ⋯ } (basis!AsCharges j) = 0]n:ℕj:Fin n⊢ { toFun := fun S => ∑ i, S i, map_add' := ⋯, map_smul' := ⋯ } (basis!AsCharges j) = 0
  simp [sum_oddShift, basis!_on_oddShiftZero, basis!_oddShiftSnd_eq_minus_oddShiftFst]All goals completed! 🐙

C.4. The basis vectors as `LinSols`

The second part of the basis as LinSols.

@[simps!]
def basis! (j : Fin n) : (PureU1 (2 * n + 1)).LinSols :=
  ⟨basis!AsCharges j, byn:ℕj:Fin n⊢ ∀ (i : Fin (PureU1 (2 * n + 1)).numberLinear), ((PureU1 (2 * n + 1)).linearACCs i) (basis!AsCharges j) = 0
    intro in:ℕj:Fin ni:Fin (PureU1 (2 * n + 1)).numberLinear⊢ ((PureU1 (2 * n + 1)).linearACCs i) (basis!AsCharges 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✝⟩) (basis!AsCharges 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 basis!AsCharges 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)) • basis!AsCharges 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)) • basis!AsCharges 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)) • basis!AsCharges 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)) • basis!AsCharges 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)) • basis!AsCharges 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)) • basis!AsCharges 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)) • basis!AsCharges 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)) • basis!AsCharges 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)) • basis!AsCharges 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)) • basis!AsCharges 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)) • basis!AsCharges 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)) • basis!AsCharges 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)) • basis!AsCharges 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)) • basis!AsCharges 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)) • basis!AsCharges 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)) • basis!AsCharges 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)) • basis!AsCharges 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)) • basis!AsCharges 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)) * basis!AsCharges 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 second plane into charges

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

def P! (f : Fin n → ℚ) : (PureU1 (2 * n + 1)).Charges := ∑ i, f i • basis!AsCharges i

C.7. Components of the second plane

              

lemma P!_oddShiftFst (f : Fin n → ℚ) (j : Fin n) : P! f (oddShiftFst j) = f j := byn:ℕf:Fin n → ℚj:Fin n⊢ P! f (oddShiftFst j) = f j
  rw [P!,n:ℕf:Fin n → ℚj:Fin n⊢ (∑ i, f i • basis!AsCharges i) (oddShiftFst j) = f jn:ℕf:Fin n → ℚj:Fin n⊢ ∑ i, (f i • basis!AsCharges i) (oddShiftFst j) = f j sum_of_chargesn:ℕf:Fin n → ℚj:Fin n⊢ ∑ i, (f i • basis!AsCharges i) (oddShiftFst j) = f jn:ℕf:Fin n → ℚj:Fin n⊢ ∑ i, (f i • basis!AsCharges i) (oddShiftFst j) = f j]n:ℕf:Fin n → ℚj:Fin n⊢ ∑ i, (f i • basis!AsCharges i) (oddShiftFst j) = f j
  simp only [HSMul.hSMul, SMul.smul]n:ℕf:Fin n → ℚj:Fin n⊢ ∑ x, f x * basis!AsCharges x (oddShiftFst j) = f j
  rw [Fintype.sum_eq_single jn:ℕf:Fin n → ℚj:Fin n⊢ f j * basis!AsCharges j (oddShiftFst j) = f jn:ℕf:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n), x ≠ j → f x * basis!AsCharges x (oddShiftFst j) = 0n:ℕf:Fin n → ℚj:Fin n⊢ f j * basis!AsCharges j (oddShiftFst j) = f jn:ℕf:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n), x ≠ j → f x * basis!AsCharges x (oddShiftFst j) = 0]n:ℕf:Fin n → ℚj:Fin n⊢ f j * basis!AsCharges j (oddShiftFst j) = f jn:ℕf:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n), x ≠ j → f x * basis!AsCharges x (oddShiftFst j) = 0
  ·n:ℕf:Fin n → ℚj:Fin n⊢ f j * basis!AsCharges 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 * basis!AsCharges x (oddShiftFst j) = 0 intro k hkjn:ℕf:Fin n → ℚj:Fin nk:Fin nhkj:k ≠ j⊢ f k * basis!AsCharges k (oddShiftFst j) = 0
    exact mul_eq_zero_of_right (f k) (basis!_on_oddShiftFst_other hkj)All goals completed! 🐙

lemma P!_oddShiftSnd (f : Fin n → ℚ) (j : Fin n) : P! f (oddShiftSnd j) = - f j := byn:ℕf:Fin n → ℚj:Fin n⊢ P! f (oddShiftSnd j) = -f j
  rw [P!,n:ℕf:Fin n → ℚj:Fin n⊢ (∑ i, f i • basis!AsCharges i) (oddShiftSnd j) = -f jn:ℕf:Fin n → ℚj:Fin n⊢ ∑ i, (f i • basis!AsCharges i) (oddShiftSnd j) = -f j sum_of_chargesn:ℕf:Fin n → ℚj:Fin n⊢ ∑ i, (f i • basis!AsCharges i) (oddShiftSnd j) = -f jn:ℕf:Fin n → ℚj:Fin n⊢ ∑ i, (f i • basis!AsCharges i) (oddShiftSnd j) = -f j]n:ℕf:Fin n → ℚj:Fin n⊢ ∑ i, (f i • basis!AsCharges i) (oddShiftSnd j) = -f j
  simp only [HSMul.hSMul, SMul.smul]n:ℕf:Fin n → ℚj:Fin n⊢ ∑ x, f x * basis!AsCharges x (oddShiftSnd j) = -f j
  rw [Fintype.sum_eq_single jn:ℕf:Fin n → ℚj:Fin n⊢ f j * basis!AsCharges j (oddShiftSnd j) = -f jn:ℕf:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n), x ≠ j → f x * basis!AsCharges x (oddShiftSnd j) = 0n:ℕf:Fin n → ℚj:Fin n⊢ f j * basis!AsCharges j (oddShiftSnd j) = -f jn:ℕf:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n), x ≠ j → f x * basis!AsCharges x (oddShiftSnd j) = 0]n:ℕf:Fin n → ℚj:Fin n⊢ f j * basis!AsCharges j (oddShiftSnd j) = -f jn:ℕf:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n), x ≠ j → f x * basis!AsCharges x (oddShiftSnd j) = 0
  ·n:ℕf:Fin n → ℚj:Fin n⊢ f j * basis!AsCharges 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 * basis!AsCharges x (oddShiftSnd j) = 0 intro k hkjn:ℕf:Fin n → ℚj:Fin nk:Fin nhkj:k ≠ j⊢ f k * basis!AsCharges k (oddShiftSnd j) = 0
    exact mul_eq_zero_of_right (f k) (basis!_on_oddShiftSnd_other hkj)All goals completed! 🐙

lemma P!_oddShiftZero (f : Fin n → ℚ) : P! f oddShiftZero = 0 := byn:ℕf:Fin n → ℚ⊢ P! f oddShiftZero = 0
  rw [P!,n:ℕf:Fin n → ℚ⊢ (∑ i, f i • basis!AsCharges i) oddShiftZero = 0n:ℕf:Fin n → ℚ⊢ ∑ i, (f i • basis!AsCharges i) oddShiftZero = 0 sum_of_chargesn:ℕf:Fin n → ℚ⊢ ∑ i, (f i • basis!AsCharges i) oddShiftZero = 0n:ℕf:Fin n → ℚ⊢ ∑ i, (f i • basis!AsCharges i) oddShiftZero = 0]n:ℕf:Fin n → ℚ⊢ ∑ i, (f i • basis!AsCharges i) oddShiftZero = 0
  simp [HSMul.hSMul, SMul.smul, basis!_on_oddShiftZero]All goals completed! 🐙

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



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



lemma P!_accCube (f : Fin n → ℚ) : accCube (2 * n +1) (P! f) = 0 := byn:ℕf:Fin n → ℚ⊢ (accCube (2 * n + 1)) (P! f) = 0
  rw [accCube_explicit,n:ℕf:Fin n → ℚ⊢ ∑ i, P! f i ^ 3 = 0n:ℕf:Fin n → ℚ⊢ 0 ^ 3 + ∑ i, (((fun i => P! f i ^ 3) ∘ oddShiftFst) i + ((fun i => P! f i ^ 3) ∘ oddShiftSnd) i) = 0 sum_oddShift,n:ℕf:Fin n → ℚ⊢ P! f oddShiftZero ^ 3 + ∑ i, (((fun i => P! f i ^ 3) ∘ oddShiftFst) i + ((fun i => P! f i ^ 3) ∘ oddShiftSnd) i) = 0n:ℕf:Fin n → ℚ⊢ 0 ^ 3 + ∑ i, (((fun i => P! f i ^ 3) ∘ oddShiftFst) i + ((fun i => P! f i ^ 3) ∘ oddShiftSnd) i) = 0 P!_oddShiftZeron:ℕf:Fin n → ℚ⊢ 0 ^ 3 + ∑ i, (((fun i => P! f i ^ 3) ∘ oddShiftFst) i + ((fun i => P! f i ^ 3) ∘ oddShiftSnd) i) = 0n:ℕf:Fin n → ℚ⊢ 0 ^ 3 + ∑ i, (((fun i => P! f i ^ 3) ∘ oddShiftFst) i + ((fun i => P! f i ^ 3) ∘ oddShiftSnd) i) = 0]n:ℕf:Fin n → ℚ⊢ 0 ^ 3 + ∑ i, (((fun i => P! f i ^ 3) ∘ oddShiftFst) i + ((fun i => P! 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, (P! f (oddShiftFst x) ^ 3 + P! f (oddShiftSnd x) ^ 3) = 0
  refine Finset.sum_eq_zero fun i _ => ?_n:ℕf:Fin n → ℚi:Fin nx✝:i ∈ univ⊢ P! f (oddShiftFst i) ^ 3 + P! f (oddShiftSnd i) ^ 3 = 0
  simp only [P!_oddShiftFst, P!_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 P!_zero (f : Fin n → ℚ) (h : P! f = 0) : ∀ i, f i = 0 :=
  fun i => (P!_oddShiftFst f i).symm.trans (congr_fun h (oddShiftFst i))

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

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

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



lemma P!'_val (f : Fin n → ℚ) : (P!' f).val = P! f := byn:ℕf:Fin n → ℚ⊢ (P!' f).val = P! f
  simp only [P!', P!]n:ℕf:Fin n → ℚ⊢ (∑ i, f i • basis! i).val = ∑ i, f i • basis!AsCharges i
  funext in:ℕf:Fin n → ℚi:Fin (PureU1 (2 * n + 1)).numberCharges⊢ (∑ i, f i • basis! i).val i = (∑ i, f i • basis!AsCharges 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 • basis!AsCharges 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 • basis!AsCharges 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 • basis!AsCharges 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 • basis!AsCharges 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 • basis!AsCharges 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 P!' f = 0 at hn:ℕf:Fin n → ℚh:P!' f = 0⊢ ∀ (i : Fin n), f i = 0
  exact P!_zero f (P!'_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 (P g) (P g) (basis!AsCharges j)
    = (P g (oddShiftFst j))^2 - (g j)^2 := byn:ℕg:Fin n → ℚj:Fin n⊢ ((accCubeTriLinSymm (P g)) (P g)) (basis!AsCharges j) = P g (oddShiftFst j) ^ 2 - g j ^ 2
  simp only [accCubeTriLinSymm, TriLinearSymm.mk₃_toFun_apply_apply]n:ℕg:Fin n → ℚj:Fin n⊢ ∑ x, P g x * P g x * basis!AsCharges j x = P g (oddShiftFst j) ^ 2 - g j ^ 2
  erw [sum_oddShift,n:ℕg:Fin n → ℚj:Fin n⊢ P g oddShiftZero * P g oddShiftZero * basis!AsCharges j oddShiftZero +
    ∑ i,
      (((fun x => P g x * P g x * basis!AsCharges j x) ∘ oddShiftFst) i +
        ((fun x => P g x * P g x * basis!AsCharges j x) ∘ oddShiftSnd) i) =
  P g (oddShiftFst j) ^ 2 - g j ^ 2 basis!_on_oddShiftZeron:ℕg:Fin n → ℚj:Fin n⊢ P g oddShiftZero * P g oddShiftZero * 0 +
    ∑ i,
      (((fun x => P g x * P g x * basis!AsCharges j x) ∘ oddShiftFst) i +
        ((fun x => P g x * P g x * basis!AsCharges j x) ∘ oddShiftSnd) i) =
  P g (oddShiftFst j) ^ 2 - g j ^ 2]n:ℕg:Fin n → ℚj:Fin n⊢ P g oddShiftZero * P g oddShiftZero * 0 +
    ∑ i,
      (((fun x => P g x * P g x * basis!AsCharges j x) ∘ oddShiftFst) i +
        ((fun x => P g x * P g x * basis!AsCharges j x) ∘ oddShiftSnd) i) =
  P g (oddShiftFst j) ^ 2 - g j ^ 2
  simp only [mul_zero, Function.comp_apply, zero_add]n:ℕg:Fin n → ℚj:Fin n⊢ ∑ x,
    (P g (oddShiftFst x) * P g (oddShiftFst x) * basis!AsCharges j (oddShiftFst x) +
      P g (oddShiftSnd x) * P g (oddShiftSnd x) * basis!AsCharges j (oddShiftSnd x)) =
  P g (oddShiftFst j) ^ 2 - g j ^ 2
  rw [Fintype.sum_eq_single j,n:ℕg:Fin n → ℚj:Fin n⊢ P g (oddShiftFst j) * P g (oddShiftFst j) * basis!AsCharges j (oddShiftFst j) +
    P g (oddShiftSnd j) * P g (oddShiftSnd j) * basis!AsCharges j (oddShiftSnd j) =
  P g (oddShiftFst j) ^ 2 - g j ^ 2n:ℕg:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n),
  x ≠ j →
    P g (oddShiftFst x) * P g (oddShiftFst x) * basis!AsCharges j (oddShiftFst x) +
        P g (oddShiftSnd x) * P g (oddShiftSnd x) * basis!AsCharges j (oddShiftSnd x) =
      0n:ℕg:Fin n → ℚj:Fin n⊢ P g (oddShiftFst j) * P g (oddShiftFst j) * 1 + P g (oddShiftSnd j) * P g (oddShiftSnd j) * -1 =
  P g (oddShiftFst j) ^ 2 - g j ^ 2n:ℕg:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n),
  x ≠ j →
    P g (oddShiftFst x) * P g (oddShiftFst x) * basis!AsCharges j (oddShiftFst x) +
        P g (oddShiftSnd x) * P g (oddShiftSnd x) * basis!AsCharges j (oddShiftSnd x) =
      0 basis!_on_oddShiftFst_self,n:ℕg:Fin n → ℚj:Fin n⊢ P g (oddShiftFst j) * P g (oddShiftFst j) * 1 +
    P g (oddShiftSnd j) * P g (oddShiftSnd j) * basis!AsCharges j (oddShiftSnd j) =
  P g (oddShiftFst j) ^ 2 - g j ^ 2n:ℕg:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n),
  x ≠ j →
    P g (oddShiftFst x) * P g (oddShiftFst x) * basis!AsCharges j (oddShiftFst x) +
        P g (oddShiftSnd x) * P g (oddShiftSnd x) * basis!AsCharges j (oddShiftSnd x) =
      0n:ℕg:Fin n → ℚj:Fin n⊢ P g (oddShiftFst j) * P g (oddShiftFst j) * 1 + P g (oddShiftSnd j) * P g (oddShiftSnd j) * -1 =
  P g (oddShiftFst j) ^ 2 - g j ^ 2n:ℕg:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n),
  x ≠ j →
    P g (oddShiftFst x) * P g (oddShiftFst x) * basis!AsCharges j (oddShiftFst x) +
        P g (oddShiftSnd x) * P g (oddShiftSnd x) * basis!AsCharges j (oddShiftSnd x) =
      0 basis!_on_oddShiftSnd_selfn:ℕg:Fin n → ℚj:Fin n⊢ P g (oddShiftFst j) * P g (oddShiftFst j) * 1 + P g (oddShiftSnd j) * P g (oddShiftSnd j) * -1 =
  P g (oddShiftFst j) ^ 2 - g j ^ 2n:ℕg:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n),
  x ≠ j →
    P g (oddShiftFst x) * P g (oddShiftFst x) * basis!AsCharges j (oddShiftFst x) +
        P g (oddShiftSnd x) * P g (oddShiftSnd x) * basis!AsCharges j (oddShiftSnd x) =
      0n:ℕg:Fin n → ℚj:Fin n⊢ P g (oddShiftFst j) * P g (oddShiftFst j) * 1 + P g (oddShiftSnd j) * P g (oddShiftSnd j) * -1 =
  P g (oddShiftFst j) ^ 2 - g j ^ 2n:ℕg:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n),
  x ≠ j →
    P g (oddShiftFst x) * P g (oddShiftFst x) * basis!AsCharges j (oddShiftFst x) +
        P g (oddShiftSnd x) * P g (oddShiftSnd x) * basis!AsCharges j (oddShiftSnd x) =
      0]n:ℕg:Fin n → ℚj:Fin n⊢ P g (oddShiftFst j) * P g (oddShiftFst j) * 1 + P g (oddShiftSnd j) * P g (oddShiftSnd j) * -1 =
  P g (oddShiftFst j) ^ 2 - g j ^ 2n:ℕg:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n),
  x ≠ j →
    P g (oddShiftFst x) * P g (oddShiftFst x) * basis!AsCharges j (oddShiftFst x) +
        P g (oddShiftSnd x) * P g (oddShiftSnd x) * basis!AsCharges j (oddShiftSnd x) =
      0
  ·n:ℕg:Fin n → ℚj:Fin n⊢ P g (oddShiftFst j) * P g (oddShiftFst j) * 1 + P g (oddShiftSnd j) * P g (oddShiftSnd j) * -1 =
  P g (oddShiftFst j) ^ 2 - g j ^ 2 rw [← oddSnd_eq_oddShiftSnd,n:ℕg:Fin n → ℚj:Fin n⊢ P g (oddShiftFst j) * P g (oddShiftFst j) * 1 + P g (oddSnd j) * P g (oddSnd j) * -1 = P g (oddShiftFst j) ^ 2 - g j ^ 2n:ℕg:Fin n → ℚj:Fin n⊢ P g (oddShiftFst j) * P g (oddShiftFst j) * 1 + -g j * -g j * -1 = P g (oddShiftFst j) ^ 2 - g j ^ 2 P_oddSndn:ℕg:Fin n → ℚj:Fin n⊢ P g (oddShiftFst j) * P g (oddShiftFst j) * 1 + -g j * -g j * -1 = P g (oddShiftFst j) ^ 2 - g j ^ 2n:ℕg:Fin n → ℚj:Fin n⊢ P g (oddShiftFst j) * P g (oddShiftFst j) * 1 + -g j * -g j * -1 = P g (oddShiftFst j) ^ 2 - g j ^ 2]n:ℕg:Fin n → ℚj:Fin n⊢ P g (oddShiftFst j) * P g (oddShiftFst j) * 1 + -g j * -g j * -1 = P g (oddShiftFst j) ^ 2 - g j ^ 2
    ringAll goals completed! 🐙
  ·n:ℕg:Fin n → ℚj:Fin n⊢ ∀ (x : Fin n),
  x ≠ j →
    P g (oddShiftFst x) * P g (oddShiftFst x) * basis!AsCharges j (oddShiftFst x) +
        P g (oddShiftSnd x) * P g (oddShiftSnd x) * basis!AsCharges j (oddShiftSnd x) =
      0 intro k hkjn:ℕg:Fin n → ℚj:Fin nk:Fin nhkj:k ≠ j⊢ P g (oddShiftFst k) * P g (oddShiftFst k) * basis!AsCharges j (oddShiftFst k) +
    P g (oddShiftSnd k) * P g (oddShiftSnd k) * basis!AsCharges j (oddShiftSnd k) =
  0
    erw [basis!_on_oddShiftFst_other hkj.symm,n:ℕg:Fin n → ℚj:Fin nk:Fin nhkj:k ≠ j⊢ P g (oddShiftFst k) * P g (oddShiftFst k) * 0 +
    P g (oddShiftSnd k) * P g (oddShiftSnd k) * basis!AsCharges j (oddShiftSnd k) =
  0 basis!_on_oddShiftSnd_other hkj.symmn:ℕg:Fin n → ℚj:Fin nk:Fin nhkj:k ≠ j⊢ P g (oddShiftFst k) * P g (oddShiftFst k) * 0 + P g (oddShiftSnd k) * P g (oddShiftSnd k) * 0 = 0]n:ℕg:Fin n → ℚj:Fin nk:Fin nhkj:k ≠ j⊢ P g (oddShiftFst k) * P g (oddShiftFst k) * 0 + P g (oddShiftSnd k) * P g (oddShiftSnd k) * 0 = 0
    simp only [mul_zero, add_zero]All goals completed! 🐙

E. The combined basis

E.1. The combined basis as `LinSols`

The whole basis as LinSols.

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

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

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

def Pa (f : Fin n → ℚ) (g : Fin n → ℚ) : (PureU1 (2 * n + 1)).Charges := P f + P! 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 → ℚ⊢ (P f + P! g) oddShiftShiftZero = f 0n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ (P f + P! g) oddShiftShiftZero = f 0]n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ (P f + P! g) oddShiftShiftZero = f 0
  simp only [ACCSystemCharges.chargesAddCommMonoid_add]n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ P f oddShiftShiftZero + P! g oddShiftShiftZero = f 0
  nth_rewrite 1 [oddShiftShiftZero_eq_oddFst_zero]n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ P f oddShiftShiftZero + P! g oddShiftShiftZero = f 0
  rw [oddShiftShiftZero_eq_oddShiftZeron:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ P f oddShiftZero + P! g oddShiftZero = f 0n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ P f oddShiftZero + P! g oddShiftZero = f 0]n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ P f oddShiftZero + P! g oddShiftZero = f 0
  rw [P!_oddShiftZero,n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ P f oddShiftZero + 0 = f 0All goals completed! 🐙 oddShiftZero_eq_oddFst,n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ P f (oddFst 0) + 0 = f 0All goals completed! 🐙 P_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⊢ (P f + P! g) (oddShiftShiftFst j) = f j.succ + g j.castSuccn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n⊢ (P f + P! g) (oddShiftShiftFst j) = f j.succ + g j.castSucc]n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n⊢ (P f + P! 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⊢ P f (oddShiftShiftFst j) + P! 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⊢ P f (oddShiftShiftFst j) + P! 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⊢ P f (oddShiftFst j.castSucc) + P! g (oddShiftFst j.castSucc) = f j.succ + g j.castSuccn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n⊢ P f (oddShiftFst j.castSucc) + P! g (oddShiftFst j.castSucc) = f j.succ + g j.castSucc]n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n⊢ P f (oddShiftFst j.castSucc) + P! g (oddShiftFst j.castSucc) = f j.succ + g j.castSucc
  rw [P!_oddShiftFst,n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n⊢ P 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⊢ P f (oddFst j.succ) + g j.castSucc = f j.succ + g j.castSuccAll goals completed! 🐙 P_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 → ℚ⊢ (P f + P! g) oddShiftShiftMid = g (Fin.last n)n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ (P f + P! g) oddShiftShiftMid = g (Fin.last n)]n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ (P f + P! g) oddShiftShiftMid = g (Fin.last n)
  simp only [ACCSystemCharges.chargesAddCommMonoid_add]n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ P f oddShiftShiftMid + P! g oddShiftShiftMid = g (Fin.last n)
  nth_rewrite 1 [oddShiftShiftMid_eq_oddMid]n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ P f oddShiftShiftMid + P! g oddShiftShiftMid = g (Fin.last n)
  rw [oddShiftShiftMid_eq_oddShiftFst_lastn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ P f (oddShiftFst (Fin.last n)) + P! g (oddShiftFst (Fin.last n)) = g (Fin.last n)n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ P f (oddShiftFst (Fin.last n)) + P! g (oddShiftFst (Fin.last n)) = g (Fin.last n)]n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ P f (oddShiftFst (Fin.last n)) + P! g (oddShiftFst (Fin.last n)) = g (Fin.last n)
  rw [P!_oddShiftFst,n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚ⊢ P 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 → ℚ⊢ P f oddMid + g (Fin.last n) = g (Fin.last n)All goals completed! 🐙 P_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⊢ (P f + P! g) (oddShiftShiftSnd j) = -f j - g jn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n.succ⊢ (P f + P! g) (oddShiftShiftSnd j) = -f j - g j]n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n.succ⊢ (P f + P! 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⊢ P f (oddShiftShiftSnd j) + P! 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⊢ P f (oddShiftShiftSnd j) + P! g (oddShiftShiftSnd j) = -f j - g j
  rw [oddShiftShiftSnd_eq_oddShiftSndn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n.succ⊢ P f (oddShiftSnd j) + P! g (oddShiftSnd j) = -f j - g jn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n.succ⊢ P f (oddShiftSnd j) + P! g (oddShiftSnd j) = -f j - g j]n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n.succ⊢ P f (oddShiftSnd j) + P! g (oddShiftSnd j) = -f j - g j
  rw [P!_oddShiftSnd,n:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚj:Fin n.succ⊢ P 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⊢ P 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 P_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:P f + P! 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 • basisAsCharges i + P! g = 0hf:∀ (i : Fin n.succ), f i = 0⊢ ∀ (i : Fin n.succ), g i = 0 Pn:ℕf:Fin n.succ → ℚg:Fin n.succ → ℚh:∑ i, f i • basisAsCharges i + P! 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 • basisAsCharges i + P! 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 • basisAsCharges i + P! 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:P! g = 0⊢ ∀ (i : Fin n.succ), g i = 0
  exact P!_zero g hAll goals completed! 🐙

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

A point in the span of the whole 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 = P' (f ∘ Sum.inl) + P!' (f ∘ Sum.inr) := byn:ℕf:Fin n ⊕ Fin n → ℚ⊢ Pa' f = P' (f ∘ Sum.inl) + P!' (f ∘ Sum.inr)
  exact Fintype.sum_sum_type _All goals completed! 🐙

E.6. The combined 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:(P' (f ∘ Sum.inl) + P!' (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:(P' (f ∘ Sum.inl) + P!' (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:(P' (f ∘ Sum.inl) + P!' (f ∘ Sum.inr)).val = 0⊢ ∀ (i : Fin n.succ ⊕ Fin n.succ), f i = 0
  change (P' (f ∘ Sum.inl)).val + (P!' (f ∘ Sum.inr)).val = 0 at h1n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚh:Pa' f = 0h1:(P' (f ∘ Sum.inl)).val + (P!' (f ∘ Sum.inr)).val = 0⊢ ∀ (i : Fin n.succ ⊕ Fin n.succ), f i = 0
  rw [P!'_val,n:ℕf:Fin n.succ ⊕ Fin n.succ → ℚh:Pa' f = 0h1:(P' (f ∘ Sum.inl)).val + P! (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:P (f ∘ Sum.inl) + P! (f ∘ Sum.inr) = 0⊢ ∀ (i : Fin n.succ ⊕ Fin n.succ), f i = 0 P'_valn:ℕf:Fin n.succ ⊕ Fin n.succ → ℚh:Pa' f = 0h1:P (f ∘ Sum.inl) + P! (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:P (f ∘ Sum.inl) + P! (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:P (f ∘ Sum.inl) + P! (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'⊢ (P' (Sum.elim g f ∘ Sum.inl) + P!' (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'⊢ (P' (Sum.elim g f ∘ Sum.inl) + P!' (Sum.elim g f ∘ Sum.inr)).val =
  (P' (Sum.elim g' f' ∘ Sum.inl) + P!' (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'⊢ (P' (Sum.elim g f ∘ Sum.inl) + P!' (Sum.elim g f ∘ Sum.inr)).val =
  (P' (Sum.elim g' f' ∘ Sum.inl) + P!' (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'⊢ (P' (Sum.elim g f ∘ Sum.inl) + P!' (Sum.elim g f ∘ Sum.inr)).val =
  (P' (Sum.elim g' f' ∘ Sum.inl) + P!' (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'⊢ (P' (Sum.elim g f ∘ Sum.inl) + P!' (Sum.elim g f ∘ Sum.inr)).val =
  (P' (Sum.elim g' f' ∘ Sum.inl) + P!' (Sum.elim g' f' ∘ Sum.inr)).val
    simp only [succ_eq_add_one, ACCSystemLinear.linSolsAddCommMonoid_add_val, P'_val, P!'_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'⊢ P (Sum.elim g f ∘ Sum.inl) + P! (Sum.elim g f ∘ Sum.inr) = P (Sum.elim g' f' ∘ Sum.inl) + P! (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 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 basis vectors as a 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 = P g + P! f := byn:ℕS:(PureU1 (2 * n.succ + 1)).LinSols⊢ ∃ g f, S.val = P g + P! 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 = P g + P! 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 = P g + P! f
  change P' _ + P!' _ = S at hfn:ℕS:(PureU1 (2 * n.succ + 1)).LinSolsf:Fin n.succ ⊕ Fin n.succ → ℚhf:((P' fun i => f (Sum.inl i)) + P!' fun i => f (Sum.inr i)) = S⊢ ∃ g f, S.val = P g + P! f
  refine ⟨f ∘ Sum.inl, f ∘ Sum.inr, ?_⟩n:ℕS:(PureU1 (2 * n.succ + 1)).LinSolsf:Fin n.succ ⊕ Fin n.succ → ℚhf:((P' fun i => f (Sum.inl i)) + P!' fun i => f (Sum.inr i)) = S⊢ S.val = P (f ∘ Sum.inl) + P! (f ∘ Sum.inr)
  rw [← hfn:ℕS:(PureU1 (2 * n.succ + 1)).LinSolsf:Fin n.succ ⊕ Fin n.succ → ℚhf:((P' fun i => f (Sum.inl i)) + P!' fun i => f (Sum.inr i)) = S⊢ ((P' fun i => f (Sum.inl i)) + P!' fun i => f (Sum.inr i)).val = P (f ∘ Sum.inl) + P! (f ∘ Sum.inr)n:ℕS:(PureU1 (2 * n.succ + 1)).LinSolsf:Fin n.succ ⊕ Fin n.succ → ℚhf:((P' fun i => f (Sum.inl i)) + P!' fun i => f (Sum.inr i)) = S⊢ ((P' fun i => f (Sum.inl i)) + P!' fun i => f (Sum.inr i)).val = P (f ∘ Sum.inl) + P! (f ∘ Sum.inr)]n:ℕS:(PureU1 (2 * n.succ + 1)).LinSolsf:Fin n.succ ⊕ Fin n.succ → ℚhf:((P' fun i => f (Sum.inl i)) + P!' fun i => f (Sum.inr i)) = S⊢ ((P' fun i => f (Sum.inl i)) + P!' fun i => f (Sum.inr i)).val = P (f ∘ Sum.inl) + P! (f ∘ Sum.inr)
  simp only [succ_eq_add_one, ACCSystemLinear.linSolsAddCommMonoid_add_val, P'_val, P!'_val]n:ℕS:(PureU1 (2 * n.succ + 1)).LinSolsf:Fin n.succ ⊕ Fin n.succ → ℚhf:((P' fun i => f (Sum.inl i)) + P!' fun i => f (Sum.inr i)) = S⊢ ((P fun i => f (Sum.inl i)) + P! fun i => f (Sum.inr i)) = P (f ∘ Sum.inl) + P! (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 = P g + P! f) : ∃ (g' f' : Fin n.succ → ℚ),
    S'.val = P g' + P! f' ∧ P! f' = P! f +
    (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges 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 = P g + P! f⊢ ∃ g' f',
  S'.val = P g' + P! f' ∧ P! f' = P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∧ g' = g
  let X := P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges 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 = P g + P! fX:(PureU1 (2 * n.succ + 1)).Charges := P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j⊢ ∃ g' f',
  S'.val = P g' + P! f' ∧ P! f' = P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∧ g' = g
  have hf : P! f ∈ Submodule.span ℚ (Set.range basis!AsCharges) :=
    (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 = P g + P! fX:(PureU1 (2 * n.succ + 1)).Charges := P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges jhf:P! f ∈ Submodule.span ℚ (Set.range basis!AsCharges)⊢ ∃ g' f',
  S'.val = P g' + P! f' ∧ P! f' = P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∧ g' = g
  have hP : (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∈
      Submodule.span ℚ (Set.range basis!AsCharges) :=
    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 = P g + P! fX:(PureU1 (2 * n.succ + 1)).Charges := P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges jhf:P! f ∈ Submodule.span ℚ (Set.range basis!AsCharges)hP:(S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∈ Submodule.span ℚ (Set.range basis!AsCharges)⊢ ∃ g' f',
  S'.val = P g' + P! f' ∧ P! f' = P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∧ g' = g
  have hX : X ∈ Submodule.span ℚ (Set.range (basis!AsCharges)) :=
    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 = P g + P! fX:(PureU1 (2 * n.succ + 1)).Charges := P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges jhf:P! f ∈ Submodule.span ℚ (Set.range basis!AsCharges)hP:(S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∈ Submodule.span ℚ (Set.range basis!AsCharges)hX:X ∈ Submodule.span ℚ (Set.range basis!AsCharges)⊢ ∃ g' f',
  S'.val = P g' + P! f' ∧ P! f' = P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges 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 = P g + P! fX:(PureU1 (2 * n.succ + 1)).Charges := P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges jhf:P! f ∈ Submodule.span ℚ (Set.range basis!AsCharges)hP:(S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∈ Submodule.span ℚ (Set.range basis!AsCharges)hX:X ∈ Submodule.span ℚ (Set.range basis!AsCharges)f':Fin n.succ → ℚhf':∑ i, f' i • basis!AsCharges i = X⊢ ∃ g' f',
  S'.val = P g' + P! f' ∧ P! f' = P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges 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 = P g + P! fX:(PureU1 (2 * n.succ + 1)).Charges := P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges jhf:P! f ∈ Submodule.span ℚ (Set.range basis!AsCharges)hP:(S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∈ Submodule.span ℚ (Set.range basis!AsCharges)hX:X ∈ Submodule.span ℚ (Set.range basis!AsCharges)f':Fin n.succ → ℚhf':∑ i, f' i • basis!AsCharges i = X⊢ S'.val = P g + P! f' ∧ P! f' = P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∧ g = g
  change P! 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 = P g + P! fX:(PureU1 (2 * n.succ + 1)).Charges := P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges jhf:P! f ∈ Submodule.span ℚ (Set.range basis!AsCharges)hP:(S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∈ Submodule.span ℚ (Set.range basis!AsCharges)hX:X ∈ Submodule.span ℚ (Set.range basis!AsCharges)f':Fin n.succ → ℚhf':P! f' = X⊢ S'.val = P g + P! f' ∧ P! f' = P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges 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 = P g + P! fX:(PureU1 (2 * n.succ + 1)).Charges := P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges jhf:P! f ∈ Submodule.span ℚ (Set.range basis!AsCharges)hP:(S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∈ Submodule.span ℚ (Set.range basis!AsCharges)hX:X ∈ Submodule.span ℚ (Set.range basis!AsCharges)f':Fin n.succ → ℚhf':P! f' = X⊢ S'.val = P g + X ∧ X = P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges 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 = P g + P! fX:(PureU1 (2 * n.succ + 1)).Charges := P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges jhf:P! f ∈ Submodule.span ℚ (Set.range basis!AsCharges)hP:(S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∈ Submodule.span ℚ (Set.range basis!AsCharges)hX:X ∈ Submodule.span ℚ (Set.range basis!AsCharges)f':Fin n.succ → ℚhf':P! f' = X⊢ S'.val = P g + X ∧ X = P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges 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 = P g + P! fX:(PureU1 (2 * n.succ + 1)).Charges := P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges jhf:P! f ∈ Submodule.span ℚ (Set.range basis!AsCharges)hP:(S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∈ Submodule.span ℚ (Set.range basis!AsCharges)hX:X ∈ Submodule.span ℚ (Set.range basis!AsCharges)f':Fin n.succ → ℚhf':P! f' = X⊢ S'.val = P g + (P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges 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 = P g + P! fX:(PureU1 (2 * n.succ + 1)).Charges := P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges jhf:P! f ∈ Submodule.span ℚ (Set.range basis!AsCharges)hP:(S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∈ Submodule.span ℚ (Set.range basis!AsCharges)hX:X ∈ Submodule.span ℚ (Set.range basis!AsCharges)f':Fin n.succ → ℚhf':P! f' = X⊢ S'.val = P g + P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges 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 = P g + P! fX:(PureU1 (2 * n.succ + 1)).Charges := P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges jhf:P! f ∈ Submodule.span ℚ (Set.range basis!AsCharges)hP:(S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∈ Submodule.span ℚ (Set.range basis!AsCharges)hX:X ∈ Submodule.span ℚ (Set.range basis!AsCharges)f':Fin n.succ → ℚhf':P! f' = X⊢ S'.val = S.val + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges 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 = P g + P! fX:(PureU1 (2 * n.succ + 1)).Charges := P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges jhf:P! f ∈ Submodule.span ℚ (Set.range basis!AsCharges)hP:(S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∈ Submodule.span ℚ (Set.range basis!AsCharges)hX:X ∈ Submodule.span ℚ (Set.range basis!AsCharges)f':Fin n.succ → ℚhf':P! f' = X⊢ S'.val = S.val + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges 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 = P g + P! fX:(PureU1 (2 * n.succ + 1)).Charges := P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges jhf:P! f ∈ Submodule.span ℚ (Set.range basis!AsCharges)hP:(S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∈ Submodule.span ℚ (Set.range basis!AsCharges)hX:X ∈ Submodule.span ℚ (Set.range basis!AsCharges)f':Fin n.succ → ℚhf':P! f' = X⊢ S'.val = S.val + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges 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 = P g + P! fX:(PureU1 (2 * n.succ + 1)).Charges := P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges jhf:P! f ∈ Submodule.span ℚ (Set.range basis!AsCharges)hP:(S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∈ Submodule.span ℚ (Set.range basis!AsCharges)hX:X ∈ Submodule.span ℚ (Set.range basis!AsCharges)f':Fin n.succ → ℚhf':P! f' = X⊢ S'.val = S.val + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j
  apply 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 = P g + P! fX:(PureU1 (2 * n.succ + 1)).Charges := P! f + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges jhf:P! f ∈ Submodule.span ℚ (Set.range basis!AsCharges)hP:(S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j ∈ Submodule.span ℚ (Set.range basis!AsCharges)hX:X ∈ Submodule.span ℚ (Set.range basis!AsCharges)f':Fin n.succ → ℚhf':P! f' = XhS:S'.val = S.val + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges j⊢ S'.val = S.val + (S.val (oddShiftSnd j) - S.val (oddShiftFst j)) • basis!AsCharges 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 first plane

B.1. The basis vectors of the first 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 first plane into charges

B.6. Components of the first plane

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

B.8. Kernel of the inclusion into charges

B.9. The basis vectors are linearly independent

C. The second plane

C.1. The basis vectors of the second 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 second plane into charges

C.7. Components of the second plane

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

C.9. Kernel of the inclusion into charges

C.10. The inclusion of the second 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

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 basis as `LinSols`