DQN Runtime Algebra Proofs

This module proves small but high-value algebraic facts about the DQN runtime helpers.

The main target is target-network soft updates. TorchLean's element-arithmetic runtime interface is intentionally law-light, so algebraic identities are stated over ℝ, where ring laws are available. This avoids claiming that arbitrary executable arithmetic backends satisfy mathematical ring axioms definitionally.

References:

• Mnih et al., "Human-level control through deep reinforcement learning" (2015), target networks.
• Polyak and Juditsky, "Acceleration of Stochastic Approximation by Averaging" (1992), averaging.

@[simp]

theorem Proofs.RL.DQN.updateTarget_zero (online target : ℝ) : Runtime.RL.DQN.updateTarget 0 online target = target

With τ = 0, a soft target update leaves the target unchanged.

@[simp]

theorem Proofs.RL.DQN.updateTarget_one (online target : ℝ) : Runtime.RL.DQN.updateTarget 1 online target = online

With τ = 1, a soft target update copies the online value.

@[simp]

theorem Proofs.RL.DQN.updateTarget_self (tau x : ℝ) : Runtime.RL.DQN.updateTarget tau x x = x

If online and target parameters agree, soft update keeps that fixed point.

theorem Proofs.RL.DQN.updateTarget_sub_target (tau online target : ℝ) : Runtime.RL.DQN.updateTarget tau online target - target = tau * (online - target)

Soft update is exactly a convex-combination difference identity:

softUpdate τ online target - target = τ * (online - target).

This is the key algebraic fact behind target-network lag: each update moves the target by a τ-scaled online-target gap.