Scalar-register contraction lowering

This module recognizes a generic tiled vector fold and certifies its lowering to concrete scalar-register loops. Lane count affects machine representation, not the contraction semantics.

def TorchLean.Tensor.Internal.Elab.Impl.scalarizeTileNativeFold? (length nativeBound hBound nativeState nativeCoordinate hCoordinate body initial ordinaryLoop hOrdinaryReference : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr))

Replace an exact generated tiled vector update with the corresponding native loop whose lane totals remain separate scalar arguments.

The replacement is valid only when no lane value depends on the incoming vector state. The returned theorem composes the scalar-loop equivalence with the caller's certificate for the ordinary native fold.