ResNet BasicBlock training example (small CHW)

This next-step file demonstrates the public API.nn.blocks.resnetBasicBlock builder on a small 4×4 "band" dataset (vertical vs horizontal bars).

It is intentionally not part of the first quickstart path. It is here as a compact bridge from the basic MLP/CNN tutorials to the maintained model-zoo ResNet example under NN/Examples/Models.

Note: this particular example uses BatchNorm blocks, so the model is built for a fixed batch size. Most other tutorials in this folder use batch-free models and let API.train.runLoader* lift them.

Check this tutorial module directly:

• lake build NN.Examples.Quickstart.ResnetBasicblockTrain

For the maintained command-line ResNet trainer, use NN/Examples/Models/Vision/Resnet.lean:

• python3 scripts/datasets/download_example_data.py --cifar10
• lake exe torchlean resnet --cpu --n-total 20 --steps 1

Optional flags:

• --epochs E
• --quick (skip expensive before/after evaluation reports; intended for CI/smoke runs)

Public API used here:

• nn.conv, nn.batchNorm, nn.resnetBasicBlock
• nn.flattenBatch, nn.linear
• Data.batchLoader
• train.fitLoaderWith + train.Callbacks

Reader note:

• this is the one tutorial here whose model is already batched in its type because BatchNorm uses cross-batch statistics;
• so the task shape is fixed to the chosen --batch size and the loader uses drop_last=true;
• Semantics.Scalar α / Runtime.Scalar α still mean "the chosen scalar backend supports the math" and "the backend is executable".

See NN/Examples/Quickstart/README.md for the shared conventions in this folder.

Why this tutorial exists:

• it shows how TorchLean exposes residual CNN blocks, not just plain sequential stacks;
• it gives users one clean example of fixed-batch training, which matters once BatchNorm enters the model;
• it stays small enough to read in one sitting while still looking recognizably "ResNet-like".

def NN.Examples.Quickstart.ResNetBasicBlockTrain.mkModel (n : ℕ) [NeZero n] : API.nn.M (API.nn.Sequential (Shape.Images n 1 4 4) (Tensor.shapeOfDims [n, 2]))

def NN.Examples.Quickstart.ResNetBasicBlockTrain.runOnce {batch : ℕ} (task : API.train.Task (Shape.Images batch 1 4 4) (Tensor.shapeOfDims [batch, 2])) {α : Type} [API.Semantics.Scalar α] [DecidableEq Spec.Shape] [ToString α] [API.Runtime.Scalar α] (runner : API.train.Runner α task) (epochs : ℕ := 20) (seed : ℕ := 0) (quick : Bool := false) : IO Unit

Run one training session on the small band-image dataset.

This is intentionally separated from main so the tutorial keeps a clean “build task, choose backend, then train” structure.

def NN.Examples.Quickstart.ResNetBasicBlockTrain.main (args : List String) : IO Unit