Synthetic Band Dataset

Several TorchLean examples use a compact 4×4 image classification task:

• class 0: a vertical band
• class 1: a horizontal band

This domain module owns both the renderer and the canonical 4×4 dataset. Keeping these definitions out of TorchLean.Data.Synthetic prevents a particular image layout from becoming part of TorchLean's general tensor and sample abstractions.

Renderer

inductive TorchLean.Data.Bands.Axis : Type

Spatial axis along which a synthetic band varies.

• row : Axis
• column : Axis

def TorchLean.Data.Bands.instReprAxis.repr : Axis → ℕ → Std.Format

@[implicit_reducible]

instance TorchLean.Data.Bands.instReprAxis : Repr Axis

@[implicit_reducible]

instance TorchLean.Data.Bands.instDecidableEqAxis : DecidableEq Axis

def TorchLean.Data.Bands.Axis.name : Axis → String

Human-readable class name associated with an axis.

def TorchLean.Data.Bands.render (channels height width : ℕ) (value : Fin channels → Fin height → Fin width → Float) : Spec.Tensor Float (Spec.Shape.dim channels (Spec.Shape.dim height (Spec.Shape.dim width Shape.scalar)))

Render a channel-first rank-three tensor from an in-bounds scalar function.

This shape is part of this particular dataset, not a restriction on TorchLean tensors or models.

def TorchLean.Data.Bands.renderBinary (channels height width : ℕ) (selected : Fin channels → Fin height → Fin width → Bool) (onValue : Float := 1.0) (offValue : Float := 0.0) : Spec.Tensor Float (Spec.Shape.dim channels (Spec.Shape.dim height (Spec.Shape.dim width Shape.scalar)))

Render a binary-valued channel-first tensor from a finite predicate.

def TorchLean.Data.Bands.renderBand (height width : ℕ) (axis : Axis) (offset : ℕ) (thickness : ℕ := 2) (onValue : Float := 1.0) (offValue : Float := 0.0) : Spec.Tensor Float (Spec.Shape.dim 1 (Spec.Shape.dim height (Spec.Shape.dim width Shape.scalar)))

Render a single-channel horizontal or vertical band.

Classes and datasets

structure TorchLean.Data.Bands.Class : Type

Label metadata for one family of synthetic bands.

• axis : Axis

  Axis occupied by the band.

• label : ℕ

  Numeric class label.

• name : String

  Display name used by reports.

def TorchLean.Data.Bands.vertical (label : ℕ := 0) (name : String := "vertical") : Class

Construct a vertical-band class.

def TorchLean.Data.Bands.horizontal (label : ℕ := 1) (name : String := "horizontal") : Class

Construct a horizontal-band class.

def TorchLean.Data.Bands.samples (height width : ℕ) (classes : List Class) (offsets : List ℕ) (thickness : ℕ := 2) : List (Spec.Tensor Float (Spec.Shape.dim 1 (Spec.Shape.dim height (Spec.Shape.dim width Shape.scalar))) × ℕ)

Generate (tensor, label) samples for every class/offset pair.

def TorchLean.Data.Bands.namedSamples (height width : ℕ) (specs : List (Class × ℕ)) (thickness : ℕ := 2) : List (String × Spec.Tensor Float (Spec.Shape.dim 1 (Spec.Shape.dim height (Spec.Shape.dim width Shape.scalar))) × ℕ)

Generate named samples for reports and prediction probes.

def TorchLean.Data.Bands.classes : List Class

Canonical label set for the band dataset: vertical ↦ 0, horizontal ↦ 1.

Typed Tensors (Tensor-First)

@[reducible, inline]

abbrev TorchLean.Data.Bands.shape : Shape

Canonical image shape for the band dataset (single-channel 4×4).

def TorchLean.Data.Bands.trainFloat : List (Spec.Tensor Float shape × ℕ)

Training set samples: a small list of (x, label) pairs.

def TorchLean.Data.Bands.probesFloat : List (String × Spec.Tensor Float shape × ℕ)

Probe set for reporting: (name, x, expectedLabel) triples.

def TorchLean.Data.Bands.dataset : Trainer.Dataset shape (Spec.Shape.dim 2 Shape.scalar)

Small vertical-versus-horizontal dataset with one-hot class targets.

def TorchLean.Data.Bands.probes : List (Trainer.ClassProbe shape)

Named vertical and horizontal inputs used to inspect a trained classifier.

def TorchLean.Data.Bands.probeSamples : List (String × Tensor.T Float shape × ℕ)

Concrete Float probe inputs for prediction examples.