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

[pariandrea]

Slot-addressed cross contraction, and toDualAtIndex at every rank

Contracting slot i of one tensor against slot j of another is prodT then contrT. Written
that way, every call site has to locate the two post-product slots, discharge the distinctness and
τ-duality goals, and repair a cast-polluted output colour before the next step. This PR names that
operation, fixes its output colour, and proves its algebra once.

Two conventions are provided, and the names say which is which.

• crossToEnd i j deposits the survivor at the end: survivors of A, then survivors of B,
  gaps closed (Fin.append (cA ∘ i.succAbove) (cB ∘ j.succAbove)). Appending on the right is what
  makes the chain regrouping statable uniformly in rank and slot.
• crossToSlot i j M keeps the replacement index at slot i (Function.update c i d,
  nothing else moves) — T^{μ}{}_{νρ} ↦ T_{μνρ}. This 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 meet, the inverse of the cycle [i, last].

The payoff is crossToSlot_raise_lower_round_trip: for any matched pair of rank-2 tensors
collapsing to the unit tensor, raising then lowering a named index is the identity, at any rank and
any slot, with all four colours threaded propositionally so a caller whose metric sits at a literal
colour supplies it with no transporting permT. On master this result exists only at rank 1, slot 0
(toDualMap_fromDualMap), by 30 lines of hand transports.

When the pair collapses in both orders the two contractions are mutually inverse, and
crossToSlotEquiv bundles them as a ≃ₗ between the two colour assignments. The species-metric
case is the instance: toDualAtIndex is reimplemented on crossToSlot, its double-dual round trip
is proved at every rank, and it is upgraded from a →ₗ to a ≃ₗ.

API changes to existing declarations

Reviewers should decide on these first.

The trade: eleven declarations go (ten in Dual.lean, one in Reindexing.lean), and what replaces
them is a single round trip holding at every rank and every named slot, plus the general crossToSlot
it is an instance of. The deleted toDualMap_fromDualMap also carried master's
set_option backward.isDefEq.respectTransparency false on Tensors/Dual.lean:62; the general-rank
proof needs no transparency override, so the branch removes that one and adds none.

