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.

The one-step facts about discountedBackup over ℝ live here because every Bellman development (deterministic, finite stochastic, Markov kernel) builds its state-action value from it. Each of those files only has to bound its bootstrap term; the discount and the terminal mask are handled once.

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.

theorem Proofs.RL.Core.continueMask_nonneg (done : Bool) : 0 ≤ Spec.RL.continueMask done

continueMask is always nonnegative.

theorem Proofs.RL.Core.discountedBackup_mono {reward gamma b₁ b₂ : ℝ} (done : Bool) (hγ : 0 ≤ gamma) (hb : b₁ ≤ b₂) : Spec.RL.discountedBackup reward gamma b₁ done ≤ Spec.RL.discountedBackup reward gamma b₂ done

A backup is monotone in its bootstrap value when the discount is nonnegative.

theorem Proofs.RL.Core.discountedBackup_abs_sub_le {reward gamma b₁ b₂ bound : ℝ} (done : Bool) (hγ : 0 ≤ gamma) (hbound : 0 ≤ bound) (hb : |b₁ - b₂| ≤ bound) : |Spec.RL.discountedBackup reward gamma b₁ done - Spec.RL.discountedBackup reward gamma b₂ done| ≤ gamma * bound

A backup is gamma-Lipschitz in its bootstrap value.

theorem Proofs.RL.Core.eq_zero_of_le_mul_self {gamma d : ℝ} (hγ : gamma < 1) (hd : 0 ≤ d) (h : d ≤ gamma * d) : d = 0

A distance that is at most gamma times itself, with gamma < 1, is zero.