feat(Relativity): epsilon-epsilon contraction identities for the Levi-Civita tensor

[Robby955]

Follow-up to #1274: the epsilon-epsilon contraction identities at the symbol level, the form that drives leviCivita's components.

These are proved for generalizedKroneckerDelta f id, which leviCivita_basis_repr_apply already identifies with leviCivita's components, not as corollaries restated directly in terms of (Tensor.basis _).repr ε4. The lowered-index Lorentzian forms actually discussed on #1274 (ε^{...}ε_{...} with one factor lowered by the metric) are referenced below.

• Builds the reusable contraction identity for the generalized Kronecker delta (summing one shared index out of δ^{μ₁…μₖ}_{ν₁…νₖ} reduces rank, the combinatorial fact behind ε^{…}ε_{…}), then specializes it to the three symbol-level identities at rank 4:

• ε^{μνρσ} ε^{μνρσ} = 24 (full contraction)

• ε^{μνρσ} ε^{μνρτ} = 6 δ^σ_τ (three contracted, one free pair)

• ε^{μνρσ} ε^{μντω} = 2 (δ^ρ_τ δ^σ_ω - δ^ρ_ω δ^σ_τ) (two contracted, two free pairs)

These are stated at the symbol level (generalizedKroneckerDelta f id), which leviCivita_basis_repr_apply already identifies with leviCivita's components.

The general contraction lemma needed a rank-one determinant update for singular matrices (Matrix.det_add_rankOne). Mathlib's existing version requires IsUnit A.det; the singular case is left unfinished at Mathlib/LinearAlgebra/Matrix/SchurComplement.lean:425, since the delta-matrices here are generically singular. Proved it via the Schur complement to drop dimension, then a rank-one update, then a Kronecker sum collapse.

these prove the all-upper-index form (ε^{…}ε^{…}), giving +24, +6, +2(…). The mixed form ε^{…}ε_{…} (one factor lowered by the Lorentz metric) picks up a factor of det η = -1 in 4D Minkowski signature, giving the negative signs. Same tensor structure (the antisymmetric δδ - δδ in the two-index case), different convention depending on whether one side is lowered.

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

Important: If a reviewer adds an awaiting-author label to your PR, once you have addressed the review comments, please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

[jstoobysmith]

A couple of comments here:

• theorem -> lemma
• A lot of this is done using the generalizedKroneckerDelta not the leviCivitaTensor, so should likely go into the file where generalizedKroneckerDelta is defined, or it should explicitly use leviCivitaTensor here.
• It would be good to try and write these in terms of the tensor notation. I know this is difficult, but it makes things consistent.

[Robby955]

Updates:

• theorem -> lemma throughout.
• Split the file: the generalizedKroneckerDelta combinatorics (the contraction lemma, the product identity, the iterated sums) moved to Physlib/Mathematics/KroneckerDeltaContraction.lean, next to where
  generalizedKroneckerDelta itself is defined. The three headline lemmas stay in Contractions.lean and a
  re now stated over ε4's actual basis components rather than the bare integer symbol.
• On writing these in full tensor notation: tried the {ε4 | μνρσ ⊗ ε4 | μνρσ}ᵀ form directly and it doesn't elaborate. contrT needs the two contracted indices to have dual colors, and ε4 carries up on all four slots, so pairing up with up fails (τ up = up isn't provable, only τ up = down). The genuine covariant contraction needs the metric-lowered ε_{μνρσ} (all-down), which isn't in physlib yet, so I left this noted in the docstring rather than force it. I will take a better look at that as well tomorrow to confirm that.

[jstoobysmith]

Regarding the tensor contractions, I think what we really want here ε^{μνρσ} ε_{μνρσ}, which means we need to lower the indices of ε_{μνρσ}. Maybe we should define something in Tensor.Elab.lean which lowers indices for us automatically.

[jstoobysmith]

I added some notation #1348 here - and wrote the lemmas you want with sorry. It might be best to base this PR off that one

[Robby955]

Thanks for adding the notation and sketching the two lemmas.

Working through leviCivita_contract_self, I'm getting -24 rather than 24. Tracing it through minkowskiMatrix, the diagonal product over any of ε4's nonzero (permutation) components comes out to (+1)(-1)(-1)(-1) = -1, so the metric contraction picks up a sign relative to the symbol-level +24 from #1335. I may be missing something about the convention there.

Same story for leviCivita_contract_three: I'm getting -6 •ₜ unitTensor Color.down rather than the bare unit tensor. The sign plus the 3! = 6 comes from contracting three indices, cross-checked against the -24 result by taking its trace.

Separately, trying to actually build these with the τ(μ) τ(ν) τ(ρ) τ(σ) notation, I'm hitting isDefEq timeouts unifying the nested Function.update color against the plain .down color the proof needs downstream. Looks like a defeq-performance issue rather than a math one. A few things that might help: normalizing the nested color to .down before the final step, a reducibility lemma for τ on Function.update colors, or going through the tensor-algebra side instead of index-by-index. Haven't tried any of these yet, but I am going to give a few of them a try now.

I may be missing something on either the signs or the notation.

[jstoobysmith]

@Robby955 Awesome. I actually think the -24 and -6 is correct, see e.g.

https://en.wikipedia.org/wiki/Levi-Civita_symbol#Example:_Minkowski_space

Do you have an example of where you hit isDefEq which you could provide a snippet off. I'm guessing it is due to how Function.update is defined.

