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.

@[inline]

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

Elementwise addition. PyTorch: torch.add / +.

@[inline]

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

Elementwise subtraction. PyTorch: torch.sub / -.

@[inline]

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

Elementwise multiplication. PyTorch: torch.mul / *.

@[inline]

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

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.

The executable rule needs only division, multiplication, subtraction and zero; it does not require transcendental operations or an ordering on the scalar type.

@[inline]

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

Direct elementwise negation; unlike subtraction from zero, this preserves signed zero.

@[inline]

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

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

@[inline]

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

Elementwise absolute value.

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

@[inline]

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

Elementwise square root.

Uses the shared square-root specification and its range-checked weighted backward rule. Outside the positive region, the local zero factor still multiplies the upstream value. PyTorch comparison: torch.sqrt.

@[inline]

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

Elementwise clamp to [minVal, maxVal].

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

@[inline]

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

Elementwise maximum.

Tie-breaking: when a = b, the upstream gradient is split evenly (0.5) between both inputs. When both arguments name the same node, range-checked carriers combine its two contributions before graph accumulation. This avoids rounding a representable gradient to zero in each half. Other carriers retain the separate-contribution schedule. PyTorch comparison: torch.maximum.

@[inline]

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

Elementwise minimum.

Tie-breaking: when a = b, the upstream gradient is split evenly (0.5) between both inputs. Repeated references use the same coalesced-contribution convention as Tape.max on range-checked carriers; distinct nodes retain their separate halves. PyTorch comparison: torch.minimum.

@[inline]

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

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.

@[inline]

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

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

@[inline]

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 (Spec.SomeTensor α)) (xId : ℕ) : Result (Tape (Spec.SomeTensor α) × ℕ)

Elementwise ReLU.

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