feat(Tensors/Contraction): slot-addressed cross contraction and the general-rank raise/lower round trip

Physlib.lean

@@ -404,9 +404,12 @@ public import Physlib.Relativity.Tensors.Conjugation.Basic
 public import Physlib.Relativity.Tensors.Constructors
 public import Physlib.Relativity.Tensors.Contraction.Basic
 public import Physlib.Relativity.Tensors.Contraction.Basis
+public import Physlib.Relativity.Tensors.Contraction.CrossToEnd
+public import Physlib.Relativity.Tensors.Contraction.CrossToSlot
 public import Physlib.Relativity.Tensors.Contraction.Products
 public import Physlib.Relativity.Tensors.Contraction.Pure
 public import Physlib.Relativity.Tensors.Contraction.SuccSuccAbove
+public import Physlib.Relativity.Tensors.Contraction.UnitTensorContraction
 public import Physlib.Relativity.Tensors.Dual
 public import Physlib.Relativity.Tensors.Elab
 public import Physlib.Relativity.Tensors.Evaluation

Physlib/Relativity/Tensors/Basic.lean

@@ -628,6 +628,12 @@ lemma permT_eq_zero_iff {n m : ℕ} {c : Fin n → C} {c1 : Fin m → C}
   funext x
   simp [IsReindexing.inv_apply_apply]
 