[jstoobysmith]

I should also say, that I did not build any API around, toDualAtIndex, and some would no doubt be useful.

[Robby955]

So the symbol level identities stay +24 and +6, and the covariant statements pick up det η = -1, giving the -24 and -6.

Here is a minimal case of the isDefEq issue, from Function.update. The color of a τ-lowered tensor is a nested Function.update chain, and that is extensionally but not definitionally equal to the literal color vector:

import Physlib.Relativity.Tensors.LeviCivita.Contractions
import Physlib.Relativity.Tensors.RealTensor.Metrics.Basic

open realLorentzTensor

example :
    (Function.update (Function.update (Function.update (Function.update
      (![Color.up, Color.up, Color.up, Color.up] : Fin 4 → Color)
      0 ((realLorentzTensor 3).τ Color.up)) 1 ((realLorentzTensor 3).τ Color.up))
      2 ((realLorentzTensor 3).τ Color.up)) 3 ((realLorentzTensor 3).τ Color.up))
    = ![Color.down, Color.down, Color.down, Color.down] := by
  rfl

fails with "is not definitionally equal": the left side is a chain of dite lambdas, the right is a vecCons, and they only agree pointwise.

noncomputable def lowered : ℝT[3, .down, .down, .down, .down] :=
  {ε4 | τ(μ) τ(ν) τ(ρ) τ(σ)}ᵀ

-- Type mismatch
--   toDualAtIndex 3 (toDualAtIndex 2 (toDualAtIndex 1 (toDualAtIndex 0 ε4)))
-- has type
--   Tensor (Function.update (Function.update ... 0 (τ (![up,up,up,up] 0))) 1 (τ (Function.update ... 1)) ...)

The updates also nest inside the later τ's, so the term the unifier works on grows quickly. In larger elaborations it grinds through that before giving up, which is where my heartbeat timeouts came from rather than this clean failure.

What worked was staying at the component level and never asserting the color equality. Doing that, I now have both of the #1348 sketch lemmas proved at their covariant values, on a branch building on this one:

• leviCivita_contract_self : {ε4 | μ ν ρ σ ⊗ ε4 | τ(μ) τ(ν) τ(ρ) τ(σ)}ᵀ.toField = -24
• leviCivita_contract_three : the (-6) • unitTensor Color.down form

Together with component API around toDualAtIndex: single-index lowering multiplies each basis component by the diagonal η factor, the four-fold lowered ε4, det η = -1 on the support of ε4, and the scalar of a full upper-against-lower contraction as a component sum. If that makes sense I can open it as a follow-up PR once/if this one merges.

The specific mangles, if you'd rather fix in place: "color eqe both" → "color equality. Doing that, I now have both"; "branchbuilding" → "branch building"; "multipldiagonal η factor" → "multiplies each basis component by the diagonal η factor"; "ε4,and" → "ε4, and".

[Robby955]

-awaiting-author

[jstoobysmith]

Maybe we should name this file CovariantContractions? or similar

[Robby955]

The current content is the all-upper-index symbol-level identities, not the lowered ε_{μνρσ} form (that's #1348), so CovariantContractions could overstate it a bit. Want me to keep Contractions, or use SymbolContractions?

[jstoobysmith]

Will try and see if we can get Function.update to be def-eq. It is a bit annoying that it isn't.

[jstoobysmith]

import Physlib.Relativity.Tensors.LeviCivita.Contractions
import Physlib.Relativity.Tensors.RealTensor.Metrics.Basic

open realLorentzTensor

example :
    (Function.update (Function.update (Function.update (Function.update
      (![Color.up, Color.up, Color.up, Color.up] : Fin 4 → Color)
      0 ((realLorentzTensor 3).τ Color.up)) 1 ((realLorentzTensor 3).τ Color.up))
      2 ((realLorentzTensor 3).τ Color.up)) 3 ((realLorentzTensor 3).τ Color.up))
    = ![Color.down, Color.down, Color.down, Color.down] := by
  decide

works, so they are decidable equal. I think this is likely all that we can ask for here.

[jstoobysmith]

This also works here:

def lowered : ℝT[3, .down, .down, .down, .down] := permT id .auto
  {ε4 | τ(μ) τ(ν) τ(ρ) τ(σ)}ᵀ

[Robby955]

Cool, thanks!

I'll restate the follow-up branch on top of your permT form rather than the toDualAtIndex component route.

[jstoobysmith]

This permT route still uses toDaulAtIndex though in the taus unless I’m confused about what you mean

[Robby955]

You're right, thanks for catching this, I mislabeled that. The taus in {ε4 | τ(μ) τ(ν) τ(ρ) τ(σ)}ᵀ are toDualAtIndex, so permT doesn't replace it. What permT id .auto handles is the color ascription, letting the tau-lowered tensor be typed at the literal .down color; the lowering itself is still toDualAtIndex. So it composes with the component lemmas that compute the -24 and -6, rather than being an alternative to them. My earlier "permT instead of toDualAtIndex" was the wrong way to put it.

[Robby955]

Moved and made public next to their definitions:

kron_finSum → KroneckerDelta.kroneckerDelta_finSumFinEquiv; symbol_zero/one/two → sum_generalizedKroneckerDelta_mul_self / _cons / _cons₂ in KroneckerDeltaContraction. Contractions.lean keeps only cons_finSum and now calls the new names.

[Robby955]

-awaiting-author