Properties of the Pauli matrices

[jstoobysmith]

This is an issue to track the formalization of properties of the Pauli matrices.

The goal is to prove the properties of the Pauli matrices using index notation with HepLean. The properties of the Pauli matrices to be proved are (2.23)-(2.30) of this note.

• 2.23
• 2.24
• 2.25
• 2.26
• 2.27
• 2.28
• 2.29
• 2.30

It may be best to complete a number of steps before this:

• Improve the API around the basis of tensors and tensor trees, to allow calculations to be done by looking at each component (Done in feat: Improvements to index notation #343)
• Improve the @[simp]'s lemma around tensor trees and tensors, to make the calculations of the above as simple as possible. (Done in feat: Improvements to index notation #343)
• Define an integer version of (coordinates of) tensors, and show that it injects into all tensors. On these decide can be used. (Done in feat: Improvements to index notation #343)
• Using the above three, simplify the proof and speed of: pauliCo_contr_pauliContr. (Done in feat: Improvements to index notation #343)
• Define the epsilon Lorentz tensor with four four-vector indices.
• Write the above lemmas out using index notation in Lean.

After these have all been formalized:

• Make a curated noted containing for Pauli matrices and their properties.

This issue is related to: #286.

Contributions to this issue are very much welcome in any direction.