Certified native pack dispatch

Concrete pack plans compile to one native output loop and a balanced segment dispatcher. Every leaf reads one component buffer through the verified inverse unpack index, so component count and tensor rank do not create semantic cases.

Symbolic or nonportable shapes retain the general coordinate lowering.

def TorchLean.Tensor.Internal.Elab.Impl.compileNativePack? (compilerChecked checked inputFamily : Lean.Expr) (checkedValue : Check.CheckedPack) : Lean.Elab.TermElabM (Option Lean.Expr)

Try to compile a concrete pack plan to a native output loop.

The generated dispatcher supports any number of components. Native pack is an optional proof-producing optimization: if its word-arithmetic certificates cannot be constructed, elaboration transactionally restores its state and retains the general verified coordinate lowering. Symbolic, zero-volume, and nonportable plans also return none.