Flat contraction lowering

This module decodes a native row-major counter into certified tensor coordinates and lowers sufficiently large multi-axis tiled contractions to one flat native loop.

def TorchLean.Tensor.Internal.Elab.Impl.nativeCoordinateComponents (lengths : List Lean.Expr) (flatIndex hFlatIndex : Lean.Expr) : Lean.Elab.TermElabM (List Lean.Expr × List Lean.Expr × List Lean.Expr)

Decode a concrete native flat counter into row-major coordinate components.

Each component uses native quotient or remainder arithmetic. The accompanying equalities identify those executable components with the nested Fin.divNat and Fin.modNat coordinates used by Coord.unlinearize.

def TorchLean.Tensor.Internal.Elab.Impl.compileFlatCoordinateFold? (lengths : List Lean.Expr) (step initial reference : Lean.Expr) : Lean.Elab.TermElabM (Option (Lean.Expr × Lean.Expr))

Compile a large concrete multi-axis contraction as one native flat loop.

The executable callback decodes its row-major counter with native quotient and remainder operations. Its certificate identifies those coordinates with Coord.unlinearize, then transports the native fold to coordinateFoldl. The optimization is retained only when the callback is a generated four- or eight-lane update, so every scalar accumulator remains live across the complete contraction.