Context α collects the arithmetic, order, constants, natural-number casts, and transcendental operations needed by scalar-polymorphic model code. It carries no laws.

LawfulContext α records, for a scalar type that also carries a Mathlib linearly ordered field structure, that the Context dictionary computes the same addition, multiplication, subtraction, division, negation, order, maximum, minimum, absolute value, and small numeric constants as the field, and that its epsilon is positive. The instance for ℝ is proved; transcendental constants and the total power operation stay unconstrained.

This separation lets executable scalar types provide operations without claiming field laws that rounded arithmetic cannot satisfy. A theorem using LawfulContext can transfer the listed operations to Mathlib's field structure. It still needs any further hypotheses about logarithms, exponentials, or powers explicitly; the class does not supply those analytic facts.

Spec.Shape is List Nat, the dimensions outermost first, and it indexes TorchLean.Tensor α s, so tensor dimensions are present in the type. Each value stores one contiguous row-major buffer with a proof that its length equals the shape's element count. Storage α selects packed FloatArray storage for Float, ByteArray for UInt8, and ordinary arrays for other scalars. Proofs observe this same value through coordinate lookup; the storage invariant does not prove the correctness of native C or CUDA implementations.

A shape is well formed when every one of its dimensions is positive.

The empty list of dimensions satisfies this condition and describes one scalar coordinate. A shape with a zero axis instead has no elements and fails the condition. This distinction is why positivity of total size is a useful hypothesis for a mean or a normalization denominator.

CanBroadcastTo s₁ s₂ records when values with shape s₁ can be expanded to shape s₂.

toEuclidean is a linear equivalence between the real tensor representation at a shape and the Euclidean space indexed by its coordinates. The NormedAddCommGroup and InnerProductSpace ℝ instances on real tensors are induced along it, so a real tensor is a finite-dimensional inner-product space without a second representation.

Coordinates give the connection: each tensor entry becomes the corresponding coordinate of the Euclidean vector, and the inverse reconstructs those entries. The induced norm is therefore about the same values used by tensor operations. Analytic statements can use Mathlib's normed-space API without introducing a separate tensor conversion into every theorem.

A sequential GraphSpec records its parameter shapes, input shape, and output shape in its type. Graphs are built from identity, primitive, and sequential-composition nodes.

The pure interpreter evaluates a sequential graph on typed parameter and input tensors using scalar-polymorphic operations.

The runtime translation turns a sequential graph into an execution-polymorphic TorchLean program over the same scalar operations.

A typed DAG model pairs initialized parameters with a term whose environment contains the parameter and input shapes. Terms may name arguments and share intermediate results.

Sharing is represented by a typed reference into that environment. Two later operations can use one previously computed value without copying its defining term. The reference's shape determines which operations may consume it, while the environment records where the value came from.

The DAG interpreter evaluates the model body from typed parameter and input lists under the scalar context.

The DAG lowering pass turns the same model body into an execution-polymorphic TorchLean program over the same scalar operations.

The sequential GraphSpec MLP composes two linear maps with an intervening ReLU. Its type fixes the order and shapes of both weights and biases.

The Boolean structural predicate checks that node identifiers match their array positions, operation arities are valid, and every parent points to an earlier node.

The diagnostic checker enforces the same conditions as the Boolean structural predicate, but returns the first useful error message instead of a bare false. The two implementations are kept separate; no equivalence theorem currently connects them.

After the structural check, shape validation infers every node's output shape and compares it with the shape stored in the graph.

After the structural check, IR denotation evaluates every node into a table of shape-tagged tensor values using scalar-polymorphic operations and the supplied external payload.