Auxiliary Variable Recursion for Arbitrary States

The one-step recursion for the auxiliary variable u, proved for arbitrary NesterovState (not just nesterovSeq-reachable states). This is the state-based analogue of auxVar_recursion from AuxVar.lean.

Key identity: u' = ((1-a)·P⊥v + √μ'·e - √η·P⊥g) + √μ'·ξ where u' = auxVarOfState at step(s), and all quantities are computed from s.

theorem PLAcceleratedNesterovLean.stepDispOfState_eq {d : ℕ} (f : E d → ℝ) (η ρ : ℝ) (s : NesterovState d) (hη_pos : 0 < η) : stepDispOfState f η ρ s = ρ • √η • s.v - (1 + ρ) • η • gradient f (s.lookahead η)

Step displacement formula: h = ρ·√η·v - (1+ρ)·η·g

theorem PLAcceleratedNesterovLean.auxVarOfState_step {d : ℕ} (P : E d →L[ℝ] E d) (μ' η ρ : ℝ) (π : E d → E d) (f : E d → ℝ) (s : NesterovState d) (hρ : ρ = (1 - √(μ' * η)) / (1 + √(μ' * η))) (ha_pos : 0 < √(μ' * η)) (hη_pos : 0 < η) (hμ_pos : 0 < μ') : have gn := gradient f (s.lookahead η); have en := normalDispOfState π η s; have ξn := curvatureErrorOfState (⇑P) π f η ρ s; have a := √(μ' * η); auxVarOfState P μ' π η (nesterovStep f η ρ s) = (1 - a) • (s.v - P s.v) + √μ' • en - √η • (gn - P gn) + √μ' • ξn

One-step auxVar recursion for arbitrary states.