feat: gamma endomorphisms of Dirac fermions

[lizr-phys]

Define Clifford multiplication on Dirac fermions in Lean 4 and derive the existing Dirac-representation matrices from the same operators. The canonical map is Fermion.Dirac.gammaMatrix : Lorentz.Vector →ₗ[ℝ] Module.End ℂ Dirac. It satisfies the Clifford relation for arbitrary Lorentz vectors; its components, chirality operator, and complementary chiral projectors satisfy the corresponding identities.

AI assistance: GPT-6 Astra. The human author is responsible for independently checking the definitions, statements, proofs, and the implementation of reviewer feedback before requesting re-review.

Conventions: Lorentz.Vector is real and contravariant. The chiral blocks of gammaMatrix v are [0, v⁰I − vⁱσⁱ; v⁰I + vⁱσⁱ, 0]; raising the basis index gives gamma μ. Thus gammaMatrix v = v_μ γ^μ, with signature (+,-,-,-) and gamma5 = diag(-1,-1,1,1).

Reviewer map: start with endEquivMatrix in Dirac/Basic.lean, then the vector action and its Clifford proof in sections A–B of Dirac/GammaMatrices.lean, followed by chirality and projectors in sections C–D. Finally, inspect CliffordAlgebra.lean, where the existing algebra construction now uses endEquivMatrix (gamma μ) directly. The quadratic form retains Fin 4 coordinates; finSumFinEquiv connects these coordinates to the canonical Fin 1 ⊕ Fin 3 indices.

Declarations added in Physlib/Relativity/Fermions/Dirac/Basic.lean, under Fermion.Dirac:

Declaration	Purpose
endEquivMatrix	Complex algebra equivalence from Dirac endomorphisms to matrices in the Dirac representation.
endEquivMatrix_apply	Explicit change of coordinates from the chiral basis.

Declarations added in Physlib/Relativity/Fermions/Dirac/GammaMatrices.lean, under Fermion.Dirac:

Declaration	Purpose
gammaMatrix	Real linear Clifford multiplication on Dirac fermions.
gammaMatrix_toMatrix, gammaMatrix_basis_toMatrix	Chiral matrices for arbitrary vectors and basis vectors.
gammaMatrix_basis_anticomm, gammaMatrix_anticomm, gammaMatrix_mul_self	Clifford relations on basis pairs and arbitrary vectors, and the square identity.
gamma, gammaMatrix_basis, gammaMatrix_eq_sum	Upper-index components and their relation to vector Clifford multiplication.
gamma_toMatrix	Explicit chiral component matrices.
gamma_anticomm, gamma_mul_self, gamma_inl_zero_mul_self, gamma_inr_mul_self, gamma_mul_gamma_of_ne	Component anticommutators and squares.
gamma5, gamma5_toMatrix, gamma5_mul_self, gamma5_mul_gamma, gamma5_mul_gammaMatrix	Chirality, its chiral matrix, square, and anticommutation properties.
leftChiralProjector, rightChiralProjector	Left and right chiral projectors.
leftChiralProjector_toMatrix, rightChiralProjector_toMatrix	Coordinate projections onto the Weyl components.
leftChiralProjector_mul_self, rightChiralProjector_mul_self	Idempotence.
leftChiralProjector_mul_rightChiralProjector, rightChiralProjector_mul_leftChiralProjector	Orthogonality in both orders.
leftChiralProjector_add_rightChiralProjector	The projectors sum to the identity.

Changes in Physlib/Relativity/CliffordAlgebra.lean:

• spaceTime.γ0, γ1, γ2, γ3 are derived from Fermion.Dirac.gamma through endEquivMatrix. Their entries and existing square/anticommutation statements are preserved. The proofs of γ0_mul_γ0, γ1_mul_γ1, γ2_mul_γ2, γ3_mul_γ3, γ1_mul_γ0, γ2_mul_γ0, γ3_mul_γ0, γ2_mul_γ1, γ3_mul_γ1, and γ3_mul_γ2 transport the operator identities.
• γ5_eq_endEquivMatrix identifies the existing product definition γ5 with the canonical chirality endomorphism in the Dirac representation.
• The redundant spaceTime.γ : Fin 4 → Matrix (Fin 4) (Fin 4) ℂ is removed. The spaceTime.γ namespace is retained for the existing algebra API.
• spaceTime.γ.γSet, γ_in_γSet, γ_in_diracAlgebra, and γ_subtype_in_range now use endEquivMatrix (Fermion.Dirac.gamma μ) with μ : Fin 1 ⊕ Fin 3. diracAlgebra and γSet_subset_diracAlgebra keep their construction.
• ofCliffordAlgebra and ofCliffordAlgebra_ι_single use the canonical components through finSumFinEquiv. The diracForm, range, and surjectivity API is preserved, including ofCliffordAlgebra_range_eq_top and ofCliffordAlgebra_surjective.

