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

i. Overview

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

ii. Key results

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

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

Shifted.planeLinSols : The inclusion of the shifted plane.

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

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

iii. Table of contents

A. Splitting the charges up into groups

A.1. The even split: Spltting the charges up via n.succ + n.succ

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

A.3. Lemmas relating the two splittings

B. The unshifted plane

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

B.2. Components of the basis vectors

B.3. The basis vectors satisfy the linear ACCs

B.4. The basis vectors satisfy the cubic ACC

B.5. The basis vectors as linear solutions

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

B.7. Components of the inclusion into charges

B.8. The inclusion into charges satisfies the linear and cubic ACCs

B.9. Kernel of the inclusion into charges

B.10. The inclusion of the plane into linear solutions

B.11. The basis vectors are linearly independent

B.12. Every vector-like even solution is in the span of the basis of the unshifted plane

C. The shifted plane

C.2. Components of the vectors

C.3. The vectors satisfy the linear ACCs

C.4. The vectors satisfy the cubic ACC

C.6. The vectors as linear solutions

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

C.8. Components of the inclusion into charges

C.9. The inclusion into charges satisfies the cubic ACC

C.10. Kernel of the inclusion into charges

C.11. The inclusion of the shifted plane into the span of the basis

C.12. The inclusion of the plane into linear solutions

C.13. The basis vectors are linearly independent

C.14. Properties of the basis vectors relating to the span

C.15. Permutations as additions of basis vectors

D. Mixed cubic ACCs involving points from both planes

E. The combined basis

E.1. As a map into linear solutions

E.2. Inclusion of the span of the basis into charges

E.3. Components of the inclusion into charges

E.4. Kernel of the inclusion into charges

E.5. The inclusion of the span of the basis into linear solutions

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

A. Splitting the charges up into groups

We have 2 * n.succ 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 even split: Spltting the charges up via n.succ + n.succ

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

The inclusion of Fin n.succ into Fin (n.succ + n.succ) via the second n.succ, casted into Fin (2 * n.succ).

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

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

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

The element of Fin (1 + (n + n + 1)) corresponding to the first 1, casted into Fin (2 * n.succ).

The element of Fin (1 + (n + n + 1)) corresponding to the second 1, casted into Fin (2 * n.succ).