Native TorchLean FNO1D Burgers

Read this after the basic CNN/MLP examples if you want the operator-learning path. The Python scripts do the two jobs Lean should not own here: download and reshape the public burgers_data_R10.mat file, then plot the prediction CSV. The model, loss, optimizer, and training loop stay in TorchLean.

This executable uses real-split Fourier arithmetic because the Burgers data are real-valued. CPU and GPU execution use the same full-spectrum model and spectral parameter layout, with separate real and imaginary tensors. The runtime selects how the operations are executed.

The training task follows the standard FNO Burgers setup: learn the operator $u_0(x)\mapsto u(x,T)$ on a fixed periodic grid. The default grid and row counts are modest enough for a local run while still exercising the real operator-learning path. Larger runs can raise --steps, export more rows, and bump the constants below.

References for the dataset/training convention:

• Li et al., “Fourier Neural Operator for Parametric Partial Differential Equations”, 2020/2021.
• MathWorks’ Burgers FNO example and the burgers_data_R10.mat public dataset.
• SciML FNO tutorials using fields a for initial conditions and u for final solutions.

def NN.Examples.Models.Operators.Fno1dBurgers.exeName : String

CLI subcommand name used in terminal banners and errors.

def NN.Examples.Models.Operators.Fno1dBurgers.gridSize : ℕ

Spatial grid resolution used by the prepared Burgers .npy slices.

def NN.Examples.Models.Operators.Fno1dBurgers.width : ℕ

Channel width inside the compact FNO block.

def NN.Examples.Models.Operators.Fno1dBurgers.modes : ℕ

Spectral mode budget.

The full-spectrum model uses this as the width of each end band on both CPU and GPU.

def NN.Examples.Models.Operators.Fno1dBurgers.blocks : ℕ

Number of spectral blocks used by the compact training run.

def NN.Examples.Models.Operators.Fno1dBurgers.defaultTrainRows : ℕ

Default number of training rows expected from the preparation script.

def NN.Examples.Models.Operators.Fno1dBurgers.defaultTestRows : ℕ

Default number of held-out rows expected from the preparation script.

@[reducible, inline]

abbrev NN.Examples.Models.Operators.Fno1dBurgers.modelConfig : TorchLean.nn.models.FNO.Config 1

FNO configuration shared by the constructor and sample loaders.

@[reducible, inline]

abbrev NN.Examples.Models.Operators.Fno1dBurgers.input : Spec.Shape

Model input shape: one sampled initial condition on the fixed grid.

@[reducible, inline]

abbrev NN.Examples.Models.Operators.Fno1dBurgers.output : Spec.Shape

Model output shape: one predicted terminal solution on the same grid.

def NN.Examples.Models.Operators.Fno1dBurgers.defaultDir : System.FilePath

Directory where the preparation script writes Burgers tensors by default.

def NN.Examples.Models.Operators.Fno1dBurgers.trainXPath : System.FilePath

Default training input tensor path.

def NN.Examples.Models.Operators.Fno1dBurgers.trainYPath : System.FilePath

Default training target tensor path.

def NN.Examples.Models.Operators.Fno1dBurgers.testXPath : System.FilePath

Default held-out input tensor path.

def NN.Examples.Models.Operators.Fno1dBurgers.testYPath : System.FilePath

Default held-out target tensor path.

def NN.Examples.Models.Operators.Fno1dBurgers.defaultPlotCsv : System.FilePath

Default CSV path for the prediction-vs-target plot script.

def NN.Examples.Models.Operators.Fno1dBurgers.defaultLogPath : System.FilePath

Default JSON training-log path.

def NN.Examples.Models.Operators.Fno1dBurgers.missingDataHint : String

User-facing hint printed when the prepared Burgers tensors are missing.

structure NN.Examples.Models.Operators.Fno1dBurgers.Options : Type

FNO Burgers command-line options: training flags, data paths, and artifact paths.

The record keeps optimizer/log settings, tensor paths, and output artifacts as separate named concerns.

• training : TorchLean.CLI.Training.OptimizerOptions

  Optimizer, step, batching, and logging controls.

• data : Support.Npy.SplitOptions

  Prepared train/test tensors and evaluation row counts.

• plotCsv : System.FilePath

  Output path for the prediction diagnostic.

def NN.Examples.Models.Operators.Fno1dBurgers.instReprOptions.repr : Options → ℕ → Std.Format

@[instance_reducible]

instance NN.Examples.Models.Operators.Fno1dBurgers.instReprOptions : Repr Options

