feat: generalized Kronecker delta definition

[wdconinc]

This is my first small definitional PR on the way to proving the gamma matrix trace identities in QFT, part assisted by AI and as part of a general Lean learning trajectory:

1. the generalized Kronecker delta (https://en.wikipedia.org/wiki/Kronecker_delta#Definitions_of_the_generalized_Kronecker_delta) is the Levi-Civita symbol ε^{μνρσ} that comes about in trace identities,
2. contractions over the generalized Kronecker delta, in particular δ^{μ₁...μₖ λₖ₊₁...λₙ}_{μ₁...μₖ ωₖ₊₁...ωₙ} = k! δ^{λₖ₊₁...λₙ}_{ωₖ₊₁...ωₙ}, are at the basis of proving (naturally) Levi-Civita contractions like ε^{μνρσ} ε_{μνρτ} = -6 g^σ_τ,
3. this then leads to proofs of e.g. Tr[ γ5 /a /b /c /d ] = 4i ε^{μνρσ} a_μ b_ν c_ρ d_σ, (with /a the slash notation for a_μ γ^μ).

Review map:

This PR only changes Physlib/Mathematics/KroneckerDelta.lean (where the 1D Kronecker delta is already), and adds the definition of the generalized Kronecker delta. Due to the sign, this must be over ℤ, not just ℕ. Due to this being inside Physlib, I'm using a d = 3 default spatial dimensions. Indices can be any finite type with decidable equality.

Future work:

I'm hoping to extend this gradually (potentially putting some things in PhyslibAlpha) with additional proofs.

• Physlib/Mathematics/KroneckerDelta.lean for the contraction property proof and lemmas (~350 lines),
• Physlib/Relativity/Tensors/RealTensor/Metrics/LeviCivita.lean for the definition of the Levi-Civita symbol as

abbrev leviCivita4Int (μ ν ρ σ : Fin 4) : ℤ :=
  generalizedKroneckerDelta 4 ![μ, ν, ρ, σ] id

and the associated contraction identities (based on generalizedKroneckerDelta_contraction)

• Physlib/Relativity/CliffordAlgebra.lean with the definition of the slash as

def slash (k : Lorentz.Vector 3) : Matrix (Fin 4) (Fin 4) ℂ :=
  ∑ μ, coord k μ • γ μ

and the associated identities.

The heavy lift is the generalized Kronecker delta contraction identity which relies on Laplace expansion (cofactor expansion) and I couldn't find a lot of pre-existing functionality in mathlib. I'm not happy with that and hope to figure out a more compact proof.

AI disclosure

This particular definition is minor enough and has been modified a few times by me (e.g. to prefer ℤ over ℝ, and to reuse the existing definition), but it originates in an AI session. The pitfalls addressed in the AI instructions in #1187 are relevant (i.e. AI reinventing stuff that's already in mathlib).

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

[Copilot]

Pull request overview

Note

Copilot was unable to run its full agentic suite in this review.

Adds a Lean definition of the generalized Kronecker delta (as a determinant of a matrix of Kronecker deltas) to the existing KroneckerDelta development.

Changes:

• Introduces a new “Generalized Kronecker delta” section with brief module documentation.
• Defines an integer-valued entry function δℤ from the existing kroneckerDelta.
• Defines generalizedKroneckerDelta as Matrix.det (δℤ (μ i) (ν j)).

---

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

[jstoobysmith]

Also some build issue here maybe down to a lack of an import?

[jstoobysmith]

I've approved and, assuming this builds, I will merge when ready. Many thanks for this PR - hopefully the first of many :).

[jstoobysmith]

Actually this is not going to build (just checked the linters). Could you make sure lake build works locally - and fix any errors it brings up. Let me know if you need help with this.

[wdconinc]

I've approved and, assuming this builds, I will merge when ready. Many thanks for this PR - hopefully the first of many :).

Likely still needs the import:

public import Mathlib.Data.Matrix.Basic

but untested locally as of yet.

[wdconinc]

This now builds without errors, and the remaining unusedSimpArgs warnings in https://github.com/leanprover-community/physlib/actions/runs/27706659672/job/81959560932?pr=1192#step:6:136 appear to be in the pre-existing code. I can resolve these here or in a separate PR if you want. I don't know what the common practice is in this community.

[jstoobysmith]

@wdconinc Nice! Weird that that simp argument is now triggering - would you mind fixing it here?

[jstoobysmith]

I have put the awaiting-author label to help with review management - when done could you comment with -awaiting-author to remove this label.

[jstoobysmith]

This looks good with me. Happy for me to merge @wdconinc?

[wdconinc]

Yes, fine to merge. I was waiting for CI confirmation before removing the awaiting tag.