Declaration	File	Change
toDualAtIndex	Tensors/Dual.lean	was a →ₗ at every rank with no lemmas; now a ≃ₗ, defined via crossToSlot. The map itself is split off as toDualMapAtIndex (what Elab.lean's jiggle now emits).
toDualMap, fromDualMap, toDual (+ toDualMap_apply, fromDualMap_apply, toDualMap_fromDualMap, fromDualMap_toDualMap, fromDualMap_eq_permT_toDualMap, toDualMap_eq_permT_fromDualMap, toDual_equivariant)	Tensors/Dual.lean	removed, superseded. They are the rank-1, slot-0 case of toDualMapAtIndex / toDualAtIndex, with no in-tree consumers. Note the instance is not literally the old statement: at n = 1, i = 0 the colour list is Function.update ![c] 0 (S.τ c) rather than ![S.τ c]. Happy to restore them as thin wrappers if you would rather keep the rank-1 names.
IsReindexing.contr_two_rotate	Tensors/Reindexing.lean	removed. It existed only to state the old toDualAtIndex's output permutation; IsReindexing.crossToSlot_cycle replaces it.

Declarations added

Tensors/Contraction/CrossToEnd.lean (new)

• crossToEnd — the slot-addressed cross contraction, as a curried bilinear map. Additivity,
  scalar multiplication and sums in either argument come from the LinearMap structure.
• crossToEnd_two — at rank two on each factor, a plain contrT of the product on slots 1, 2.
  Discharges the concrete slot arithmetic once so contrT-level identities lift by one rewrite.
• crossToEnd_equivariant — commutes with the G-action.
• crossToEnd_assoc_rankTwo — rebracket the chain A —(iA·0)— B —(last·0)— C for rank-two B, C,
  up to permT id. Not full associativity: only A's attachment slot is free.
• crossToEnd_permT_left / crossToEnd_permT_right — move a relabelling of either factor through
  the contraction, the contracted slot moving with it. The survivor relabelling σ' is a caller
  argument constrained by the square (σ i).succAbove ∘ σ' = σ ∘ i.succAbove.

Tensors/Contraction/CrossToSlot.lean (new)

• IsReindexing.crossToSlot_cycle — the output colour list, after the survivor is rotated back.
• crossToSlot — the result-to-slot contraction against a rank-2 tensor; raising and lowering a
  named index.
• crossToSlot_eq_crossToEnd — the bridge between the two conventions.
• crossToSlotInv — the returning contraction, with the round trip's two-Function.update colour
  cast absorbed so a round trip is cast-free at both ends.
• crossToSlot_permT_right_id — an identity reindexing of the rank-2 tensor passes through.
• crossToSlot_equivariant — commutes with the G-action.

Tensors/Contraction/UnitTensorContraction.lean (new, [RCLike k])

• crossToEnd_unitTensor — the unit tensor is an identity for crossToEnd at any named slot.
  (Private steps: crossToEnd_prodT_unitTensor, crossToEnd_unitTensor_slot.)
• IsReindexing.unitTensor_pair — the colour list a matched rank-2 pair contracts to.
• crossToEnd_round_trip_of_unit_slot — the round trip in result-to-end form.
• crossToSlot_raise_lower_round_trip — the round trip in result-to-slot form, every colour
  propositional. (Private step: crossToSlot_round_trip_of_unit.)
• crossToSlotInv_crossToSlot, crossToSlot_crossToSlotInv — both directions, for a pair
  collapsing in both orders. The second gets its injectivity from the reversed collapse.
• crossToSlotEquiv — raising and lowering a named index against a mutually inverse pair, as a
  ≃ₗ between c and Function.update c i d.

Tensors/Dual.lean

• toDualMapAtIndex — dualise a named index, as crossToSlot against metricTensor (τ (c i)).
• crossToEnd_dual_metricTensor_metricTensor,
  crossToEnd_metricTensor_metricTensor_eq_dual_unit — the metric collapses against the metric at
  the dual colour, in both orders: the two hypotheses crossToSlotEquiv needs.
• toDualMapAtIndex_toDualMapAtIndex — the double-dual round trip, at every rank. Its output
  reindexing is IsReindexing.update_update_of_eq at τ (τ (c i)) = c i.
• fromDualMapAtIndex — the inverse, as crossToSlotInv against metricTensor (c i).
• fromDualMapAtIndex_toDualMapAtIndex, toDualMapAtIndex_fromDualMapAtIndex — both directions.
• toDualMapAtIndex_equivariant — G-equivariance.
• toDualAtIndex (+ _apply, _symm_apply) — the resulting ≃ₗ. Not a new name: this redefines
  the existing declaration, see the table above.

Tensors/Reindexing.lean — Fin index maps (new namespace Fin section)

• append_swap_val — the .val of the block-swap map, in closed form.
• append_castAdd_natAdd_eq_id, append_castAdd_cast, append_natAdd_cast — reassembling the two
  blocks of a Fin is the identity, or the length cast if one block was cast first.
• append_succAbove_const_eq_cycleIcc — moving slot i to the end is the cycle [i, last].
• cycleIcc_last_symm_apply_succAbove — the inverse cycle on a reinserted survivor.
• exists_succAbove_comm — an injection of Fin (n+1) restricts to the survivors of a slot.
• cast_castAdd_eq_mk, cast_natAdd_eq_mk — pin a Fin.cast/block composite to a literal
  ⟨v, _⟩.

Tensors/Reindexing.lean — IsReindexing

• succAbove_of_succAbove_eq — the caller-supplied survivor relabelling is itself a reindexing; the
  square (σ i).succAbove ∘ σ' = σ ∘ i.succAbove forces its injectivity, so no bijectivity
  hypothesis is needed. Unlike the existing IsReindexing.succAbove, which builds the relabelling
  from σ as a dite composite, the map here is the caller's, which is what lets it stand in the
  statement of a lemma the caller instantiates.
• moveLast — split a colour list at an arbitrary slot rather than at the last one.
• update_update_of_eq — updating slot i to d and back to c i returns c: the colour cast a
  round trip at slot i generates.

Other existing files

• Tensors/Contraction/SuccSuccAbove.lean: Fin.reinsert_castAdd, Fin.reinsert_natAdd — reinsert
  a survivor when the two removed slots straddle the two blocks of a product.
• Tensors/Contraction/Pure.lean: Pure.permP_dropPair_dropPair_congr,
  Pure.permP_dropPair_permP_congr — two permP/dropPair towers over a common pure tensor agree
  once their composite slot maps agree pointwise. Pure.contrPCoeff_congr — contrPCoeff is
  insensitive to its proof arguments (public, next to contrPCoeff).
• Tensors/Contraction/Products.lean: prodT_contrT_fst — the mirror of prodT_contrT_snd.
• Tensors/Basic.lean: permT_injective — from the existing permT_eq_zero_iff.
• Tensors/Elab.lean: jiggle emits toDualMapAtIndex; two #guard_msgs updated accordingly.
  Imports narrowed to Dual + Tensorial.

Reviewer map

1. Tensors/Dual.lean — the API change and the removals above. Everything else exists to make
   this file possible; if the deletions are unwelcome, say so here first.
2. Tensors/Reindexing.lean, Contraction/SuccSuccAbove.lean — the index-map lemmas. Pure
   Fin arithmetic, no tensor content.
3. Contraction/Pure.lean, Products.lean, Basic.lean — the pure-level congruences
   the long proofs key on.
4. Contraction/CrossToEnd.lean — the definition and its algebra. crossToEnd_assoc_rankTwo is
   the one long proof (66 lines); see the note below.
5. Contraction/CrossToSlot.lean — small, the convention bridge.
6. Contraction/UnitTensorContraction.lean — the round trips and the equivalence.
7. Tensors/Elab.lean — mechanical rename.

Known rough edges

• crossToEnd_assoc_rankTwo has a 66-line proof body, over the 50-LOC guideline. The index
  arithmetic is factored out into the Fin lemmas above and the closing case analysis is
  grind (splits := 20), the idiom SuccSuccAbove.lean already uses. What remains is
  proof-specific normalisation: the contrT_permT push sequence, the funPredPredAbove
  cancellation, and the nine Fin.cast→literal pins succSuccAbove_val needs to fire. I have not
  found a further split that leaves an independently meaningful lemma behind; suggestions welcome.
• Seven erw steps remain, six in UnitTensorContraction.lean and one in Dual.lean, each
  commented with the defeq the rw keying fails on.
• No set_option of any kind in the three files this PR adds. On the branch as a whole the net
  change is one backward.isDefEq.respectTransparency false removed (it sat on the deleted
  toDualMap_fromDualMap) and none added; no maxHeartbeats bump anywhere.

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

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

[jstoobysmith]

How is this different from contrT_congr?

[pariandrea]

contrT_cast` deleted; the file is back to its master content, untouched by this PR

[jstoobysmith]

What is the motivation for moving these results? I don't think ./Contraction/... is the best place for them

[pariandrea]

the results are back in Dual.lean

[jstoobysmith]

Should not do this, as one can just use Pure.congr_mid

[jstoobysmith]

Don't need lemmas like this

[pariandrea]

pure_cast_congr deleted; Pure.congr_mid used directly

[jstoobysmith]

My comment here still holds, that I don't see the difference between this and contrT_congr.

[jstoobysmith]

Should move to file where contrPCoeff and not made private

[pariandrea]

public, in Contraction/Pure.lean beside contrPCoeff

[jstoobysmith]

awaiting-author

[pariandrea]

Rebased onto current master and force-pushed, so the diff reads as new, sorry for that but the commits were becoming complicated. All threads from the last round are addressed and I've replied in each.
An important note:
toDualMapAtIndex_toDualMapAtIndex is now proved at every rank and
every slot, which makes the rank-one toDualMap / fromDualMap / toDual the n = 1, i = 0
case of it. I deleted those three and renamed the map toDualAtIndex to toDualMapAtIndex, so
that toDualAtIndex can be the ≃ₗ, the same naming relation toDualMap and toDual had on
master. Elab.lean follows the rename in jiggle and in two #guard_msgs. Nothing else in the
repo referenced the deleted names and the full build is green, but if you'd rather keep the rank-one API, or keep the old name on the map and give the equivalence a new one, say so and I'll change it.

Thank you both for the time you have put into this. The PR is much larger than the guidelines ask for, and I should have rescoped it before review rather than during. Future work will go up in smaller pieces. What it leaves behind is the raise/lower round trip proved once for any matched pair of rank two tensors that collapses to the unit tensor, at any rank, any slot, and any colours, so the species metric and the Kähler metric are both instances of it. The double dual round trip, which on master held only at rank one and slot zero, now holds at every rank and every slot.

[jstoobysmith]

Some minor comments

[pariandrea]

Addressed the latest round; replied in each thread.

• The Fin block in Reindexing.lean is down from nine lemmas to two. Seven had a single consumer and are now local hypotheses in the proof that used them. The two survivors have multiple consumers across three files.
• Fin.reinsert_castAdd / reinsert_natAdd →
  succSuccAbove_castAdd_natAdd_apply_castAdd / ..._apply_natAdd.
• IsReindexing.moveLast → move_last.
• Both CrossToEnd docstring points rewritten.

[jstoobysmith]

Ok, many thanks for iterating - approving this and will merge shortly!

[jstoobysmith]

I think @nateabr also needs to approve this PR for me to be able to merge it, given there are requested changes above.

Outdated Review

[nateabr]

Sorry about that :((

[jstoobysmith]

@nateabr Nothing to apologise about :) - tbh, I didn't even know this was a thing until now.