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

Merged

jstoobysmith merged 9 commits into

leanprover-community:masterfrom

pariandrea:tensors-bond-contraction

Jul 28, 2026

Commits on Jul 27, 2026

feat(Tensors/Reindexing): index-map and reindexing lemmas for slot-addressed contraction

pariandrea
and
Claude Opus 4.8
committed
feat(Tensors/Contraction): pure-tensor congruences and prodT_contrT_fst

pariandrea
and
Claude Opus 4.8
committed
feat(Tensors/Contraction): crossToEnd, the slot-addressed cross contraction

pariandrea
and
Claude Opus 4.8
committed
feat(Tensors/Contraction): crossToSlot, the result-to-slot convention

pariandrea
and
Claude Opus 4.8
committed
feat(Tensors/Contraction): unit-tensor collapse and the raise/lower round trip

pariandrea
and
Claude Opus 4.8
committed
refactor(Tensors/Dual): dualise a named index through crossToSlot, at every rank

pariandrea
and
Claude Opus 4.8
committed
feat(Tensors/Contraction): raising and lowering a named index as an equivalence

pariandrea
and
Claude Opus 4.8
committed
refactor(Tensors): drop the unused equivalence unfolding lemmas and update_dual_dual

pariandrea
and
Claude Opus 4.8
committed

Commits on Jul 28, 2026

refactor(Tensors): inline the single-consumer index-map lemmas and rename per review

pariandrea
and
Claude Opus 4.8
committed