Direct native lowering for pack and unpack

The checked component-to-packed coordinate equivalence drives both kernels. Packing fills one packed output buffer by reading the corresponding component entry. Unpacking fills each component buffer by reading its corresponding packed entry. Neither direction allocates slice, reshape, or concatenation intermediates.

The compiler-correctness theorems compare these direct row-major kernels with the independent coordinate semantics. The resulting inverse and adjoint laws apply to arbitrary scalar types or semirings as appropriate; they do not assume positive dimensions or a fixed tensor rank.

def TorchLean.Tensor.Internal.Lowering.packTensor {α : Type u} [Storage α] (checked : Check.CheckedPack) (inputTensors : checked.InputTensors α) : checked.OutputTensor α

Execute pack by filling the packed row-major buffer directly.

Each output flat index is converted once to its certified component coordinate, then read from that component's native tensor storage. No reshaped component tensors or concatenation buffers are allocated.

def TorchLean.Tensor.Internal.Lowering.unpackTensor {α : Type u} [Storage α] (checked : Check.CheckedPack) (packedTensor : checked.OutputTensor α) : checked.InputTensors α

Return a component-indexed function that fills the requested component buffer directly from the packed tensor.

The checked coordinate equivalence maps each component flat index to its unique packed location, so no slice or reshape buffer is constructed. The definition does not memoize component buffers or eagerly construct the whole family; callers control which components they evaluate and retain.

theorem TorchLean.Tensor.Internal.Lowering.packTensor_correct {α : Type u} [Storage α] (checked : Check.CheckedPack) (inputTensors : checked.InputTensors α) : packTensor checked inputTensors = Semantics.denotePack checked inputTensors

The direct row-major pack kernel equals the independent coordinate denotation.

theorem TorchLean.Tensor.Internal.Lowering.unpackTensor_correct {α : Type u} [Storage α] (checked : Check.CheckedPack) (packedTensor : checked.OutputTensor α) : unpackTensor checked packedTensor = Semantics.denoteUnpack checked packedTensor

The direct row-major unpack kernel equals the independent coordinate denotation.

@[simp]

theorem TorchLean.Tensor.Internal.Lowering.unpackTensor_packTensor {α : Type u} [Storage α] (checked : Check.CheckedPack) (inputTensors : checked.InputTensors α) : unpackTensor checked (packTensor checked inputTensors) = inputTensors

Unpacking a lowered pack recovers every input tensor.

@[simp]

theorem TorchLean.Tensor.Internal.Lowering.packTensor_unpackTensor {α : Type u} [Storage α] (checked : Check.CheckedPack) (packedTensor : checked.OutputTensor α) : packTensor checked (unpackTensor checked packedTensor) = packedTensor

Packing a complete lowered unpack recovers the packed tensor.

theorem TorchLean.Tensor.Internal.Lowering.dot_packTensor {R : Type u} [Storage R] [AddCommMonoid R] [Mul R] (checked : Check.CheckedPack) (inputTensors : checked.InputTensors R) (packedTensor : checked.OutputTensor R) : Rep.dot (packTensor checked inputTensors) packedTensor = ∑ component : Fin checked.inputShapes.length, (inputTensors component).dot (unpackTensor checked packedTensor component)

Pack is adjoint to unpack for the standard finite tensor pairing.

The sum ranges over the dependent component family. Multiplication order is preserved, so a commutative scalar multiplication is not required.

theorem TorchLean.Tensor.Internal.Lowering.dot_unpackTensor {R : Type u} [Storage R] [AddCommMonoid R] [Mul R] (checked : Check.CheckedPack) (packedTensor : checked.OutputTensor R) (componentTensors : checked.InputTensors R) : ∑ component : Fin checked.inputShapes.length, (unpackTensor checked packedTensor component).dot (componentTensors component) = Rep.dot packedTensor (packTensor checked componentTensors)

Unpack is adjoint to pack with the packed tensor in the left pairing slot.

This is stated separately from dot_packTensor because it preserves the opposite ordering of the two factors without imposing multiplication laws.