+/-- `permT` is injective. -/
+lemma permT_injective {n m : ℕ} {c : Fin n → C} {c1 : Fin m → C}
+    {σ : Fin m → Fin n} (h : IsReindexing c c1 σ) :
+    Function.Injective (permT (S := S) σ h) :=
+  (injective_iff_map_eq_zero' _).mpr (permT_eq_zero_iff h)
+
 /-!
 ## field
 -/

Physlib/Relativity/Tensors/Contraction/CrossToSlot.lean

@@ -0,0 +1,151 @@
+/-
+Copyright (c) 2026 Andrea Pari. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrea Pari
+-/
+module
+
+public import Physlib.Relativity.Tensors.Contraction.CrossToEnd
+/-!
+
+# Result-to-slot contraction against a rank-2 tensor
+
+## i. Overview
+
+`crossToEnd` deposits the surviving index of a slot contraction at the end of the survivor list.
+Raising and lowering a named index instead wants the replacement to stay *in place*: contracting
+slot `i` of `t` against a rank-2 tensor `M` (a metric, the unit tensor) should return `t` with only
+slot `i`'s color changed, `T^{μ}{}_{νρ} ↦ T_{μνρ}`. `crossToSlot i j hc M` is that operation, and
+`crossToSlot_eq_crossToEnd` is the one place the two conventions meet.
+
+This module stays at the `CommRing` altitude of `crossToEnd`; the `RCLike` round trips built on the
+operation live with the unit-tensor collapse theory in
+`Physlib.Relativity.Tensors.Contraction.UnitTensorContraction`.
+
+## ii. Key results
+
+- `TensorSpecies.Tensor.crossToSlot` : contract slot `i` against slot `j` of a rank-2 tensor and
+    rotate the survivor back into position `i`; raising and lowering a named index.
+- `TensorSpecies.Tensor.crossToSlot_eq_crossToEnd` : the bridge to the result-to-end convention.
+- `TensorSpecies.Tensor.crossToSlotInv` : the returning half of a round trip, the contraction
+    against the second factor with the round trip's color cast absorbed.
+- `TensorSpecies.Tensor.crossToSlot_permT_right_id` : an identity reindexing of the rank-2 tensor
+    passes through the contraction.
+- `TensorSpecies.Tensor.crossToSlot_equivariant` : the contraction commutes with the `G`-action.
+
+## iii. Table of contents
+
+- A. The result-to-slot contraction
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+namespace TensorSpecies
+
+variable {k : Type} [CommRing k] {C : Type} {G : Type} [Group G]
+    {V : C → Type} [∀ c, AddCommGroup (V c)] [∀ c, Module k (V c)]
+    {basisIdx : C → Type} [∀ c, Fintype (basisIdx c)] [∀ c, DecidableEq (basisIdx c)]
+    {rep : (c : C) → Representation k G (V c)} {b : (c : C) → Module.Basis (basisIdx c) k (V c)}
+    {S : TensorSpecies k C G V basisIdx rep b}
+
+namespace Tensor
+
+/-!
+
+## A. The result-to-slot contraction
+
+-/
+
+/-- The survivor color of `crossToEnd i j` against a rank-2 tensor of color `cM` is `c` with
+  slot `i` replaced by the surviving color `cM (j.succAbove 0)`, once the survivors are rotated
+  back by the inverse of the cycle `[i, last]`. -/
+lemma IsReindexing.crossToSlot_cycle {nA : ℕ} {c : Fin (nA + 1) → C} {cM : Fin 2 → C}
+    (i : Fin (nA + 1)) (j : Fin 2) :
+    IsReindexing
+      (Fin.append (c ∘ i.succAbove) (cM ∘ j.succAbove))
+      (Function.update c i (cM (j.succAbove 0)))
+      ⇑(Fin.cycleIcc i (Fin.last nA)).symm := by
+  refine ⟨(Fin.cycleIcc i (Fin.last nA)).symm.bijective, fun y => ?_⟩
+  obtain ⟨z, rfl⟩ : ∃ z, y = Fin.cycleIcc i (Fin.last nA) z :=
+    ⟨_, (Equiv.apply_symm_apply _ _).symm⟩
+  rw [Equiv.symm_apply_apply, ← Fin.append_succAbove_const_eq_cycleIcc i]
+  refine Fin.addCases (fun a => ?_) (fun a => ?_) z
+  · rw [Fin.append_left, Fin.append_left, Function.comp_apply,
+      Function.update_of_ne (Fin.succAbove_ne i a)]
+  · rw [Fin.append_right, Fin.append_right, Function.comp_apply, Function.update_self]
+    fin_cases a
+    rfl
+
+/-- Contract slot `i` of `t` against slot `j` of the rank-2 tensor `M`, whose `j`-slot color must
+  equal the dual color `τ (c i)` (propositionally, via `hc`), and rotate `M`'s surviving slot back
+  into position `i`. The result is `t` with slot `i` relabelled to `M`'s surviving color.
+
+  This is raising and lowering a named index; the metric case is `j = 0`,
+  `M = metricTensor (τ (c i))`. Because `hc` is propositional, a rank-2 tensor whose slot color
+  matches only up to an equality enters directly, with no transport. -/
+noncomputable def crossToSlot {nA : ℕ} {c : Fin (nA + 1) → C} {cM : Fin 2 → C}
+    (i : Fin (nA + 1)) (j : Fin 2) (hc : S.τ (c i) = cM j) (M : S.Tensor cM) :
+    S.Tensor c →ₗ[k] S.Tensor (Function.update c i (cM (j.succAbove 0))) :=
+  permT ⇑(Fin.cycleIcc i (Fin.last nA)).symm (IsReindexing.crossToSlot_cycle i j) ∘ₗ
+    (crossToEnd i j hc).flip M
+
+/-- The bridge between the two conventions: `crossToSlot i j hc M t` is `crossToEnd i j hc t M`
+  with the survivor rotated from the last slot back to slot `i` by the inverse cycle. -/
+lemma crossToSlot_eq_crossToEnd {nA : ℕ} {c : Fin (nA + 1) → C} {cM : Fin 2 → C}
+    (i : Fin (nA + 1)) (j : Fin 2) (hc : S.τ (c i) = cM j) (M : S.Tensor cM) (t : S.Tensor c) :
+    crossToSlot i j hc M t =
+      permT ⇑(Fin.cycleIcc i (Fin.last nA)).symm (IsReindexing.crossToSlot_cycle i j)
+        (crossToEnd i j hc t M) := rfl
+
+/-- Contract slot `i` of a tensor whose color there is `d` against `M'`, then absorb the color cast
+  the two `Function.update`s generate, landing back on `c`. This is the returning half of a
+  raise-then-lower round trip; absorbing the cast here is what keeps the round trip cast-free at
+  both ends. -/
+noncomputable def crossToSlotInv {nA : ℕ} {c : Fin (nA + 1) → C} {b d e : C} (i : Fin (nA + 1))
+    (he : c i = e) (hb : S.τ d = b) (M' : S.Tensor ![b, e]) :
+    S.Tensor (Function.update c i d) →ₗ[k] S.Tensor c :=
+  permT (id : Fin (nA + 1) → Fin (nA + 1))
+      (IsReindexing.on_id_symm (IsReindexing.update_update_of_eq (d := d) i he)) ∘ₗ
+    crossToSlot i (0 : Fin 2)
+      (by rw [Function.update_self]; exact hb : S.τ (Function.update c i d i) = b) M'
+
+/-- An identity reindexing of the rank-2 tensor becomes the corresponding identity reindexing of
+  the contracted output: the `crossToSlot`-level case of `crossToEnd_permT_right` where the rank-2
+  tensor's colors are only propositionally recast. -/
+lemma crossToSlot_permT_right_id {nA : ℕ} {c : Fin (nA + 1) → C} {cM cM' : Fin 2 → C}
+    (i : Fin (nA + 1)) (j : Fin 2) (hc : S.τ (c i) = cM' j)
+    (M : Tensor S cM) (hM : IsReindexing cM cM' (id : Fin 2 → Fin 2)) (t : Tensor S c) :
+    crossToSlot i j hc (permT (id : Fin 2 → Fin 2) hM M) t =
+      permT (id : Fin (nA + 1) → Fin (nA + 1))
+        (IsReindexing.on_id.mpr (fun a => by
+          by_cases ha : a = i
+          · subst ha
+            simpa using hM.2 (j.succAbove 0)
+          · simp [Function.update_of_ne ha]))
+        (crossToSlot i j (hc.trans (hM.2 j).symm) M t) := by
+  rw [crossToSlot_eq_crossToEnd, crossToSlot_eq_crossToEnd]
+  rw [crossToEnd_permT_right i j
+    (id : Fin 2 → Fin 2) id hM (by rfl)]
+  simp only [permT_permT]
+  apply permT_congr
+  · funext x
+    simpa only [Function.comp_apply, Function.comp_id, id_eq] using
+      congrFun Fin.append_castAdd_natAdd_eq_id ((Fin.cycleIcc i (Fin.last nA)).symm x)
+  · rfl
+
+/-- Cross contraction into a slot is `G`-equivariant, both constituents (`crossToEnd`, `permT`)
+  being so. -/
+@[simp]
+lemma crossToSlot_equivariant {nA : ℕ} {c : Fin (nA + 1) → C} {cM : Fin 2 → C}
+    (i : Fin (nA + 1)) (j : Fin 2) (hc : S.τ (c i) = cM j) (g : G)
+    (M : Tensor S cM) (t : Tensor S c) :
+    crossToSlot i j hc (g • M) (g • t) = g • crossToSlot i j hc M t := by
+  rw [crossToSlot_eq_crossToEnd, crossToSlot_eq_crossToEnd, crossToEnd_equivariant,
+    permT_equivariant]
+
+end Tensor
+
+end TensorSpecies

Physlib/Relativity/Tensors/Contraction/Products.lean

@@ -153,6 +153,23 @@ lemma contrT_prodT_snd {n n1 : ℕ} {c : Fin (n + 1 + 1) → C}
   rw [prodT_contrT_snd]
   simp
 
+/-- A contraction internal to the left factor commutes past the outer product with a right
+  spectator. The mirror of `prodT_contrT_snd`, obtained from it by `prodT_swap`, so the right-hand
+  side contracts the swapped product `prodT t1 t` and carries a block swap. -/
+lemma prodT_contrT_fst {n n1 : ℕ} {c : Fin (n + 1 + 1) → C}
+    {c1 : Fin n1 → C}
+    (i j : Fin (n + 1 + 1)) (hij : i ≠ j ∧ S.τ (c i) = c j)
+    (t : Tensor S c) (t1 : Tensor S c1) :
+    prodT (contrT n i j hij t) t1 =
+    permT _ IsReindexing.append_swap
+      (permT id (IsReindexing.append_succSuccAbove_natAdd i j) <|
+      contrT _
+        (Fin.natAdd n1 i)
+        (Fin.natAdd n1 j)
+        (by simpa using hij) <|
+      prodT t1 t) := by
+  rw [prodT_swap, prodT_contrT_snd]
+
 end Tensor
 
 end TensorSpecies

Physlib/Relativity/Tensors/Contraction/Pure.lean

@@ -133,6 +133,60 @@ lemma dropPair_permP {n n1 : ℕ} {c : Fin (n + 1 + 1) → C}
   · simp [hσ.2]
   · simp [hσ.2]
 
+/-- Two `permP`–`dropPair`–`dropPair` towers over a common pure tensor agree once their composite
+  slot maps agree pointwise. Comparing two orders of dropping two pairs of slots this way keeps
+  every slot map an opaque variable, so the comparison closes by unification rather than by
+  `whnf`-reducing the color and index-map composites. -/
+lemma permP_dropPair_dropPair_congr {nP nOut : ℕ}
+    {c : Fin (nP + 1 + 1 + 1 + 1) → C} {cOut : Fin nOut → C} (p : Pure S c)
+    (aL bL : Fin (nP + 1 + 1 + 1 + 1)) (habL : aL ≠ bL)
+    (a2L b2L : Fin (nP + 1 + 1)) (hab2L : a2L ≠ b2L)
+    (σ1L : Fin nOut → Fin nP)
+    (h1L : IsReindexing ((c ∘ Fin.succSuccAbove aL bL) ∘ Fin.succSuccAbove a2L b2L) cOut σ1L)
+    (aR bR : Fin (nP + 1 + 1 + 1 + 1)) (habR : aR ≠ bR)
+    (a2R b2R : Fin (nP + 1 + 1)) (hab2R : a2R ≠ b2R)
+    (σ1R : Fin nOut → Fin nP)
+    (h1R : IsReindexing ((c ∘ Fin.succSuccAbove aR bR) ∘ Fin.succSuccAbove a2R b2R) cOut σ1R)
+    (hslot : ∀ m : Fin nOut,
+      Fin.succSuccAbove aL bL (Fin.succSuccAbove a2L b2L (σ1L m)) =
+      Fin.succSuccAbove aR bR (Fin.succSuccAbove a2R b2R (σ1R m))) :
+    permP σ1L h1L (dropPair a2L b2L hab2L (dropPair aL bL habL p)) =
+    permP σ1R h1R (dropPair a2R b2R hab2R (dropPair aR bR habR p)) := by
+  funext m
+  simp only [permP, dropPair]
+  exact congr_mid (cOut m) p _ _ (hslot m) (h1L.preserve_color m).symm
+    (h1R.preserve_color m).symm
+
+/-- Two `permP`–`dropPair`–`permP` towers over a common pure tensor agree once their composite
+  slot maps agree pointwise. The one-contraction, inner-relabelled sibling of
+  `permP_dropPair_dropPair_congr`. -/
+lemma permP_dropPair_permP_congr {nP nOut mL mR : ℕ}
+    {c : Fin nP → C} {cL : Fin (mL + 1 + 1) → C} {cR : Fin (mR + 1 + 1) → C}
+    {cOut : Fin nOut → C} (p : Pure S c)
+    (σ0L : Fin (mL + 1 + 1) → Fin nP) (h0L : IsReindexing c cL σ0L)
+    (aL bL : Fin (mL + 1 + 1)) (habL : aL ≠ bL)
+    (σ1L : Fin nOut → Fin mL)
+    (h1L : IsReindexing (cL ∘ Fin.succSuccAbove aL bL) cOut σ1L)
+    (σ0R : Fin (mR + 1 + 1) → Fin nP) (h0R : IsReindexing c cR σ0R)
+    (aR bR : Fin (mR + 1 + 1)) (habR : aR ≠ bR)
+    (σ1R : Fin nOut → Fin mR)
+    (h1R : IsReindexing (cR ∘ Fin.succSuccAbove aR bR) cOut σ1R)
+    (hslot : ∀ m : Fin nOut,
+      σ0L (Fin.succSuccAbove aL bL (σ1L m)) = σ0R (Fin.succSuccAbove aR bR (σ1R m))) :
+    permP σ1L h1L (dropPair aL bL habL (permP σ0L h0L p)) =
+    permP σ1R h1R (dropPair aR bR habR (permP σ0R h0R p)) := by
+  funext m
+  simp only [permP, dropPair]
+  -- Each side is a two-`cast` tower, one cast from the inner `permP` and one from the outer
+  -- `permP`-after-`dropPair`. `LinearEquiv.cast` is defeq to `_root_.cast`, so drop to the plain
+  -- cast, fuse the tower with `cast_cast`, and close with the single-cast lemma `congr_mid`.
+  change _root_.cast _ (_root_.cast _ (p _)) =
+    _root_.cast _ (_root_.cast _ (p _))
+  simp only [_root_.cast_cast]
+  exact congr_mid (cOut m) p _ _ (hslot m)
+    ((h0L.2 _).trans (h1L.2 m))
+    ((h0R.2 _).trans (h1R.2 m))
+
 /-!
 
 ## Contraction coefficient
@@ -146,6 +200,16 @@ noncomputable def contrPCoeff {n : ℕ} {c : Fin n → C}
     (i j : Fin n) (hij : i ≠ j ∧ S.τ (c i) = c j) (p : Pure S c) : k :=
   S.contr (c i) (p i ⊗ₜ (LinearEquiv.cast (R := k) (by simp [hij.2]) (p j)))
 
+/-- `contrPCoeff` is insensitive to its proof arguments once the two contracted slots agree. Lets a
+  coefficient comparison rewrite the slots without a `congr` search through the proof fields. -/
+lemma contrPCoeff_congr {n : ℕ} {c : Fin n → C} (p : Pure S c)
+    {i i' j j' : Fin n} (hi : i = i') (hj : j = j')
+    {hij : i ≠ j ∧ S.τ (c i) = c j} {hij' : i' ≠ j' ∧ S.τ (c i') = c j'} :
+    p.contrPCoeff i j hij = p.contrPCoeff i' j' hij' := by
+  subst hi
+  subst hj
+  rfl
+
 attribute [-simp] LinearEquiv.cast_apply
 
 @[simp]

Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean

@@ -231,6 +231,38 @@ lemma succSuccAbove_natAdd_apply_castAdd {n n1 : ℕ}
   simp only [Fin.ext_iff, succSuccAbove_val, natAdd, castAdd]
   grind (splits := 20)
 
+/-- Reinserting a left-block survivor `a` after removing the `i`-th slot of the left block and the
+  `j`-th slot of the right block of `Fin ((nA + 1) + (nB + 1))`, the removal read at the contracted
+  length `(nA + nB) + 1 + 1`. Unlike `succSuccAbove_natAdd_apply_castAdd` the two holes straddle the
+  two blocks, so the statement carries the reshaping `Fin.cast`s. -/
+lemma succSuccAbove_castAdd_natAdd_apply_castAdd {nA nB : ℕ} (i : Fin (nA + 1)) (j : Fin (nB + 1))
+    (a : Fin nA) :
+    Fin.cast (show (nA + nB) + 1 + 1 = (nA + 1) + (nB + 1) by omega)
+        ((Fin.cast (show (nA + 1) + (nB + 1) = (nA + nB) + 1 + 1 by omega)
+            (Fin.castAdd (nB + 1) i)).succSuccAbove
+          (Fin.cast (show (nA + 1) + (nB + 1) = (nA + nB) + 1 + 1 by omega)
+            (Fin.natAdd (nA + 1) j)) (Fin.castAdd nB a))
+      = Fin.castAdd (nB + 1) (i.succAbove a) := by
+  apply Fin.ext
+  simp only [Fin.succSuccAbove_val, Fin.val_cast, Fin.val_castAdd, Fin.val_natAdd,
+    Fin.succAbove, Fin.lt_def, Fin.val_castSucc, Fin.val_succ, apply_ite Fin.val]
+  split_ifs <;> omega
+
+/-- Reinserting a right-block survivor, the mirror of
+  `Fin.succSuccAbove_castAdd_natAdd_apply_castAdd`. -/
+lemma succSuccAbove_castAdd_natAdd_apply_natAdd {nA nB : ℕ} (i : Fin (nA + 1)) (j : Fin (nB + 1))
+    (a : Fin nB) :
+    Fin.cast (show (nA + nB) + 1 + 1 = (nA + 1) + (nB + 1) by omega)
+        ((Fin.cast (show (nA + 1) + (nB + 1) = (nA + nB) + 1 + 1 by omega)
+            (Fin.castAdd (nB + 1) i)).succSuccAbove
+          (Fin.cast (show (nA + 1) + (nB + 1) = (nA + nB) + 1 + 1 by omega)
+            (Fin.natAdd (nA + 1) j)) (Fin.natAdd nA a))
+      = Fin.natAdd (nA + 1) (j.succAbove a) := by
+  apply Fin.ext
+  simp only [Fin.succSuccAbove_val, Fin.val_cast, Fin.val_castAdd, Fin.val_natAdd, Fin.succAbove,
+    Fin.lt_def, Fin.val_castSucc, Fin.val_succ, apply_ite Fin.val]
+  split_ifs <;> omega
+
 lemma succSuccAbove_natAdd_image_range_castAdd {n n1 : ℕ}
     (i j : Fin (n + 1 + 1)) :
     (succSuccAbove (n := n1 + n) (Fin.natAdd n1 i) (Fin.natAdd n1 j)) ''