Certified native reduction indices

Concrete reductions decode their output and fiber counters separately. This module compiles those counters directly into the source tensor's row-major index, avoiding the extra combined-coordinate decode used by the compact semantic law.

def TorchLean.Tensor.Internal.Elab.Impl.compileReductionLogicalIndex (checked : Lean.Expr) (_checkedValue : Check.CheckedTransform) (outputFin fiberFin outputValue fiberValue : Lean.Expr) : Lean.Elab.TermElabM (Lean.Expr × Lean.Expr × Lean.Expr)

Compile the logical input index of a concrete reduction.

The executable expression is the partial evaluation of the general separated row-major index. Its theorem composes with the checked reduction law, so no generated arithmetic proof depends on a tensor's rank or concrete dimensions.