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_μ. Introduce a combining character for slash notation (not used yet).

Reviewer map

All changes in Physlib/Relativity/CliffordAlgebra.lean.

γ

This moves γ to be indexed as Fin 1 ⊕ Fin 3 for compatibility with Lorentz vectors.

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).

slash

The definition of /a = γ^μ a_μ. Since γ is now indexed over Fin 1 ⊕ Fin 3 there is no more need to bridge the Fin 1 ⊕ Fin d → ℝ (Lorentz vectors) to Fin 4 → ℂ (gamma matrices) gap.

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). Also implemented via LinearMap.

Future work

The next step here is implement a theorem that extends the gamma_anticomm to slash_anticomm as well. 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.

[wdconinc]

-awaiting-author

[Copilot]

Pull request overview

This PR extends Physlib.Relativity.CliffordAlgebra with Lorentz-indexed gamma matrices (Fin 1 ⊕ Fin 3), proves the gamma anticommutation relation against the Minkowski metric, and introduces Dirac slash operators (including a list-product helper) for Lorentz vectors.

Changes:

• Re-index γ to Fin 1 ⊕ Fin 3 to align with Minkowski/Lorentz index types and update the Clifford lift accordingly.
• Add gamma_anticomm : γ μ γ ν + γ ν γ μ = 2 g^{μν} I proved by explicit case evaluation.
• Add Slash.slash and Slash.slashProd (plus linear-map helpers) for slashing Lorentz vectors and multiplying slash factors.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[jstoobysmith]

@wdconinc let me know when you want a review of this again :).

[wdconinc]

@wdconinc let me know when you want a review of this again :).

I'm at a conference this week (including talking to theorists in my field about Lean and Physlib), but I will take a final look when I'm back and mark as ready for review.

[jstoobysmith]

This may be difficult, but I think it might be possible to lift this to an intertwining map between representations.

[wdconinc]

Is your thinking here that this will then have an easier way to reuse the same structures for various spinor representations (Dirac and Weyl) without having this built up on the foundation of only a single gamma matrix definition? I think that would likely require some more work on generalizing the gamma matrix definition because the current form only works for Dirac spinors.

[jstoobysmith]

This wasn't my thinking, but this may be a benefit here. I was just thinking that slash really does represent a map between representations, and it might be nice to encode that somewhere. But this can wait till a future date. I think generalizing the gamma matrices would also be nice (making explicit that they carry e.g. complexLorentzTensor indices or similar).

[jstoobysmith]

(I think one of the things we would need to do before any of this is define and make a good API around Fermion.dirac, which we currently do not have.

[jstoobysmith]

As it stands, I'm happy to approve this PR now for merger.