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

[pariandrea]

Slot-addressed cross contraction and the general-rank raise/lower round trip

What the SUSY layer needs

The downstream SUSY layer (an N=1 Kähler stack) raises and lowers a named tensor index with the
Kähler metric g_{IJ̄}, and proves raising and lowering mutually inverse: raise (lower V) = V, the
operator form of g_{IJ̄} g^{J̄K} = δ_I^K on the physical domain. The existing tensor API does not
provide three things this requires.

• Raise/lower against a mixed-colour metric. g_{IJ̄} carries different colours on its two slots
  (chiral I, antichiral J̄), so lowering a chiralUp index yields an antiDown one. The existing
  dual toDualAtIndex contracts against the species metric, whose slots share a colour and whose
  survivor is pinned to S.τ (c i). It is the wrong shape.
• State the inverse law, a two-tensor contraction. The Kähler metric g and its inverse g⁻¹ are
  model-specific rank-2 tensors, and g · g⁻¹ = δ contracts one against the other. toDualAtIndex
  contracts a single tensor against the fixed species metric, so it cannot express a contraction of two
  such tensors. Upstream's rank-1 toDualMap_fromDualMap collapses the species metric with itself, not
  a metric against its inverse.
• Prove the round trip. raise ∘ lower = id chains (V·g)·g⁻¹ and regroups to V·(g·g⁻¹) so the
  pair collapses. Under raw contrT (prodT …) the intermediate lands at a cast-polluted colour and the
  two bracketings sit at different types, so the reassociation is not a direct same-typed equality
  without explicit transports.

Defining a different-colour dual is cheap, barely more than toDualAtIndex with a metric parameter.
The work is its law, that raising and lowering are mutually inverse for a mixed-colour metric.
That law is a two-tensor contraction plus a chain reassociation. This machinery is the algebra of the
inverse law, not the definition of the operation.

The two conventions

Every slot contraction has to decide where the surviving index lands. The PR carries both conventions,
and the names say which is which.

• crossToEnd i j contracts slot i of one tensor against slot j of another and deposits the
  result at the end: survivors of A, then survivors of B, gaps closed
  (Fin.append (cA ∘ i.succAbove) (cB ∘ j.succAbove) : Fin (nA+nB) → C). Appending survivors on the
  right is associative, which is what makes crossToEnd_chain_assoc reduce to a Fin.cast uniformly
  in rank and slot.
• crossToSlot i M performs the same contraction but keeps the replacement index at slot i
  (Function.update c i d, nothing else moved), the convention raising/lowering and toDualAtIndex
  need (T^μ{}_νρ ↦ T_μνρ). It is the front door: contract a distinguished rank-2 tensor (a metric,
  the unit tensor) at a named slot of an arbitrary tensor.

crossToSlot_eq_crossToEnd is the single place the two conventions meet, the cycle
(Fin.cycleIcc i (Fin.last nA)).symm that walks the result from the end back to slot i. The
docstrings lead with this result-to-end vs result-to-slot split: crossToSlot is the API,
crossToEnd the substrate it is built on.

The machinery

crossToEnd i j contracts slot i of one tensor against slot j of another. It adds no expressive
power over permT (contrT (prodT …)). It names the operation and normalises its output colour, so its
algebra (left-linearity, equivariance, chain associativity, the relabelling commutators) is proved once
against clean slot variables. This does not reduce associativity to count arithmetic: the central proof
still compares contraction coefficients, survivor maps, colour preservation, and count reindexings.
The gain is that these obligations are discharged once at a canonical public normal form rather than
rebuilt from raw casts by each consumer.

crossToSlot i M raises or lowers a named index by contracting against a rank-2 tensor
M : ![S.τ (c i), d], with the survivor colour d free. The SUSY layer consumes this directly:
KahlerMetric.lower and raise are crossToSlot i (g u) and crossToSlot i (gInv u) at a named slot.

crossToEnd_chain_assoc is the reassociation that makes the round trip provable. Built on it,
crossToEnd_round_trip_of_unit is the matched-pair collapse, and crossToSlot_raise_lower_roundtrip
is the round-trip theorem KahlerMetric.raise_lower consumes, with the metric's rightInverse field
(g · g⁻¹ = unit) as its hypothesis.

The round trip, parameterized by where the raised index lands

crossToSlot_raise_lower_roundtrip is the general-rank raise/lower round trip: contracting slot i
against a rank-2 tensor M, then against its inverse M', returns the tensor, at any rank and any
slot. It is parameterized by a target survivor colour e, propositionally equal to c i:

