Generated kernel utilities

This module constructs direct correctness certificates for compile-time-expanded finite folds. Shared generated-let construction lives in Einsum.Index.

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.