Generated kernel utilities

This module closes independently generated results over only the lets they use and constructs direct correctness certificates for compile-time-expanded finite folds.

def TorchLean.Tensor.Internal.Elab.Impl.withGeneratedLetResults (bindings : List (Lean.Name × Lean.Expr)) (body : List Lean.Expr → Lean.Elab.TermElabM (Array Lean.Expr)) : Lean.Elab.TermElabM (Array Lean.Expr)

Introduce generated lets around several results independently.

mkLetFVars drops unused let declarations from each result. A contraction-invariant operand can therefore remain in a scalar factor while coordinate-dependent reads stay only in the middle product.

def TorchLean.Tensor.Internal.Elab.Impl.unrollFiniteFold (length : ℕ) (step initial : Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.Expr)

Unroll a finite fold of known length and construct its equality certificate from the standard successor and zero laws.

Building this proof directly avoids asking the simplifier to normalize the dependent operand family generated for every einsum input.