crossToSlot_raise_lower_roundtrip (i) (he : c i = e)
  (M : ![S.τ (c i), d]) (M' : ![S.τ d, e])
  (hM : crossToEnd i 0 M M' = δ)   -- unit tensor at colour e
  (t) :
  crossToSlot_ofColourEq i _ M' (crossToSlot i M t) = permT id _ t

M' and the surviving index land at e, not forced to c i. A consumer whose inverse metric already
sits at a fixed colour then supplies it directly, with no permT transport, and recovers the index at
that colour. The same-colour case e := c i — species metric, survivor pinned to S.τ (c i) — is the
he := rfl instance; there is one lemma, not a general one plus a specialized one.

The toDualAtIndex result

The species-metric case, both slots one colour and survivor pinned to S.τ (c i), is the degenerate
instance of the same machinery. On it, toDualAtIndex is crossToSlot i (metricTensor (S.τ (c i))),
and the double-dual round trip toDualAtIndex_toDualAtIndex (dualising a named index twice returns the
original, at general rank and arbitrary slot) is the e := c i (he := rfl) consumer of
crossToSlot_raise_lower_roundtrip. The index-notation elaborator (Tensors/Elab.lean) consumes
toDualAtIndex; toDualAtIndex_toDualAtIndex is a reusable result with no other in-tree consumer.

Relation to prodT + contrT

crossToEnd is definitionally permT … (contrT … (prodT t1 t2)). Two properties justify wrapping it.

• Composability. contrT of a prodT lands at colour Fin.append cA cB ∘ (succSuccAbove/cast composite), not a clean function of the survivors, so a second contraction needs hand-inserted
  recasts. crossToEnd normalises the output to
  Fin.append (cA ∘ i.succAbove) (cB ∘ j.succAbove) : Fin (nA+nB) → C. Without it
  crossToEnd_chain_assoc is not statable as a direct same-typed equality without explicit
  transports; its two sides sit at different cast-laden colours.
• Reusable laws. An inlined expression has no name and no lemmas. Identities relating contraction
  orders, or moving a relabelling through a contraction, would be re-derived per site against that
  site's indices and casts. Naming the operation proves them once.

crossToSlot_round_trip_of_unit is the forcing example. Raising a named slot with M₁ and lowering it
back with M₂ returns the original whenever crossToEnd M₁ M₂ is the unit tensor. The two slot
colours are independent, so this is the conjugate-metric case, and it reduces to
crossToEnd_chain_assoc at (nB, nC) = (0, 1), with the rank nA general.

Consumers

The rest of the API is justified by the SUSY layer.

• KahlerMetric.lower and raise are crossToSlot i (g u) and crossToSlot i (gInv u) at a named
  slot of an arbitrary-rank tensor.
• The rightInverse field states g · g⁻¹ = unit as a crossToEnd equation, in the metric's
  specification.
• raise_lower is a direct instance of crossToSlot_raise_lower_roundtrip. Because g_{IJ̄} and
  g^{J̄I} carry literal colours, raising the lowered index lands the survivor at the literal
  chiralUp, not at c i — the target-colour case (e = chiralUp) the round trip is parameterized
  for. The inverse metric g^{J̄I} enters at its native colour with no permT transport, and the
  survivor lands where raise's output type expects it. Threading e into the shared lemma is what
  absorbs the identity recasts that lower/raise introduce, which the intrinsic-colour layer does
  not normalise cheaply; without it the round trip had to be assembled at the crossToEnd level. So
  raise_lower is now a one-call crossToSlot-level instance, proved once at general rank.

toDualAtIndex_toDualAtIndex is the same lemma at the same-colour instance e := c i. Both consumers
draw on one crossToSlot_raise_lower_roundtrip.

Costs

Tensor S c is indexed by c. Type identity is definitional and colour equalities are propositional,
so transport across equal colours is Eq.rec/cast.

• Each renumbering of a surviving slot wraps its component in a LinearEquiv.cast, so components come
  out as stacked casts. pure_double_cast_congr proves that two double-cast component expressions
  agree once their source indices match (the cast proofs are then proof-irrelevant), and the two towers
  from the left- and right-associated orders agree once their composite leg-indices match
  (permP_dropPair_permP_congr, permP_dropPair_dropPair_permP_congr).
• The new modules add no set_option backward.isDefEq.respectTransparency false and no maxHeartbeats
  bump; crossToEnd_chain_assoc builds at default heartbeats. The pre-existing Products.lean
  spectator lemmas the chain reuses (e.g. prodT_contrT_snd) carry upstream's
  respectTransparency false, where a slot composite is defeq only under default transparency.

Scope

crossToEnd_chain_assoc is associativity of the canonical three-tensor chain. With μ the bond
between A and B and ν the bond between B and C, each a summed τ-dual pair:

A^{…μ…}  B_{μ}{}^{…}{}_{ν}  C^{ν}{}_{…}

A's attachment slot iA carries μ and may sit anywhere in A's index list. B's slot 0 carries
μ and its last slot carries ν; C's slot 0 carries ν. So B is contracted at both
endpoints, and only iA is free. Associativity (A·B)·C = A·(B·C) says that summing μ first or ν
first gives the same tensor. In index notation the two Einstein sums are independent and the expression
carries no brackets. The mathematical content is that the two independent contractions commute (the
two scalar contraction coefficients occur in opposite orders); most of the formal proof is the
positional, colour, and dependent-type bookkeeping that makes Lean see the two orders at compatible
types. It is not full associativity for arbitrary slots; a non-canonical slot on B or C is reached
by conjugating with the permT commutators. This is the shape the Kähler round trip and
toDualAtIndex_toDualAtIndex consume. The unit-tensor material is RCLike-valued and lives in its own
module, apart from the CommRing algebra.

---

Review order

Recommended reading, following the dependency order of the commits:

1. Reindexing.lean: the Fin block-map and induced-permutation lemmas the contraction rests on.
2. Contraction/Basic.lean and Contraction/Products.lean: contrT_cast and the spectator
   commutations used by the chain lemmas.
3. Contraction/CrossContraction.lean: crossToEnd, crossToSlot, crossToSlot_eq_crossToEnd, and
   the algebra (crossToEnd_chain_assoc is the centre).
4. Contraction/UnitTensorContraction.lean: the unit-collapse identities,
   crossToEnd_round_trip_of_unit, and crossToSlot_raise_lower_roundtrip.
5. Contraction/MetricDual.lean: toDualAtIndex and its double-dual round trip, the same-colour
   instance of the round-trip lemma.

---

Files changed

Legend: bold = public API; plain = private proof helper.

Physlib/Relativity/Tensors/Contraction/CrossContraction.lean (new)

The primitive, its linear and associative algebra, contraction at a named slot, and the bridge between
the two survivor conventions.

• crossToEnd: the slot-addressed cross contraction, result at the end (def).
• crossToEnd_two: at rank two on each factor, the (last, 0) contraction is a plain contrT
  of the product on the canonical middle slots. It discharges the slot arithmetic once, so
  contrT-level identities lift to crossToEnd by one rewrite.
• crossToEnd_add_left / _smul_left / _sum_left: additivity, scalar-multiplication, and
  finite-sum distributivity in the left factor.
• crossToEnd_equivariant: commutes with the G-action.
• crossToEnd_chain_assoc: associativity of the canonical chain A^{…μ…} B_{μ}{}^{…}{}_{ν} C^{ν}{}_{…} ((A·B)·C = A·(B·C)), with A's attachment slot free and B/C pinned to their
  endpoints, with explicit count reindexings for the regrouped final survivor count and the
  intermediate B·C tensor.
• crossToEnd_permT_left: move an arbitrary relabelling of the left factor through the
  contraction, sending the contracted slot to σ i and relabelling survivors by the induced
  permutation.
• crossToEnd_permT_left_of_fix / _permT_right_of_fix: the same for a relabelling that fixes
  the contracted slot.
• IsReindexing.crossToSlot_cycle: the survivor relabelling (inverse cycle [i, last]) for
  crossToSlot.
• crossToSlot: contract slot i against slot 0 of a rank-2 M : ![S.τ (c i), d] and rotate
  the survivor back to i (def).
• crossToSlot_eq_crossToEnd: the bridge, crossToSlot i M t as a cycle of crossToEnd i 0 t M.
• crossToSlot_ofColourEq: crossToSlot absorbing a propositional first-colour equality, so M
  may enter at a colour equal only up to an involution (def). crossToSlot_ofColourEq_apply is its
  applied form.
• Private helpers: crossToEnd_reinsert_castAdd / _reinsert_natAdd (survivor reinsertion after
  dropping a slot from each factor); contrPCoeff_congr (the contraction coefficient is insensitive to
  its proof arguments once the two contracted slots agree); crossToEnd_chain_assoc_survivor_arith
  (the arithmetic core of the survivor-slot comparison in crossToEnd_chain_assoc); the cast-tower
  congruence pure_double_cast_congr and the survivor-tower closers permP_dropPair_permP_congr /
  permP_dropPair_dropPair_permP_congr.

Physlib/Relativity/Tensors/Contraction/UnitTensorContraction.lean (new)

The unit tensor is the identity for slot contraction; the raise/lower round trips. ([RCLike k].)

• IsReindexing.moveLast: the reindexing carrying slot i to the survivor tail.
• crossToEnd_last_unitTensor: contracting the last slot against unitTensor returns the
  tensor, slot carried to the end (boundary case).
• crossToEnd_unitTensor: the unit tensor is an identity for crossToEnd at any slot.
• crossToEnd_round_trip_of_unit: two contractions against a pair that collapses to the unit
  tensor return the original tensor, up to the cycle moving the round-tripped slot back.
• crossToSlot_permT_right_id: an identity recast of the rank-2 tensor in a crossToSlot becomes
  the corresponding identity recast of the output.
• crossToSlot_round_trip_of_unit: the round trip in crossToSlot form (raw permT-cast
  statement).
• crossToSlot_raise_lower_roundtrip: the same in crossToSlot_ofColourEq form, M' entering at
  its natural colour and the survivor landing at a target colour e = c i; the shape
  KahlerMetric.raise_lower and MetricDual.toDualAtIndex_toDualAtIndex consume.
• Private helpers: pure_cast_congr (Pure.congr_mid wrapper); crossToEnd_prodT_unitTensor
  (rank-one spectator seed); crossToEnd_unitTensor_slot / crossToEnd_round_trip_of_unit_slot
  (restatements at a propositionally-last slot); succAboveInduced_cycleIcc_symm (the inverse cycle
  induces the identity survivor permutation).

Physlib/Relativity/Tensors/Contraction/MetricDual.lean (new)

Named-index dual via metric contraction, on crossToSlot. Imports UnitTensorContraction and
MetricTensor.

• toDualAtIndex: dualise a named index against the species metric,
  crossToSlot i (metricTensor (S.τ (c i))) (the same-colour, survivor-pinned case). Consumed by the
  index-notation elaborator.
• toDualAtIndex_toDualAtIndex: dualising a named index twice returns the original tensor, up to
  the colour cast from the two Function.updates. The e := c i instance of
  crossToSlot_raise_lower_roundtrip; general rank, arbitrary slot.

Physlib/Relativity/Tensors/Reindexing.lean

New Fin block-map and induced-permutation lemmas, plus an id-witness helper. IsReindexing itself
is unchanged (still def := Function.Bijective σ ∧ ∀ i, c (σ i) = c1 i).

• idReindex: reducible id reindexing witness from a pointwise colour equality. Its reducibility
  keeps the resulting proof matchable under instances transparency by the permT/crossToEnd
  rewrite lemmas.
• Fin.append_swap_val / append_castAdd_cast_natAdd_val / append_castAdd_natAdd_cast_val: the
  .val of the product and contraction block maps as explicit piecewise formulas, so omega closes
  slot arithmetic without exponential split_ifs.
• Fin.append_castAdd_natAdd_eq_id: the natural-order block map is the identity (id
  specialisation of Mathlib's Fin.append_castAdd_natAdd).
• Fin.append_succAbove_const_eq_cycleIcc: listing the i.succAbove survivors then i is the
  cycle [i, last].
• Fin.succAboveInduced / succAbove_succAboveInduced / succAboveInduced_bijective /
  succAboveInduced_id: the map on the i.succAbove survivors of slot i induced by a bijection
  σ, landing in the complement of σ i. succAbove_succAboveInduced_of_fix gives its defining
  property when σ fixes i.
• Fin.eq_of_bijective: a bijection Fin m → Fin n forces m = n.

Physlib/Relativity/Tensors/Contraction/Products.lean

• prodT_contrT_fst: a contraction internal to the left factor commutes past an outer product with
  a right spectator (mirror of prodT_contrT_snd via prodT_swap).
• contrT_prodT_fst: the same read in reverse.

Physlib/Relativity/Tensors/Contraction/Basic.lean

• contrT_cast: commute a Fin.cast reshape of the rank through contrT.

Physlib/Relativity/Tensors/Dual.lean and Physlib/Relativity/Tensors/Elab.lean

toDualAtIndex lives in MetricDual.lean; Dual.lean carries only the rank-1
toDual/toDualMap/fromDualMap family (unchanged from upstream). Elab.lean's import is repointed
from Dual to MetricDual (its only use was toDualAtIndex).

Physlib.lean

Imports of the new CrossContraction, UnitTensorContraction, and MetricDual modules.

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

[nateabr]

Hi I had a look through your work and it looks great! I just had a few comments that might help.

I think in general it might be worth considering that these are foundational files and will probably be used as we build up more physics in relativity so compilation times would be a good thing to think about as we scale :)

[nateabr]

I'm a bit concerned about this import being here, is it a good design choice to import high level algebra into a a basic module like this? I think down the line this might cause some issues with compilation as this file is imported in many other files.

Furthermore I do believe the lemmas you have placed in this file ideally should've been in bond.lean.

[nateabr]

Do the lemmas above need to be private? They seem quite helpful maybe you should move them to reindexing.lean so they can be used later.

[nateabr]

this could also be made public and moved to reindexing.lean?

[nateabr]

For the proofs above I think its worth heavily refactoring them(especially since you needed to increase the heartbeats). Particularly the generalize blocks.

Maybe try isolating the index logic into standalone lemmas (consider adding them to reindexing.lean).

[nateabr]

Overriding the transperency like this can be very brittle especially during mathlib bumps.

Could we try replacing the raw rw with a congruence-based approach instead? Using something like refine or explicit congruence lemmas (which are available in reindexing.lean I think) usually unifies these dependent types naturally without needing to override transparency or target specific coordinates.

[nateabr]

also upon reading my comments I believe have come across a little rude, I apologize for this :(

awaiting-author

[pariandrea]

also upon reading my comments I believe have come across a little rude, I apologize for this :(

awaiting-author

Not rude at all! I am already working on them. Thank you very much for such a quick feedback!

[jstoobysmith]

Would this work with just (nA +1) and (nB + 1), I don't see why you need the additional 1+.

[jstoobysmith]

Is it worth naming this bondT (or just bond then?)

[jstoobysmith]

To ask a more general question: What is does this give you which normal tensor contraction doesn't. For example Aⁱⱼ Bʲₖ can already be concisely written using index notation as {A | i j ⊗ B | j k}ᵀ. The problem with this bond things is that they don't correspond to anything in index notation, so everytime one uses them it would have to be written out explicitly. I wonder if it is better to just improve the API around the existing definitions rather than introducing new ones here.

[nateabr]

@jstoobysmith even i was thinking about this and you are right that this doesn't have an index notation anologue, but maybe its similar to operator algebra?

But moreover practically, the use case that jumped out to me is if we need to chain many contractions together of tensors of different rank, leans system might fight against us and we probably wont be able to use rwand proof's might explode in length as the tensor rank's increase.

However, I'm not a 100% sure, maybe there's some lean metaprogramming that can help us here?

[pariandrea]

@jstoobysmith You're right that for a single contraction the index notation already wins: Aⁱⱼ Bʲₖ is just {A | i j ⊗ B | j k}ᵀ.
@nateabr As you said, I was trying to address the chain of tensors problem.
Each contraction tears two indices out and the survivors keep their old positions, so you're left with gaps in the numbering. One contraction is fine, but the next one inherits those gaps, and every further link adds more, so you paste a Fin.cast correction at each step, the corrections stack instead of cancelling, and eventually rw can't fire because it has to see through the whole pile.

The bond fixes a standard slot layout for every tensor: the two indices used for contracting always sit at fixed positions, first slot and last slot, with everything else in the middle. The contraction operation is defined so that its output is put back into this same standard layout. So the result of one contraction is already in exactly the form the next contraction expects, and no correction is needed between steps. The output of a contraction is again a valid input.

That said, I fully agree it's not ideal that this has no index-notation analogue. I'm currently exploring whether the current physlib machinery can be extended to solve this chaining problem.

[jstoobysmith]

Actually, I think it does have an index notation analog! It's just something akin to mulVec e.g. we could write

 {A *ᵥ B | i k}ᵀ =  {A | i j ⊗ B | j k}ᵀ

etc. Where does the name bond come from here?

[pariandrea]

The name comes from tensor networks (https://tensornetwork.org/mps/).

I adopted it somewhat loosely, as I am not familiar with tensor network theory.

If we consider tensors that are represented by matrices A | i j and B | j k, contracting the last index of A and the first of B is just the row by column product.

[jstoobysmith]

Maybe worth extracting and putting into Reindexing

[jstoobysmith]

Likewise with the other large proofs in permT's.

[jstoobysmith]

Is it worth naming this bondT (or just bond then?)

[jstoobysmith]

This I think already exists, though if it doesn't this file is not the right place.

[jstoobysmith]

Lift to a bilinear map? Then you don't need all of the proofs below.

[jstoobysmith]

I'm slightly confused about the difference between these. But maybe I can ask, will we only ever use these for nA, nB, nV and nM = 0? or are there application when this is not the case?

If the former, I think the Api would be simplified a lot by making this restriction (and it would let us proof a lot more about these things I think).

[jstoobysmith]

Also, I think we can make these doc-strings less verbose as well (I don't think AI does a particularly good job at writing these).

[pariandrea]

Yes that is true.

[pariandrea]

I am currently writing a crosscontraction file which is just contrT and prodT on a pair of tensors where we prove associativity and other basic properties. This is very useful when we want to raise and lower indices with metric tensors.

Example: crossContrT 2 0 R u reads back as R_{μνρσ} uᵖ

Bond becomes a specific case where we have a chain of tensors contracted at extremal indices such as a chain of lorentz transformations. Ideally, we would have a general rank tensor algebra that does not need Fin.cast at every step. This turns out to be very challenging. I have not replied to the comments yet because I am still exploring a few possibilities.

[jstoobysmith]

Sounds good! I think you already know this, but just in case not: this (which is now merged with toDualAtIndex) #1348 allows you to rise and lower indices more easily, with the index notation.

[pariandrea]

Rescoping

I've replaced the PR description with a rescoped version (see the updated body).

Original scope. The goal was a general-rank tensor algebra to solve the Fin-cast problem that
appears when chaining tensor contractions: contrT of a prodT lands at a cast-polluted colour, so a
second contraction needs hand-inserted recasts and the two bracketings of a chain sit at different
types. Doing this in full generality turned out to be very hard.

New scope. I've cut the PR down to exactly what my SUSY (N=1 Kähler) work needs, and no more.

Summary

The PR adds crossContrT i j, a slot-addressed contraction of one tensor's slot i against another's
slot j, which normalises its output colour to a clean Fin (nA+nB) → C so a following contraction
composes against plain slot variables with no hand-inserted colour recasts. Built on it:

• contrAtSlot i M: contract a named index against a compatible rank-2 tensor M, with the
  replacement colour parameterised by d. Taking M to be a metric implements raising or lowering;
  the Kähler lower / raise use exactly this operation.
• crossContrT_chain_assoc: the reassociation used to prove raise ∘ lower = id. In raw
  contrT/prodT form the two bracketings have different cast-laden output types, so their equality
  needs a bespoke transport. The canonical output of crossContrT gives this reassociation a stable,
  reusable statement with its remaining reindexings explicit.
• crossContrT_crossContrT_of_unit_at: the round-trip theorem the metric inverse law g · g⁻¹ = δ
  feeds.

The general-rank named-index dual (toDualAtIndex reimplemented on this machinery, plus its
double-dual round trip) is a self-contained extra. The SUSY work does not use it, and it sits in the
final commit, which can be dropped to leave a machinery-only PR that still builds.

What this does not solve

crossContrT normalises the survivor count and colour layout of each individual contraction: inputs
with nA+1 and nB+1 slots return the canonical nA+nB survivors. It cannot make the counts produced
by two bracketings of a chain, (nA+nB)+nC and nA+(nB+nC), definitionally equal. Reassociation
therefore still needs explicit count reindexings. In crossContrT_chain_assoc these include the outer
permT (Fin.cast (nA+nB+nC = nA+(nB+nC))) on the result and an inner count reindexing that puts the
intermediate B·C contraction into the shape expected by the outer contraction.

crossContrT itself also inserts Fin.casts internally to reshape the product
(nA+1)+(nB+1) into the (nA+nB)+1+1 shape contrT needs, then transports the result to its canonical
colour function. These transports are packaged by the definition; they are not deleted. The current
round-trip consumer simplifies the resulting reindexings and discharges the final equality with
permT_congr.

Naming the operation does not remove the count cast, but it is still worthwhile.

• It localises the recurring fibre-level colour transports inside the definition and reusable lemmas.
  Those transports are Eq.rec / LinearEquiv.casts on components that block defeq and stack; they
  still exist internally, because permT itself is implemented using component casts. Callers work
  against one canonical survivor layout instead of rebuilding a raw-to-canonical transport tower at
  every use site.
• It gives downstream statements a stable public normal form. raise ∘ lower = id and the
  double-dual can be expressed with their residual transports explicit rather than with a bespoke
  tower derived from the syntax of raw contrT/prodT. Chain reassociation carries count-level
  Fin.cast reindexings; the double-dual instead retains an identity permT carrying the colour
  equality generated by Function.update and τ ∘ τ = id.
• It turns the algebra into reusable lemmas. Left-linearity, equivariance, the permT commutators, and
  crossContrT_chain_assoc are proved once against clean slot variables. The associativity proof still
  compares contraction coefficients, survivor maps, colour preservation, and the count reindexings;
  the gain is that this work is centralised instead of re-derived per consumer against concrete casts.
• It bounds and localises the residual reassociation cost. The exposed transports are a controlled
  collection of permT (Fin.cast …) reindexings whose colour-preservation proofs are determined by the
  canonical survivor order. The current round-trip proof simplifies them through the permT algebra
  and closes the final reindexing equality with permT_congr. Separate propositional colour equalities
  can still produce identity-permT transports.

So crossContrT does not eliminate the Fin-cast problem or reduce associativity to arithmetic. It
chooses a canonical public type for each cross contraction, proves the raw-to-canonical transports in
one place, and supports reusable algebra at that normal form. Count parenthesisation and its associated
colour-preservation proofs remain explicit when contractions are reassociated.

[nateabr]

will get to this @pariandrea if Joseph doesn't beat me to it, please bare with me

Thanks for your work :))

[jstoobysmith]

Could you give an example here of where you want to use crossContrT, but where index notation would not work?

[jstoobysmith]

Could you give an example here of where you want to use crossContrT, but where index notation would not work?

Maybe I'm asking here: what is your exact use case for these functions. Above you write: R_{μνρσ} uᵖ, but our index notation already covers this.

What is the situation which index notation does not cover concretely? Is it something which goes beyond index notion even on pen and paper, or is it something which is a limitation of the index notation in Physlib.

[pariandrea]

I have rescoped the branch and rewritten the description.
R_{μνρσ} uᵖ is done by the index notation.
The problem I wanted to solve is to prove some lemmas such as associativity for index contraction.
This is in general hard so the problem I try to solve here is simply:

(t·g)·g⁻¹ = t·(g·g⁻¹)

for a general rank tensor t.

The round-trip lemma:

lemma crossContrT_crossContrT_of_unit_at {nA : ℕ} {c : Fin (nA + 1) → C} {d : C}
(i : Fin (nA + 1))
(M₁ : Tensor S ![S.τ (c i), d]) (M₂ : Tensor S ![S.τ d, c i]) ...
is stated for arbitrary rank nA + 1 at an arbitrary slot i. Index notation is syntactic, one index symbol is written per slot, so a tensor of variable rank has no notation expression, and there is no way to name "slot i". This lemma feeds toDualAtIndex_toDualAtIndex in MetricDual.lean, which generalises the upstream/master round trips (toDualMap_fromDualMap, fromDualMap_toDualMap, rank 1 slot 0) to any rank and any named slot.

For the concrete rank-one Kähler application index notation can describe the diagram, e.g. schematically {V | I ⊗ g | I J̄}ᵀ, but that elaborates to raw contrT (prodT …) at a non-canonical colour, and the round trip still has to be proved against that term. The cost of doing this per fixed rank is visible on master: toDualMap_fromDualMap is a ~35-line transport computation needing respectTransparency false, for rank 1 and slot 0 only. Each fixed-rank instance reproduces that grind with its own transports.

My logic is to give a cross contraction a canonical end form: survivor indices of A followed by survivor indices of B, relabelled without gaps. However, I am unsure crossContrT is the right abstraction. This canonical ordering always puts the replacement index in the last slot, whatever slot was contracted: contracting slot i = 1 of [c₀, c₁, c₂, c₃] against a rank-2 M = [τ(c₁), d] gives [c₀, c₂, c₃, d], not [c₀, d, c₂, c₃]. That ordering is what makes crossContrT_chain_assoc statable at general rank: appending survivors on the right is itself associative, so both bracketings produce the same survivor list in the same order.

But raising and lowering needs the index in place. It wants the result colour Function.update c i d: slot i relabelled, nothing moved, as in T^μ_νρ ↦ T_μνρ. This is the type of contrAtSlot, and the one the Kähler raise/lower and toDualAtIndex need.

So I proved associativity in the appended-survivor convention and the raise/lower round trip in the in-place convention, and the friction between the two is where the remaining complexity lives: contrAtSlot is crossContrT plus the cycle rotating d back to slot i, and that rotation resurfaces in every lemma connecting the two layers. Honestly, I have spent a long time trying to come up with something better and I might need some guidance. Otherwise, we can also postpone this and work at fixed rank until a better design comes up.

[jstoobysmith]

Opps: commented this before I saw your reply

Sorry for the noise, but let me answer my own question here. I think the real motivation for defining this general construction is that it is often the case that we have some special tensors in a theory, for example, the unit tensors, the metric tensors, or the Kahler metric tensors. In general, we want to contract those tensors and specific indices of those tensors with specific indices of other, often arbitrary, tensors. The mechanism that's in this pull request is what gives us the framework to do that.

You could use the definitions we have already to do this. However, because these sorts of manipulations are so common, it is useful to have a general way to construct these index contractions. A specific example is the toDualIndexAt, which now uses this function as a base. This is really one of the main motivations behind defining it: it allows you to define toDualIndexAt, but also other things which are similar.

If this is correct, I think we need to include this in the doc string and consider how we can frame things around this, because this is the clear motivation behind this. I don't think the motivation about needing to contract to indices of two different tensors is as strong.

[jstoobysmith]

My logic is to give a cross contraction a canonical end form: survivor indices of A followed by survivor indices of B, relabelled without gaps. However, I am unsure crossContrT is the right abstraction. This canonical ordering always puts the replacement index in the last slot, whatever slot was contracted: contracting slot i = 1 of [c₀, c₁, c₂, c₃] against a rank-2 M = [τ(c₁), d] gives [c₀, c₂, c₃, d], not [c₀, d, c₂, c₃]. That ordering is what makes crossContrT_chain_assoc statable at general rank: appending survivors on the right is itself associative, so both bracketings produce the same survivor list in the same order.

If we instead focus on abstracting toDualAtIndex for an arbitrary two-index tensor, then I think this might be a better abstraction, as it seems to cover most of the cases that we want. Why do we need crossContrT_chain_assoc?

[pariandrea]

Yes, contracting the special tensors of a theory (unit, metric, Kähler metric) against named slots of arbitrary tensors is the right description of the use case, and I'll lead the docstrings with it.

One precision: the theorems are one level more general than the metric examples. The round trip is proved once, for any matched pair of rank-2 tensors that collapses to the unit tensor (crossContrT_crossContrT_of_unit_at), at any colour pair, any rank, any slot.

Example of crossContrT_crossContrT_of_unit_at is T^{μνρ} (M₁)_{νσ} (M₂)^{στ} = δ_ν^τ T^{μνρ} = T^{μτρ}

The species metric (toDualAtIndex_toDualAtIndex) and the Kähler metric (raise/lower, where the two slots have different colours, the reason d is free in contrAtSlot) are instances. Any future metric-like pairing gets its round trip from the same lemma.

That generality comes from crossContrT_chain_assoc: associativity of a contraction chain, (A·B)·C = A·(B·C). The two bracketings land at differently grouped types, (nA + nB) + nC vs nA + (nB + nC), but since crossContrT appends survivors on the right, both sides produce the same survivor list in the same order, so the lemma only needs the regrouping cast, at any rank, any slot. The round trip runs on this: raising then lowering is (t·g)·g⁻¹, and g·g⁻¹ = δ can't fire until you regroup to t·(g·g⁻¹).

On "you could use the definitions we have already", at fixed rank, yes: that's what toDualMap_fromDualMap on master does, ~35 lines of transports doing that regrouping by hand, rank 1 slot 0 only (and toDualAtIndex has no lemmas at all). At general rank the raw bracketings sit at non-canonical colours and the reassociation isn't statable as one lemma; the canonical output colour is what turns it into a cast.

The issue with general rank crossContrT_chain_assoc is that it forces the following two conventions:

Convention 1 — survivors appended (what crossContrT does). Output = A's surviving slots, then B's surviving slots, gaps closed. The new index always ends up last:

contract slot 1 of [c₀, c₁, c₂, c₃] against [τc₁, d] → [c₀, c₂, c₃, d]

Convention 2 — index in place (what contrAtSlot exposes). Output = same layout as the input, only the contracted slot's colour changes:

contract slot 1 of [c₀, c₁, c₂, c₃] against [τc₁, d] → [c₀, d, c₂, c₃]

So this framework looks messy because for the associativity we need the first convention and for raise/lower we need the second.
The alternative (I have not tried) is to keep only convention 2 and prove associativity at fixed ranks for every rank tensor we need.

[jstoobysmith]

Is there an easy way to see why associatively forces the first convention?

[pariandrea]

I do not think that it is impossible to prove without the convention.
The chain_assoc proof is easier when we know where the contraction ends up.

Convention 1
append — b always lands last:
contract slot 0: [a₁, a₂, b] b at position 2
contract slot 2: [a₀, a₁, b] b at position 2

Convention 2
in place — b lands where the contracted slot was:
contract slot 0: [b, a₁, a₂] b at position 0
contract slot 2: [a₀, a₁, b] b at position 2

If we use the physically better convention 2 the colour position will depend on the indices we contract.
I could try to reprove chain_assoc without convention 1.
Alternatively, we could work at the fixed ranks and prove something like crossContrT_chain_assoc_rank_one which should be easy in either the conventions.
This would be better than index notation becomes it would be more general and it could be used to prove round trips for general metric types such as Kahler metric and it would strip away the index bookkeeping complexity of the currect toDualAtIndex.

[jstoobysmith]

I think convention 2 only works anyway in the case where one of the tensors is of rank 2, maybe this assumption is enough to simplify the calculation enough?

[pariandrea]

Fixing the metric to rank 2 doesn't simplify chain_assoc. The generality that makes that proof hard lives in the general-rank tensor t of (t·g)·g⁻¹ = t·(g·g⁻¹), not in the metric; g and g⁻¹ are already rank 2. chain_assoc is a specific chained configuration A—B—C: A's slot iA is free and possibly interior, and contracts with B's first slot; B's other contracted slot lands at the last position of A·B, which then contracts with C's locked first slot. B and C are pinned to their chain endpoints, so only A carries the arbitrary rank and the free slot. Constraining B and C to rank 2 leaves the hard part untouched: the complexity is tracking A's surviving slots around an interior contraction at symbolic rank.

Following your point that the abstraction is contracting special tensors at named slots, I've reframed the API so the names carry the design. No behaviour change beyond the renamed identifiers.

The two conventions

Every slot contraction has to decide where the surviving index lands, and the names now say which.

• crossContrT → crossToEnd. Deposits the result at the end (survivors of A, then survivors of B, gaps closed). This is what makes crossToEnd_chain_assoc easier to prove because appending survivors on the right is associative.
• contrAtSlot → crossToSlot. Keeps the result at the slot (Function.update c i d, nothing else moves), as in T^μ_νρ ↦ T_μνρ — the convention raising/lowering and toDualAtIndex need, and the front door.

The connecting lemma

crossToSlot_eq_crossToEnd :
  crossToSlot i M t = permT (Fin.cycleIcc i (Fin.last nA)).symm _ (crossToEnd i 0 t M)

The single place the two conventions meet: the cycle that walks the result from the end back to slot i.

Structure

• crossToEnd — the underlying cross contraction, with crossToEnd_chain_assoc and crossToEnd_round_trip_of_unit (the matched-pair collapse, at any rank and any slot).
• crossToSlot — the front-door operation, with crossToSlot_eq_crossToEnd connecting the two and crossToSlot_raise_lower_roundtrip built on the crossToEnd engine. That round trip is parameterized by a target survivor colour e = c i: the inverse metric and the raised index land at e, so a consumer whose inverse metric sits at a literal colour supplies it with no permT transport.
• toDualAtIndex — the species-metric instance of crossToSlot; its double-dual round trip is the same-colour (e := c i) consumer of the one round-trip lemma.
• Docstrings lead with "result-to-end vs result-to-slot", crossToSlot as the API and crossToEnd as the substrate.

What consumes this downstream

The N=1 Kähler layer is the live consumer, exercising exactly the generality the species metric does not:

• KahlerMetric.raise/lower are crossToSlot against g_{IJ̄} and its inverse, at a named slot of an arbitrary-rank tensor. That metric carries two different colours (chiralDown, antiDown), so the replacement colour differs from τ(c i) , the free-d case the same-colour metric never hits.
• KahlerMetric.raise_lower : raise (lower t) = t is a direct instance of crossToSlot_raise_lower_roundtrip. Because g_{IJ̄} and g^{J̄I} carry literal colours, raising lands the survivor at the literal chiralUp (e = chiralUp), the inverse metric enters at its native colour, and the inverse law g · g⁻¹ = δ is the metric's rightInverse field. Proved once at general rank.
• The F-term potential consumes raise directly: g^{J̄I} D_I W D̄_J̄ W̄.