Reusable neural-network blocks.

This module defines public block constructors such as residual, convolutional, and MLP-style compositions built from the public layer-building API.

inductive TorchLean.nn.Internal.blocks.Activation : Type

Small set of activation choices for block builders.

PyTorch analogues:

• relu <-> torch.nn.relu
• gelu <-> torch.nn.gelu
• silu <-> torch.nn.silu
• tanh <-> torch.nn.tanh
• sigmoid <-> torch.nn.sigmoid

• relu : Activation
• gelu : Activation
• silu : Activation
• tanh : Activation
• sigmoid : Activation

def TorchLean.nn.Internal.blocks.instReprActivation.repr : Activation → ℕ → Std.Format

@[implicit_reducible]

instance TorchLean.nn.Internal.blocks.instReprActivation : Repr Activation

@[implicit_reducible]

instance TorchLean.nn.Internal.blocks.instDecidableEqActivation : DecidableEq Activation

def TorchLean.nn.Internal.blocks.activation {s : Spec.Shape} : Activation → Sequential s s

Interpret an Activation as a TorchLean layer.

structure TorchLean.nn.Internal.blocks.MLP : Type

MLP (multi-layer perceptron) configuration.

This builder produces a sequential stack of linear layers with activations and optional dropout.

PyTorch analogue: a hand-written nn.Sequential(Linear(...), ReLU(), ..., Linear(...)).

• hidden : List ℕ

  Hidden layer widths (each entry creates a Linear -> Activation stage).

• activation : Activation

  Activation used after each hidden linear layer.

• dropout? : Option Float

  Optional dropout probability after each activation.

• seedBase : ℕ

  Base seed used to deterministically initialize all linear layers (and dropout if present).

def TorchLean.nn.Internal.blocks.mlpGo (act : Activation) (dropout? : Option Float) (inDim : ℕ) (hidden : List ℕ) (outDim seed : ℕ) : Sequential (Spec.Shape.dim inDim Spec.Shape.scalar) (Spec.Shape.dim outDim Spec.Shape.scalar)

Internal recursion for mlp.

This builds the sequential stack stage-by-stage, threading a seed so each linear (and optional dropout) layer gets a deterministic initialization key.

def TorchLean.nn.Internal.blocks.mlp (inDim outDim : ℕ) (cfg : MLP := { }) : Sequential (Spec.Shape.dim inDim Spec.Shape.scalar) (Spec.Shape.dim outDim Spec.Shape.scalar)

Build an MLP as a sequential stack of linear layers and activations.

This is a small PyTorch-shaped constructor: a typical call looks like: TorchLean.nn.blocks.mlp 784 10 { hidden := [128, 128], activation := .relu }.

structure TorchLean.nn.Internal.blocks.ConvAct (d : ℕ) : Type

Convolution followed by an activation and optional dropout.

• conv : Conv d
• activation : Activation
• dropout? : Option Float
• seedDropout : ℕ

def TorchLean.nn.Internal.blocks.convAct (leading : Spec.Shape := Spec.Shape.scalar) {d inChannels : ℕ} (spatial : Vector ℕ d) (cfg : ConvAct d) [NeZero inChannels] : Sequential (leading.concat (Spec.Shape.ofList (inChannels :: spatial.toList))) (leading.concat (Spec.Shape.ofList (cfg.conv.outChannels :: (Spec.convOutSpatial spatial cfg.conv.kernel cfg.conv.stride cfg.conv.padding).toList)))

Build a rank-polymorphic convolution/activation block.

structure TorchLean.nn.Internal.blocks.ConvActPool (d : ℕ) : Type

Convolution/activation followed by max pooling.

• block : ConvAct d
• pool : Pool d

def TorchLean.nn.Internal.blocks.convActPool (leading : Spec.Shape := Spec.Shape.scalar) {d inChannels : ℕ} (spatial : Vector ℕ d) (cfg : ConvActPool d) [NeZero inChannels] : Sequential (leading.concat (Spec.Shape.ofList (inChannels :: spatial.toList))) (leading.concat (Spec.Shape.ofList (cfg.block.conv.outChannels :: (Spec.poolOutSpatialPad (Spec.convOutSpatial spatial cfg.block.conv.kernel cfg.block.conv.stride cfg.block.conv.padding) cfg.pool.kernel cfg.pool.stride cfg.pool.padding).toList)))

Build a rank-polymorphic convolution/activation/max-pooling block.

def TorchLean.nn.Internal.blocks.residualLayer {s : Spec.Shape} (inner : Sequential s s) : LayerDef s s

Residual/skip-connection layer as a single LayerDef.

Given inner : Seq s s, this builds a layer that computes $x \mapsto \operatorname{inner}(x) + x$.

PyTorch analogue: $x + f(x)$ blocks used throughout ResNets and Transformers.

def TorchLean.nn.Internal.blocks.residual {s : Spec.Shape} (inner : Sequential s s) : Sequential s s

Lift residualLayer into a sequential model.

Branching (skip connections)

Seq is linear, but we sometimes want a PyTorch-like $x \mapsto f(x) + g(x)$ block.

We expose this as a single LayerDef whose parameter list is params(f) ++ params(g) and whose forward pass runs both programs and adds their outputs.

def TorchLean.nn.Internal.blocks.addBranchesLayer {σ τ : Spec.Shape} (f g : Sequential σ τ) : LayerDef σ τ

Combine two sequential branches into a single layer that adds their outputs.

The resulting layer runs both f and g on the same input $x$ and returns $f(x) + g(x)$. Parameters are concatenated as params(f) ++ params(g).

def TorchLean.nn.Internal.blocks.addBranches {σ τ : Spec.Shape} (f g : Sequential σ τ) : Sequential σ τ

Combine two models with the same input/output shapes by summing their outputs.

This is a typed residual-add block: addBranches f g represents the model $x \mapsto f(x) + g(x)$, and its parameter list is the concatenation of the two branches’ parameter lists.

def TorchLean.nn.Internal.blocks.residualBlock {input output : Spec.Shape} (main skip : Sequential input output) (act : Activation := Activation.relu) : Sequential input output

Apply an activation after adding two branches with the same output shape.