Tensor concatenation by families and binary folds

The family coordinate map places each parent occurrence in its consecutive axis segment. These identities connect that map to the binary tensor primitive used by the IR evaluator.

theorem TorchLean.Tensor.Internal.Rep.concatenateAxes_cons {α : Type} [Storage α] (leading trailing : Shape) (length : ℕ) (lengths : List ℕ) (values : (parent : Fin (length :: lengths).length) → Rep α (leading ++ (length :: lengths).get parent :: trailing)) : concatenateAxes leading trailing (length :: lengths) values = concatenateAxis leading trailing (values 0) (concatenateAxes leading trailing lengths fun (parent : Fin lengths.length) => values parent.succ)

A family concatenation separates into its first occurrence and the remaining family.

theorem TorchLean.Tensor.Internal.Rep.concatenateAxis_zero_right {α : Type} [Storage α] (leading trailing : Shape) {length : ℕ} (left : Rep α (leading ++ length :: trailing)) (right : Rep α (leading ++ 0 :: trailing)) : concatenateAxis leading trailing left right = left

Appending an empty axis segment preserves every coordinate of the left tensor.

theorem TorchLean.Tensor.Internal.Rep.concatenateAxes_singleton {α : Type} [Storage α] (leading trailing : Shape) (length : ℕ) (values : (parent : Fin [length].length) → Rep α (leading ++ [length].get parent :: trailing)) : concatenateAxes leading trailing [length] values = values 0

Concatenation of one occurrence preserves its tensor.

theorem TorchLean.Tensor.Internal.Rep.concatenateAxis_assoc {α : Type} [Storage α] (leading trailing : Shape) {first second third : ℕ} (a : Rep α (leading ++ first :: trailing)) (b : Rep α (leading ++ second :: trailing)) (c : Rep α (leading ++ third :: trailing)) : castShape ⋯ (concatenateAxis leading trailing (concatenateAxis leading trailing a b) c) = concatenateAxis leading trailing a (concatenateAxis leading trailing b c)

Binary concatenation is associative, including zero-length segments.