RL Core Proofs

The shared tensor horizon enforces trajectory alignment in the type. The pointwise law below states what each reconstructed return means, rather than restating a container-size invariant.

theorem Proofs.RL.Core.returnsFromAdvantages_getScalar {α : Type} [TorchLean.Storage α] [Add α] {n : ℕ} (advantages values : TorchLean.Tensor α [n]) (index : Fin n) : (Spec.RL.returnsFromAdvantages advantages values).getScalar index = advantages[index] + values[index]

Every lambda-return is its advantage plus its baseline value at the same timestep.