Certified native unpack

Concrete unpack plans compile each component to one native flat pullback from the packed buffer. The generated source index is specialized row-major arithmetic; the independent packed-coordinate equivalence remains the correctness reference.

Symbolic or nonportable shapes retain the general coordinate lowering.

def TorchLean.Tensor.Internal.Elab.Impl.compileNativeUnpack? (scalarType storage checked packedTensor : Lean.Expr) (checkedValue : Check.CheckedPack) : Lean.Elab.TermElabM (Option Lean.Expr)

Compile every component of one concrete unpack plan to native flat loops.

The result keeps the same dependent component family as ordinary unpack; only component storage construction changes.