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.

[wdconinc]

Didn't want to redefine the existing kroneckerDelta without discussion, but open to it.

[jstoobysmith]

I agree with the way you have done this not how copilot is suggesting it. The decision to define the dirac-delta in terms of natural numbers was a deliberate one.

[jstoobysmith]

Suggested change

	`δ^{μ₁...μₙ}_{ν₁...νₙ} = det (δ[μᵢ, νⱼ])`.
	`δ^{μ₁...μₙ}_{ν₁...νₙ} = det (δ[μᵢ, νⱼ])`.

Linter is complaining about this trailing whitespace.

[jstoobysmith]

I wonder if this is more general still

Suggested change

	This is defined for any finite type `α` with decidable equality. -/
	def generalizedKroneckerDelta {α : Type} [DecidableEq α] [Fintype α] (n : ℕ)
	(μ : Fin n → α) (ν : Fin n → α) : ℤ :=
	Matrix.det (fun i j => δℤ (μ i) (ν j))
	This is defined for any finite type `α` with decidable equality. -/
	def generalizedKroneckerDelta {α ι : Type} [DecidableEq α] [Fintype α]
	[DecidableEq ι] [Fintype ι]
	(μ : ι → α) (ν : ι → α) : ℤ :=
	Matrix.det (fun i j => δℤ (μ i) (ν j))

[jstoobysmith]

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