Ordinary calculations on the existing autograd tape

Function.run uses this internal frontend when recording an ordinary scalar or tensor function. Supported arithmetic, reductions and matrix products become existing Ops calls. Shared local bindings stay shared. Eager execution records those calls on its tape; no second differentiation engine or gradient representation is introduced.

The frontend checks equality of the translated operation recipe in Lean's kernel. No ring simplification, reassociation, precision conversion or speculative derivative is used. This equality is not a proof of a foreign backend's implementation. Analytic correctness still uses the existing local derivative laws and graph-composition theorems.

The call site's input supplies the element type and shape. Captured scalars and tensors are constants, not learnable parameters. Quotients and direct negation use the existing operation interface. Scalar conditionals inspect the current value and record only the selected branch; on GPU, this decision synchronizes to Lean. Fixed-parameter recurrences record their steps on the same tape. Neither feature supplies a derivative at a discontinuous branch boundary.

structure TorchLean.autograd.Result (α : Type) [Storage α] (input output : Shape) : Type

A forward value and its recorded input pullback. Backward consumes the recording; close releases it without differentiation. The value remains usable after either operation.

• value : Tensor α output

  Materialized forward value, retaining the requested element type.

• device : NN.Backend.Device

  Effective device, including a precision-preserving CPU fallback.

• pullback : Tensor α output → IO (Tensor α input)

  Consume the existing tape with an explicit output cotangent.

• close : IO Unit

  Release an unused recording. Calling this more than once is harmless.

def TorchLean.autograd.Result.backward {α : Type} [Storage α] [One α] {input output : Shape} (result : Result α input output) (seed : Tensor α output := Tensor.full output 1) : IO (Tensor α input)

Differentiate with the supplied cotangent. The default differentiates the sum of output entries. The recording is released even when backward fails; a consumed recording cannot be reused.

@[instance_reducible]

instance TorchLean.autograd.instReprResultOfTensor {α : Type} [Storage α] {input output : Shape} [Repr (Tensor α output)] : Repr (Result α input output)

def TorchLean.autograd.Internal.iterate {m : Type → Type} [Monad m] {β : Type} (step : ℕ → β → m β) : ℕ → m β → m β

Record each step on the existing tape, retaining the order of a scalar or tensor recurrence.

theorem TorchLean.autograd.Internal.recurrence_eq {α : Type} (f : ℕ → α) (initial : α) (step : ℕ → α → α) (hzero : f 0 = initial) (hsucc : ∀ (n : ℕ), f (n + 1) = step n (f n)) (n : ℕ) : Nat.rec initial step n = f n

Constructor equations identify a recurrence without imposing algebraic laws or reassociation.

structure TorchLean.autograd.Internal.Recording (α : Type) [Storage α] (input output : Shape) : Type 1

An element context and a program using only the existing operation interface.

• context : Context α
• program {m : Type → Type} [Monad m] [Runtime.Autograd.Torch.Ops m α] : Runtime.ValueRef m α input → m (Runtime.ValueRef m α output)

def TorchLean.autograd.Internal.Recording.elementwise {α : Type} [Storage α] {shape : Shape} (recording : Recording α [] []) : Recording α shape shape

Lift scalar control flow through the existing balanced tensor traversal. No unselected branch is evaluated. GPU arithmetic and backward stay on the GPU; scalar decisions synchronize to Lean.

def TorchLean.autograd.Internal.Recording.run {α : Type} [Storage α] [transfer : Runtime.Autograd.Torch.TensorTransfer α] {input output : Shape} (recording : Recording α input output) (value : Tensor α input) (device : NN.Backend.Device) (grad : Bool := true) : IO (Result α input output)

Execute through the existing eager session, owned until backward or explicit close.

def TorchLean.autograd.Internal.programStx : Lean.ParserDescr

Internal call-site translation; ordinary function definitions need no recording annotation.

def TorchLean.autograd.Internal.elaborateProgram : Lean.Elab.Term.TermElab