Tensor Buffer Traversal

Laws connecting native physical-buffer folds to finite row-major index folds. These results keep executable reductions on specialized storage while exposing the ordinary finite traversals needed by proofs.

theorem TorchLean.Tensor.Internal.fin_foldl_product {α : Type u} (outer inner : ℕ) (step : α → Fin outer → Fin inner → α) (initial : α) : Fin.foldl outer (fun (value : α) (outerIndex : Fin outer) => Fin.foldl inner (fun (value : α) (innerIndex : Fin inner) => step value outerIndex innerIndex) value) initial = Fin.foldl (outer * inner) (fun (value : α) (index : Fin (outer * inner)) => step value index.divNat index.modNat) initial

Nested finite folds are one row-major fold over the product index.

theorem TorchLean.Tensor.Internal.Rep.foldl_eq_fin_foldl {α β : Type} [Storage α] {s : Shape} (step : β → α → β) (initial : β) (x : Rep α s) : foldl step initial x = Fin.foldl s.size (fun (value : β) (index : Fin s.size) => step value (x.getFlat index)) initial

A packed fold is the finite fold over the tensor's flat row-major indices.

theorem TorchLean.Tensor.Internal.Rep.getFlat_stack_product {α : Type} [Storage α] {n : ℕ} {s : Shape} (components : Fin n → Rep α s) (outer : Fin n) (inner : Fin s.size) : (stack components).getFlat (Fin.cast ⋯ (finProdFinEquiv (outer, inner))) = (components outer).getFlat inner

Flat lookup into a stack selects the corresponding row and inner flat index.

theorem TorchLean.Tensor.Internal.Rep.foldl_stack {α β : Type} [Storage α] {n : ℕ} {s : Shape} (step : β → α → β) (initial : β) (components : Fin n → Rep α s) : foldl step initial (stack components) = Fin.foldl n (fun (value : β) (component : Fin n) => foldl step value (components component)) initial

Folding a stack is folding each row in leading-axis order.