Certified affine-index normalization

This module removes mixed-radix decode/encode pairs from generated source indices. It recognizes the canonical row-major form remainder + radix * digit, obtains the range proof from the Fin value used as the remainder, and emits an equality certificate for every replacement.

The pass is independent of tensor rank and concrete axis names. Symbolic radices are simplified whenever the remainder carries the matching Fin bound; unsupported arithmetic remains unchanged.

def TorchLean.Tensor.Internal.Elab.Impl.simplifyAffineIndex (value : Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.Expr)

Normalize mixed-radix arithmetic in one generated flat index.

The returned equality is oriented from the original expression to the optimized expression, ready to compose with the operand-view certificate.