Core Reinforcement-Learning Runtime Helpers

This module adds the tensor-shaped and runtime layer pieces that sit on top of the mathematical RL core in NN.Spec.RL.Core.

Keeping Bellman / return / GAE definitions in the spec layer avoids an awkward split where the same mathematics would otherwise exist in both runtime and proof namespaces. This file therefore only keeps:

• a typed transition record for tensor-valued states and discrete actions,
• public exports of the spec return and advantage helpers,
• and scalar losses commonly used by deep RL objectives.

structure Runtime.RL.Core.Transition (α : Type) [TorchLean.Storage α] (σ : Spec.Shape) (nActions : ℕ) : Type

A typed one-step transition for discrete-action RL over a tensor-valued state.

• state : TorchLean.Tensor α σ

  Current state s_t.

• action : Fin nActions

  Discrete action a_t.

• reward : α

  Reward r_t.

• nextState : TorchLean.Tensor α σ

  Next state s_{t+1}.

• done : Bool

  Whether nextState is terminal. TD targets drop the bootstrap term when this is set, so set it only for true termination; a time-limit truncation should leave it false.

def Runtime.RL.Core.squaredError {α : Type} [Context α] (prediction target : α) : α

Squared-error helper used by critic / TD objectives.

def Runtime.RL.Core.huberLoss {α : Type} [Context α] (prediction target : α) (delta : α := 1) : α

Scalar Huber loss used by robust TD objectives.

We use the standard piecewise form:

• quadratic region: (pred - target)^2 / 2
• linear region: delta * (|pred - target| - delta / 2)

This is the HuberLoss convention, not the rescaled SmoothL1Loss convention. The intended domain is delta > 0.