nn.functional mirrors torch.nn.functional: pure, stateless building blocks.

In TorchLean these are derived ops over the small primitive Ops API, so the same code works on both the eager backend and the compiled backend.

PyTorch references:

• torch.nn.functional: https://pytorch.org/docs/stable/nn.functional.html

Leading-Dimension Mapping

mapLeading leading model applies a model independently across every index in an arbitrary leading shape. A conventional batch is the special case leading = .dim batch .scalar; multiple leading axes work without introducing another tensor or model type.

Correctness-first batch lift for exposing PyTorch-like N×... APIs even when a primitive only exists for the unbatched shape.

def TorchLean.nn.Internal.Implementation.adaptFlatBatch (leading : Spec.Shape) {σ τ : Spec.Shape} (l : LayerDef (Spec.Shape.dim leading.size σ) (Spec.Shape.dim leading.size τ)) : LayerDef (leading.concat σ) (leading.concat τ)

Expose a runtime layer whose outer axis is a flat batch as a layer over an arbitrary leading shape. The adapter changes only the view of the input and output; parameters, buffer updates, and the underlying forward program are preserved.

def TorchLean.nn.Internal.Implementation.mapLayerOverAxis (n : ℕ) {σ τ : Spec.Shape} (l : LayerDef σ τ) : LayerDef (Spec.Shape.dim n σ) (Spec.Shape.dim n τ)

Lift a single-example LayerDef σ τ to operate on a leading batch axis.

This is a correctness-first batch lift: it runs the underlying layer independently on each batch element. Prefer a primitive batched layer when one exists.

def TorchLean.nn.Internal.Implementation.mapModelOverAxis (n : ℕ) {σ τ : Spec.Shape} : Sequential σ τ → Sequential (Spec.Shape.dim n σ) (Spec.Shape.dim n τ)

Lift a sequential model to act pointwise on a leading batch axis.

def TorchLean.nn.Internal.mapLeading (leading : Spec.Shape) {σ τ : Spec.Shape} : Sequential σ τ → Sequential (leading.concat σ) (leading.concat τ)

Apply a model pointwise over an arbitrary collection of leading dimensions.

Note: some low-level TorchLean layers (notably conv/pool/norm) have Nat-side well-formedness proof arguments (e.g. kH ≠ 0).

The public path is record-based specs that hide those proofs via typeclasses like NeZero, so examples can stay PyTorch-like without relying on positional macros.