Minibatch MLP training (batching is implicit)

This next-step file shows the intended minibatch path in TorchLean:

1. load a CSV dataset through Data,
2. choose persistent runtime settings with Trainer.RunConfig,
3. write the model over the minibatch shape (batch × Vec inDim),
4. call trainer.train data trainOptions,
5. reuse the trained handle for one follow-up prediction batch.

Run the loader tutorial instead when possible:

• lake exe torchlean data_csv --steps 1 --batch 5 --dtype float --backend eager

Build this comparison module directly with:

• lake build NN.Examples.Quickstart.MinibatchMlpTrain

Optional flags (tutorial-specific):

• --data-dir PATH (default: NN/Examples/Data)
• --csv PATH (override the CSV file)
• --seed S
• --steps N
• --batch N

def NN.Examples.Quickstart.MinibatchMLPTrain.defaultLogJson : System.FilePath

Default JSON log path used only when the user explicitly passes --log.

def NN.Examples.Quickstart.MinibatchMLPTrain.missingCsvHint : String

def NN.Examples.Quickstart.MinibatchMLPTrain.inDim : ℕ

def NN.Examples.Quickstart.MinibatchMLPTrain.hidDim : ℕ

def NN.Examples.Quickstart.MinibatchMLPTrain.outDim : ℕ

def NN.Examples.Quickstart.MinibatchMLPTrain.mkModel {batch : ℕ} : TorchLean.nn.M (TorchLean.nn.Sequential (TorchLean.Shape.mat batch inDim) (TorchLean.Shape.mat batch outDim))

Batched MLP 2 -> 8 -> 1 built from the public model constructor.

def NN.Examples.Quickstart.MinibatchMLPTrain.usage : String

Command-line help for the minibatch MLP quickstart.

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