1. Introduction
An architecture fixes how layers connect, but many different functions share that architecture. The weight values select one of them. A training run changes those values while retaining the same layer interfaces; saving a checkpoint records one particular state of that process. When we later ask Lean to prove something about a model, the statement must identify which of these objects it concerns. A shape theorem may apply to every parameter state, while an output bound will usually depend on the weights.
The running example keeps these distinctions visible in a small program. Its input has two coordinates and its output has one, so the forward map can be written out and compared with the layer definition. The same program supplies concrete tensors, gradients, and loss values for reading the API. Lean syntax enters as a way to express those objects and their relationships.