def NN.Examples.Models.Operators.Fno1dBurgers.dataPaths (config : Options) : Array System.FilePath

All required dataset files for this run.

def NN.Examples.Models.Operators.Fno1dBurgers.Options.parse (args : List String) : Except String (Options × List String)

Parse the FNO Burgers command-line options.

def NN.Examples.Models.Operators.Fno1dBurgers.Options.memoryCadence (config : Options) (runtime : TorchLean.Runtime.Config) : ℕ

Effective CUDA-memory-watch cadence for this run.

def NN.Examples.Models.Operators.Fno1dBurgers.Options.experiment (config : Options) (spectralPath device : String) (history : Runtime.Training.MetricHistory) : Runtime.Training.ExperimentLog

The experiment record of one run: the model and run settings as config entries, the train and test curves, and the dataset files as notes.

def NN.Examples.Models.Operators.Fno1dBurgers.model : TorchLean.nn.Builder (TorchLean.nn.Sequential input output)

The Fourier neural operator this example trains, at the width, mode count and depth fixed by modelConfig.

def NN.Examples.Models.Operators.Fno1dBurgers.loadSplit (xPath yPath : System.FilePath) (n : ℕ) : IO (TorchLean.Data.SampleStream (TorchLean.Sample.Supervised Float input output))

Load one fixed-grid Burgers split as supervised TorchLean samples.

def NN.Examples.Models.Operators.Fno1dBurgers.writePrediction (plotCsv : System.FilePath) (x target prediction : TorchLean.Tensor Float input) : IO Unit

Write one FNO prediction row to CSV for the companion plotting script.

def NN.Examples.Models.Operators.Fno1dBurgers.metrics : Runtime.Training.MetricHistory

Two tracked curves, train and test MSE, with the colours the log viewer will use.

def NN.Examples.Models.Operators.Fno1dBurgers.writeLog (destination : Runtime.Training.LogDestination) (history : Runtime.Training.MetricHistory) (config : Options) (spectralPath device : String) : IO Unit

Persist the train/test MSE history as an experiment record.

structure NN.Examples.Models.Operators.Fno1dBurgers.Splits : Type

Loaded train/test splits before evaluation prefixes and cycling streams are derived.

• train : TorchLean.Data.SampleStream (TorchLean.Sample.Supervised Float input output)

  Training split as supervised samples.

• test : TorchLean.Data.SampleStream (TorchLean.Sample.Supervised Float input output)

  Held-out split as supervised samples.

def NN.Examples.Models.Operators.Fno1dBurgers.load (config : Options) : IO Splits

Validate paths and load both Burgers splits.

structure NN.Examples.Models.Operators.Fno1dBurgers.Evaluation : Type

Deterministic evaluation prefixes and cycling stream derived from the loaded train/test sets.

• train : TorchLean.Data.SampleStream (TorchLean.Tensor Float input × TorchLean.Tensor Float output)
• test : TorchLean.Data.SampleStream (TorchLean.Tensor Float input × TorchLean.Tensor Float output)
• sample : TorchLean.Sample.Supervised Float input output

  Training sample used to initialize the runtime's compiled evaluation path.

• probe : TorchLean.Tensor Float input × TorchLean.Tensor Float output

  Held-out sample used for the prediction CSV.

• next : ℕ → TorchLean.Sample.Supervised Float input output

def NN.Examples.Models.Operators.Fno1dBurgers.prepare (config : Options) (data : Splits) : IO Evaluation

Prepare deterministic evaluation prefixes and a cycling stream of training samples.

def NN.Examples.Models.Operators.Fno1dBurgers.record (history : Runtime.Training.MetricHistory) (step : ℕ) (tag : String) (trainLoss testLoss : Float) : IO Runtime.Training.MetricHistory

Push one train/test MSE point into the metric history and print the tagged report line.

def NN.Examples.Models.Operators.Fno1dBurgers.run (runtime : TorchLean.Runtime.Config) (config : Options) : IO Unit

Train the same full-spectrum model through the shared trainer on CPU or GPU.

def NN.Examples.Models.Operators.Fno1dBurgers.printHeader (runtime : TorchLean.Runtime.Config) (config : Options) : IO Unit

Print the run's configuration: device, model geometry, row counts and file paths.

An FNO run that silently loaded the wrong split can look like a training problem. Printing the paths and row counts helps identify the data error.

def NN.Examples.Models.Operators.Fno1dBurgers.main (args : List String) : IO UInt32

Train and evaluate with the selected runtime and the shared FNO parameterization.