Migration from the preceding PR revision: spaceTime.diracMatrix and diracMatrix_apply move to Fermion.Dirac.endEquivMatrix and endEquivMatrix_apply; γ5_eq_diracMatrix becomes γ5_eq_endEquivMatrix; γ_eq_diracMatrix is removed with the redundant family. Physlib.lean imports the new gamma module, and Dirac/API-map.yaml records the API.

PR #1206 remains separate and overlaps CliffordAlgebra.lean; its matrix-family references will require coordination. This PR does not add slash, Lorentz equivariance, or new Clifford-algebra functionality.

Validation: targeted builds pass, and lake --no-cache build completes all 9,358 jobs. The 14 focused theorem linters pass for Dirac.Basic, Dirac.GammaMatrices, and CliffordAlgebra; their axiom audit permits only propext, Classical.choice, and Quot.sound. Explicit matrix checks preserve the old Dirac-representation entries. Redundant-import checks for all three modules, the repository import-completeness check, API-map checks, focused source style, spelling, and git diff --check pass. The native lint_all launcher is blocked by missing cc on Windows. The full shell style check reports CRLF line endings only in untouched files; it reports no errors in this revision's modified files.

[github-actions]

Thank you for this pull-request (PR). If this is your first PR, welcome to the community!

Below is what will happen next. Please read carefully if you are not familiar with the process. You may open other PRs while this one is being reviewed, and can stack PRs on top of each other, so don't let these steps slow you down.

1. Some automated checks will be run on your PR. You can see the results of these checks at the buttom of your PR page. If any of these checks fail, you will need to fix the issues before your PR can be merged. You can learn more about these here, including how to run them locally, which is sometimes quicker than relying on the GitHub Actions. If you have never had a PR merged before, you may have to wait for a reviewer to manually start these checks (this is for security).

2. A reviewer will look at your PR and may ask you to make changes. This may happen a couple of days after you submit your PR, so you may need to be patient. But it should not be longer than that - if it is please bring it to the attention of the community on the Zulip. The level of review will depend on where your PR is submitted. If it is submitted to ./Physlib or ./QuantumInfo, the review will be more thorough than if it is submitted to ./PhyslibAlpha. You can find out more about what the review process is looking for in our review guidelines. If a reviewer adds an awaiting-author label to your PR, address the review comments, then please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

3. The reviewer will either approve your PR, or request more changes (in which case we return to step 2). Once your PR is approved, it will be merged by a maintainer, this should happen shortly after approval, though you may get more comments at this stage.

Tip: The easiest way to get have a fast review is to submit a PR that is small and self-contained, and has clear documentation explaining why things are the way they are in your chages.

If you have any problems or questions, please reach out to the community on the Zulip.

[jstoobysmith]

One comment here, but it is a definitional change, so will affect a lot of the other things here.

[jstoobysmith]

If you can, I would make this the definition of gammaMatrx write all of the lemmas in terms of this. You could even lift this to a linear map:

Lorentz.Vector \to Module.End ℂ Dirac

[lizr-phys]

Hi Joseph, PR #1627 has been updated according to your definition-level suggestion. The current GitHub Actions workflows are awaiting maintainer approval. Could you please approve and run them when convenient?

[jstoobysmith]

awaiting-author

[jstoobysmith]

Couple more comments

[jstoobysmith]

Would remove priviate on these lemmas. Not really needed.

[lizr-phys]

Hi Joseph, I addressed both comments. The two Lorentz-basis calculation lemmas are now public and documented. The existing Dirac-representation matrices γ0–γ5 are now derived from the canonical Dirac-space gamma endomorphisms through an explicit chiral-to-Dirac algebra equivalence, while preserving the existing matrix and Clifford-algebra API. Targeted and full builds pass. PR #1206 remains separate; its overlap with CliffordAlgebra.lean will need coordination.

[jstoobysmith]

I would replace the existing definitions of gamma matrices we have in Physlib with this definition in this PR. As this is much better.

[jstoobysmith]

Would move this to ./Fermions/Dirac, and rename it endEquivMatrix

[jstoobysmith]

If we can remove this altogether and just use your definitions I think that would be better.

[lizr-phys]

Thanks for the comments. I’ve addressed both in the latest revision: endEquivMatrix is now in Fermions/Dirac/Basic.lean, and the redundant matrix-level γ family has been removed so that the Clifford algebra construction uses Fermion.Dirac.gamma directly.
If there are only minor cleanups or style/API adjustments remaining, please feel free to make them directly on the branch.

[jstoobysmith]

Approved. Many thanks @lizr-phys for this PR! Hopefully the first of many :).