feat: gamma anticommutator and slash of Lorentz vector

[wdconinc]

This PR adds the gamma matrix anticommutation relation (γ^μ γ^ν + γ^ν γ^μ = 2 g^μν I_4), and the slash operator on Lorentz vectors: /a = γ^μ a_μ. Although it would be nice, there is no notation for slash included since (naturally) slash is already taken.

Reviewer map

All changes in Physlib/Relativity/CliffordAlgebra.lean.

gamma_anticomm

This is proven with explicit evaluation. Since the gamma matrices are defined as explicit matrices, there's not much we can fall back on, I think. If the gamma matrices were defined using Pauli matrices, then we might be able to approach this differently by falling back to Pauli matrices anticommutators (not currently implemented).

coord and slash

To bridge the Fin 1 ⊕ Fin d → ℝ (Lorentz vectors) to Fin 4 → ℂ (gamma matrices) gap, coord does the cast for d = 3.

slashProd

To assist with the common occurrence of multiple (typ. 4) slash momentum products, the slashProd definition takes a list of Lorentz vectors, slashes them, and gives the product (left to right).

Future work

The next step here is implement a theorem that extends the gamma_anticomm to slash_anticomm as well, which is relatively straightforward but gets wordier than I would like due to the same Fin 1 ⊕ Fin 3 → ℝ to Fin 4 → ℂ mismatch between Lorentz vectors, gamma matrices, and metrics. The step after that is to add the trace identities on products of slash momenta.

The addition of the generalized Kronecker delta will allow for a Levi-Civita module, which can then be included here for the trace identities that have a gamma5.

AI disclosure

The initial version was written with help of AI, but it was reworked a few times (e.g. making the gamma_anticomm theorem the basis instead of including a slash_anticomm theorem from scratch).

[github-actions]

Thank you for this PR, which will now be reviewed.
If submitting to ./Physlib or ./QuantumInfo, please
see our review guidelines
if you are not familiar with the process. You should expect a back and forth
with a reviewer before your PR is merged. See also that link for how to
add appropriate labels to your PR. The PR will also go through a number
of automated checks. You can learn more about these here,
including how to run them locally.

If you are submitting to ./PhyslibAlpha there will be a lighter review process,
though your PR must still pass the automated checks.

If you want to bring attention to this PR, please write a message on this
thread of the Lean Zulip.

[jstoobysmith]

You shouldn't actually need the 3 in Lorentz.Vector 3 as it should default to that value.

[jstoobysmith]

I also think the solution to this is to change the definition of gamma so it is based on Fin 1 ⊕ Fin 3 rather then Fin 4, likewise with all the occurances of Fin 4 below.

[jstoobysmith]

The three below lemmas can be consolidated with lifting this to a linear map.