Elementwise eager-engine operations.

This file contains scalar-lifted tensor nodes and their runtime/autograd implementation, including arithmetic, comparisons, activations, and loss-adjacent pointwise operations.

def Runtime.Autograd.Tape.add {α : Type} [TorchLean.Storage α] [Add α] {s : Spec.Shape} (t : Tape α) (aId bId : ℕ) : Result (Tape α × ℕ)

Elementwise addition. PyTorch: torch.add / +.

def Runtime.Autograd.Tape.sub {α : Type} [TorchLean.Storage α] [Sub α] [Zero α] {s : Spec.Shape} (t : Tape α) (aId bId : ℕ) : Result (Tape α × ℕ)

Elementwise subtraction. PyTorch: torch.sub / -.

def Runtime.Autograd.Tape.mul {α : Type} [TorchLean.Storage α] [Mul α] {s : Spec.Shape} (t : Tape α) (aId bId : ℕ) : Result (Tape α × ℕ)

Elementwise multiplication. PyTorch: torch.mul / *.

def Runtime.Autograd.Tape.div {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (t : Tape α) (aId bId : ℕ) : Result (Tape α × ℕ)

Elementwise division. PyTorch: torch.div / /. Backward is the ordinary quotient rule, valid for nonzero denominators: ∂(a/b)/∂a = 1/b, ∂(a/b)/∂b = −a/b² (mirrors the CUDA div node; negation subtracts from Tensor.full s 0 as sub does, so no Neg α is required).

Domain: real calculus does not define the derivative of a/b at b = 0, so this backward is the genuine quotient rule only where b ≠ 0. The carrier's / (and hence divSpec) may totalize or be backend-dependent at b = 0, but no real-valued gradient is implied there.

Requires [TorchLean.Storage α] [Context α] like the sibling abs/sqrt/exp nodes (its divSpec forward rides the carrier's /).

def Runtime.Autograd.Tape.scale {α : Type} [TorchLean.Storage α] [Mul α] {s : Spec.Shape} (t : Tape α) (xId : ℕ) (c : α) : Result (Tape α × ℕ)

Multiply a tensor by a scalar constant. PyTorch: x * c for Python scalar c.

def Runtime.Autograd.Tape.abs {α : Type} [TorchLean.Storage α] [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] {s : Spec.Shape} (t : Tape α) (xId : ℕ) : Result (Tape α × ℕ)

Elementwise absolute value.

Backward uses the sign function (signSpec) as a subgradient at 0. PyTorch comparison: torch.abs.

def Runtime.Autograd.Tape.sqrt {α : Type} [TorchLean.Storage α] [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] {s : Spec.Shape} (t : Tape α) (xId : ℕ) : Result (Tape α × ℕ)

Elementwise square root.

Backward uses 1 / (2 * sqrt(x)) for x > 0 and 0 otherwise (totalized). PyTorch comparison: torch.sqrt.

def Runtime.Autograd.Tape.clamp {α : Type} [TorchLean.Storage α] [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] {s : Spec.Shape} (t : Tape α) (xId : ℕ) (minVal maxVal : α) : Result (Tape α × ℕ)

Elementwise clamp to [minVal, maxVal].

Backward multiplies by an indicator of the open interval (minVal, maxVal) (zero at boundaries). PyTorch comparison: torch.clamp.

def Runtime.Autograd.Tape.max {α : Type} [TorchLean.Storage α] [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] {s : Spec.Shape} (t : Tape α) (aId bId : ℕ) : Result (Tape α × ℕ)

Elementwise maximum.

Tie-breaking: when a = b, the upstream gradient is split evenly (0.5) between both inputs. PyTorch comparison: torch.maximum.

def Runtime.Autograd.Tape.min {α : Type} [TorchLean.Storage α] [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] {s : Spec.Shape} (t : Tape α) (aId bId : ℕ) : Result (Tape α × ℕ)

Elementwise minimum.

Tie-breaking: when a = b, the upstream gradient is split evenly (0.5) between both inputs. PyTorch comparison: torch.minimum.

def Runtime.Autograd.Tape.sin {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (t : Tape α) (xId : ℕ) : Result (Tape α × ℕ)

Record elementwise sine with the VJP from Spec.sinOp.

The tape retains the input for cos(x) * dLdy, so the backward pass uses the same angle as the forward pass even when different angles produce the same sine value.

def Runtime.Autograd.Tape.cos {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (t : Tape α) (xId : ℕ) : Result (Tape α × ℕ)

Record elementwise cosine with the VJP -sin(x) * dLdy from Spec.cosOp.

def Runtime.Autograd.Tape.relu {α : Type} [TorchLean.Storage α] [Mul α] [Zero α] [Max α] [BEq α] [One α] [LT α] [DecidableRel fun (x1 x2 : α) => x1 > x2] {s : Spec.Shape} (t : Tape α) (xId : ℕ) : Result (Tape α × ℕ)

Elementwise ReLU.

PyTorch comparison: torch.relu(x) / torch.nn.functional.relu(x).