Contraction-loop invariant motion

This module floats compiler-generated index bases to the earliest contraction loop where all referenced coordinates are available, preserving a certificate for the optimized expression.

partial def TorchLean.Tensor.Internal.Elab.Impl.hoistCoordinateLoopLets (value : Lean.Expr) : Lean.MetaM Lean.Expr

Float generated index-base lets to the earliest contraction loop where all of their coordinates are available.

The pass is deliberately limited to the standard, native, and tiled fold expressions emitted by the einsum compiler. It does not rewrite user terms.

def TorchLean.Tensor.Internal.Elab.Impl.optimizeCoordinateFoldExpression (generated hReferenceGenerated : Lean.Expr) : Lean.Elab.TermElabM (Lean.Expr × Lean.Expr)

Normalize native index conversions and float generated index bases out of contraction loops.

The input certificate must identify the semantic reference with the generated expression. The returned certificate has the same orientation after both normalization passes and loop-invariant let motion.