Rearrange and repeat semantics

Independent coordinate denotations and algebraic laws for checked rearrangements and repetitions.

def TorchLean.Tensor.Internal.Semantics.denoteRearrange {α : Type u} [Storage α] (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.rearrange) (inputTensor : checked.InputTensor α) : checked.OutputTensor α

Independent rearrange denotation: pull the input tensor along the certified elementary-axis permutation.

@[simp]

theorem TorchLean.Tensor.Internal.Semantics.denoteRearrange_apply {α : Type u} [Storage α] (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.rearrange) (inputTensor : checked.InputTensor α) (outputCoordinate : Coord checked.value.output) : Rep.get (denoteRearrange checked hKind inputTensor) outputCoordinate = Rep.get inputTensor (checked.inputCoordinateOfOutput ⋯ outputCoordinate)

Rearrange reads the input entry selected by its output coordinate.

@[simp]

theorem TorchLean.Tensor.Internal.Semantics.inverse_denoteRearrange {α : Type u} [Storage α] (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.rearrange) (inputTensor : checked.InputTensor α) : Rep.reindex (checked.rearrangeCoordinateEquiv hKind).symm (denoteRearrange checked hKind inputTensor) = inputTensor

Reindexing a rearranged tensor by the inverse coordinate equivalence recovers the original tensor.

theorem TorchLean.Tensor.Internal.Semantics.map_denoteRearrange {α : Type u} {β : Type v} [Storage α] [Storage β] (f : α → β) (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.rearrange) (inputTensor : checked.InputTensor α) : Rep.map f (denoteRearrange checked hKind inputTensor) = denoteRearrange checked hKind (Rep.map f inputTensor)

Rearrange commutes with every pointwise scalar map.

theorem TorchLean.Tensor.Internal.Semantics.zipWith_denoteRearrange {α : Type u} {β : Type v} {γ : Type w} [Storage α] [Storage β] [Storage γ] (f : α → β → γ) (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.rearrange) (leftTensor : checked.InputTensor α) (rightTensor : checked.InputTensor β) : Rep.zipWith f (denoteRearrange checked hKind leftTensor) (denoteRearrange checked hKind rightTensor) = denoteRearrange checked hKind (Rep.zipWith f leftTensor rightTensor)

Rearrange commutes with every pointwise binary operator when both operands have the same input shape.

theorem TorchLean.Tensor.Internal.Semantics.sum_denoteRearrange {α : Type u} [Storage α] [AddCommMonoid α] (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.rearrange) (inputTensor : checked.InputTensor α) : ∑ outputCoordinate : Coord checked.value.output, Rep.get (denoteRearrange checked hKind inputTensor) outputCoordinate = ∑ inputCoordinate : Coord checked.value.normalized.input, Rep.get inputTensor inputCoordinate

Rearrange preserves the total sum over any additive commutative monoid.

theorem TorchLean.Tensor.Internal.Semantics.dot_denoteRearrange {R : Type u} [Storage R] [Semiring R] (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.rearrange) (inputTensor : checked.InputTensor R) (outputTensor : checked.OutputTensor R) : Rep.dot (denoteRearrange checked hKind inputTensor) outputTensor = Rep.dot inputTensor (Rep.reindex (checked.rearrangeCoordinateEquiv hKind).symm outputTensor)

The adjoint of a checked rearrangement under the finite tensor pairing is reindexing by its inverse coordinate equivalence.

This algebraic identity is the pattern-level core of the inverse-rearrange VJP; connecting it to a differentiability framework is a separate theorem.

theorem TorchLean.Tensor.Internal.Semantics.dot_denoteRearrange_denoteRearrange {R : Type u} [Storage R] [Semiring R] (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.rearrange) (leftTensor rightTensor : checked.InputTensor R) : Rep.dot (denoteRearrange checked hKind leftTensor) (denoteRearrange checked hKind rightTensor) = Rep.dot leftTensor rightTensor

Rearranging both operands preserves their finite tensor pairing.

def TorchLean.Tensor.Internal.Semantics.denoteRepeat {α : Type u} [Storage α] (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.repeat) (inputTensor : checked.InputTensor α) : checked.OutputTensor α

Independent repeat denotation: pull the input tensor along the projection that forgets axes introduced on the output side.

@[simp]

theorem TorchLean.Tensor.Internal.Semantics.denoteRepeat_apply {α : Type u} [Storage α] (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.repeat) (inputTensor : checked.InputTensor α) (outputCoordinate : Coord checked.value.output) : Rep.get (denoteRepeat checked hKind inputTensor) outputCoordinate = Rep.get inputTensor (checked.inputCoordinateOfOutput ⋯ outputCoordinate)

Repeat copies the input entry selected after new output axes are forgotten.

theorem TorchLean.Tensor.Internal.Semantics.push_denoteRepeat {α : Type u} [Storage α] [AddCommMonoid α] (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.repeat) (inputTensor : checked.InputTensor α) : Rep.push (checked.inputCoordinateOfOutput ⋯) (denoteRepeat checked hKind inputTensor) = Rep.map (fun (value : α) => (List.map checked.value.axisLength (List.filter (fun (axis : Check.AxisId) => !checked.value.normalized.inputAxes.contains axis) checked.value.normalized.outputAxes)).prod • value) inputTensor

Aggregating a repeated tensor back to its input coordinates multiplies every entry by the number of settings of the introduced axes.

Natural-number scalar multiplication states the result over any additive commutative monoid, including the zero-multiplicity case.

theorem TorchLean.Tensor.Internal.Semantics.sum_denoteRepeat {α : Type u} [Storage α] [AddCommMonoid α] (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.repeat) (inputTensor : checked.InputTensor α) : ∑ outputCoordinate : Coord checked.value.output, Rep.get (denoteRepeat checked hKind inputTensor) outputCoordinate = (List.map checked.value.axisLength (List.filter (fun (axis : Check.AxisId) => !checked.value.normalized.inputAxes.contains axis) checked.value.normalized.outputAxes)).prod • ∑ inputCoordinate : Coord checked.value.normalized.input, Rep.get inputTensor inputCoordinate

Repeat scales the total additive sum by the product of the introduced axis lengths.

theorem TorchLean.Tensor.Internal.Semantics.dot_denoteRepeat {R : Type u} [Storage R] [CommSemiring R] (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.repeat) (inputTensor : checked.InputTensor R) (outputTensor : checked.OutputTensor R) : Rep.dot (denoteRepeat checked hKind inputTensor) outputTensor = Rep.dot inputTensor (Rep.push (checked.inputCoordinateOfOutput ⋯) outputTensor)

Fiber aggregation is the adjoint of repeat under the finite tensor pairing.

Commutativity of scalar multiplication is needed because Rep.dot records the left operand first, whereas the general push/pull adjunction is stated with the pushed tensor on the left.