Flat-Case Lyapunov Contraction: Arithmetic Core

Pure arithmetic lemma for the flat-case bound: Fn1 + wn_sq/2 + Tn1 ≤ (1-a) * (Fn + Un/2 + Tn)

All quantities are real numbers. The geometric content (norms, inner products, projections) has been extracted by the caller.

Proof strategy

Use the function-value identity (1-a)·Fn = Fnprime − (1-a)·(Fnprime − Fn) − a·Fnprime and bound each piece: • Fn1 via descent: Fn1 ≤ Fnprime − η/2·(PGsq + PperpGsq) • (1-a)·(Fnprime − Fn) via segment estimate • a·Fnprime − a·ip_PperpG_en via aiming

After cancellations the remaining coefficients are all ≤ 0: • PGsq: −a·η/2 ≤ 0 • PperpGsq: 0 • ip_PG_PV, ip_PperpG_PperpV, ip_PperpG_en, Esq: cancel to 0 • PVsq: ((1-a)·εη − 3a − a²)/2 ≤ 0 (since εη ≤ a) • PperpVsq: (1-a)·(εη − a)/2 ≤ 0 (since εη ≤ a)

theorem PLAcceleratedNesterovLean.flat_case_arithmetic (a : ℝ) (ha_pos : 0 < a) (ha_lt1 : a < 1) (η μ sqrtμ sqrtη : ℝ) (hη_pos : 0 < η) (_hμ_pos : 0 < μ) (_hsqrtμ_nn : 0 ≤ sqrtμ) (_hsqrtη_nn : 0 ≤ sqrtη) (_hsqrtμ_sq : sqrtμ ^ 2 = μ) (_hsqrtη_sq : sqrtη ^ 2 = η) (_h_prod : sqrtμ * sqrtη = a) (εη : ℝ) (hεη_nn : 0 ≤ εη) (hεη_le : εη ≤ a) (Fn Fn1 Fnprime : ℝ) (_hFn_nn : 0 ≤ Fn) (_hFn1_nn : 0 ≤ Fn1) (_hFnp_nn : 0 ≤ Fnprime) (PVsq PperpVsq PGsq PperpGsq Esq : ℝ) (hPVsq_nn : 0 ≤ PVsq) (hPperpVsq_nn : 0 ≤ PperpVsq) (hPGsq_nn : 0 ≤ PGsq) (_hPperpGsq_nn : 0 ≤ PperpGsq) (_hEsq_nn : 0 ≤ Esq) (ip_PperpG_en ip_PG_PV ip_PperpG_PperpV ip_PperpV_en proj_error : ℝ) (_hproj_nn : 0 ≤ proj_error) (h_descent : Fn1 ≤ Fnprime - η / 2 * (PGsq + PperpGsq)) (h_segment : sqrtη * (ip_PG_PV + ip_PperpG_PperpV) ≥ Fnprime - Fn - εη / 2 * (PVsq + PperpVsq)) (h_aiming : ip_PperpG_en ≥ Fnprime + μ / 2 * Esq - proj_error) (wn_sq : ℝ) (hwn_sq : wn_sq = (1 - a) ^ 2 * PperpVsq + μ * Esq + η * PperpGsq + 2 * (1 - a) * sqrtμ * ip_PperpV_en - 2 * (1 - a) * sqrtη * ip_PperpG_PperpV - 2 * a * ip_PperpG_en) (Un : ℝ) (hUn : Un = PperpVsq + 2 * sqrtμ * ip_PperpV_en + μ * Esq) (Tn1 : ℝ) (hTn1 : Tn1 = (1 - a) / 2 * PVsq - (1 - a) * sqrtη * ip_PG_PV + (1 - a) * η / 2 * PGsq) (Tn : ℝ) (hTn : Tn = (1 + a) ^ 2 / (2 * (1 - a)) * PVsq) : Fn1 + wn_sq / 2 + Tn1 ≤ (1 - a) * (Fn + Un / 2 + Tn) + a * proj_error

The main arithmetic assembly for the flat-case Lyapunov contraction.

Parameters represent extracted real values from the geometric proof: • a = √(μ·η), the contraction rate • Fn, Fn1 = function gaps at steps n, n+1 • Fnprime = function gap at lookahead point x'_n • PVsq, PperpVsq = ‖P v‖², ‖P⊥ v‖² • PGsq, PperpGsq = ‖P g‖², ‖P⊥ g‖² • Esq = ‖e_n‖² • Various inner products