Coordinate semantics for pack and unpack

A checked packing pattern identifies one star region in every input shape. Its dimensions may differ between components, but all leading and trailing dimensions agree. The star region is flattened in row-major order and the flattened segments are placed consecutively on one packed axis.

The central object in this module is CheckedPack.packedCoordinateEquiv. It first reshapes each component's star region to its checked segment, then uses the general segment-concatenation equivalence. denotePack reads through the inverse equivalence, while denoteUnpack reads through the forward equivalence. Both round-trip laws therefore hold for every scalar type, including scalar components, zero-size shapes, and zero-length segments.

No tensor lowering is executed here. The later lowering theorem compares reshape and concatenation primitives with this coordinate denotation.

@[reducible, inline]

abbrev TorchLean.Tensor.Internal.Check.CheckedPack.InputTensors (checked : CheckedPack) (α : Type u) [Storage α] : Type u

The dependent family of input tensors accepted by a checked pack plan.

@[reducible, inline]

abbrev TorchLean.Tensor.Internal.Check.CheckedPack.OutputTensor (checked : CheckedPack) (α : Type u) [Storage α] : Type u

The packed tensor type determined by a checked pack plan.

def TorchLean.Tensor.Internal.Check.CheckedPack.componentCoordinateEquiv (checked : CheckedPack) : (component : Fin checked.inputShapes.length) × Coord (checked.inputShapes.get component) ≃ (segment : Fin checked.segmentLengths.length) × Coord (checked.leadingShape ++ checked.segmentLengths.get segment :: checked.trailingShape)

Reshape every component coordinate into the corresponding segment coordinate.

The equivalence is dependent because components may have different ranks and star shapes. Row-major reshape preserves all scalar positions, while componentSegmentEquiv keeps component and metadata order synchronized.

def TorchLean.Tensor.Internal.Check.CheckedPack.packedCoordinateEquiv (checked : CheckedPack) : (component : Fin checked.inputShapes.length) × Coord (checked.inputShapes.get component) ≃ Coord checked.output

The coordinate equivalence defining both pack and unpack.

On the input side, a coordinate records which component is selected and a coordinate inside that component. On the output side, the component's row-major star coordinate is placed in its consecutive segment of the packed axis; leading and trailing coordinates are unchanged.

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

Pack a checked family by reading the unique component coordinate represented by each packed output coordinate.

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

Unpack a tensor by embedding each requested component coordinate into its checked segment of the packed axis.

@[simp]

theorem TorchLean.Tensor.Internal.Semantics.denotePack_apply {α : Type u} [Storage α] (checked : Check.CheckedPack) (inputTensors : checked.InputTensors α) (outputCoordinate : Coord checked.output) : Rep.get (denotePack checked inputTensors) outputCoordinate = (inputTensors (checked.packedCoordinateEquiv.symm outputCoordinate).fst).get (checked.packedCoordinateEquiv.symm outputCoordinate).snd

Pack reads the component and coordinate selected by the packed coordinate.

@[simp]

theorem TorchLean.Tensor.Internal.Semantics.denoteUnpack_apply {α : Type u} [Storage α] (checked : Check.CheckedPack) (packedTensor : checked.OutputTensor α) (component : Fin checked.inputShapes.length) (inputCoordinate : Coord (checked.inputShapes.get component)) : (denoteUnpack checked packedTensor component).get inputCoordinate = Rep.get packedTensor (checked.packedCoordinateEquiv ⟨component, inputCoordinate⟩)

Unpack reads the packed coordinate assigned to the requested component entry.

@[simp]

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

Unpacking a packed component family recovers every component tensor.

@[simp]

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

Packing a complete checked unpack recovers the original packed tensor.

theorem TorchLean.Tensor.Internal.Semantics.dot_denotePack_denotePack {R : Type u} [Storage R] [Semiring R] (checked : Check.CheckedPack) (leftTensors rightTensors : checked.InputTensors R) : Rep.dot (denotePack checked leftTensors) (denotePack checked rightTensors) = ∑ component : Fin checked.inputShapes.length, (leftTensors component).dot (rightTensors component)

Packing both component families preserves their direct-sum finite pairing.

The coordinate equivalence partitions every packed coordinate into exactly one component coordinate. Multiplication order is unchanged, so the theorem holds over a potentially noncommutative semiring.