Certified native-index normalization

This module recognizes native coordinate arithmetic emitted by the einsum compiler and replaces conversion and quotient-remainder round trips with proved equal expressions.

def TorchLean.Tensor.Internal.Elab.Impl.hasNativeIndexRedex (value : Lean.Expr) : Bool

Report whether a generated kernel contains a conversion or quotient-remainder expression handled by the focused native-index simplifier.

The scan keeps the simplifier away from unrelated symbolic and scalar terms.

def TorchLean.Tensor.Internal.Elab.Impl.simplifyNativeIndexExpressions (expression : Lean.Expr) (context : Lean.Meta.Simp.Context) (pre : Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Step := fun (x : Lean.Expr) => pure Lean.Meta.Simp.Step.continue) : Lean.MetaM (Lean.Expr × Lean.Expr)

Normalize generated native-index expressions in two certified phases.

The first pass removes native-to-natural-to-native conversions. The second then sees complete quotient-remainder reconstructions and replaces them with direct native indexing. The returned equality composes both simplifier certificates.