Per-Phase Gen Convergence (State-Based Local Argument)

State-based ("gen") version of LocalArgument.lean. For each m⋆ ∈ M, chains local_fiberwise_geometry, lyapunov_coercivity_gen, curv_absorb_assembly_gen, lyapunov_contraction_gen, motion bounds, and bootstrap_total_displacement_gen

to produce a ball around m⋆ where the Nesterov iterates starting from an arbitrary initial state s₀ (not just v=0) converge geometrically.

State-based version of LocalArgument.lean. The conclusion provides gen bootstrap output: ∃ δ > 0, ∀ s₀ near m⋆ with small Lyapunov → iterates stay in Ω ∧ Lyapunov decays geometrically with nesterovSeqGen.

theorem PLAcceleratedNesterovLean.local_convergence_at_base_point_gen {d : ℕ} (hd : 0 < d) (L : NNReal) (hL : 0 < ↑L) (μ : ℝ) (hμ : 0 < μ) (hμ_le_L : μ ≤ ↑L) (μ_minus : ℝ) (hμ_minus : 0 < μ_minus) (hμ_minus_lt : μ_minus < μ) (θ : ℝ) (hθ : 0 < θ) (hθ_lt1 : θ < 1) (f : E d → ℝ) (S : Set (E d)) (hrange : S = argminSet f) (U : Set (E d)) (hTub_sub : IsTubularNeighborhoodOfSubmanifold S U) (hPL : PolyakLojasiewicz f μ U) (hf_C2 : ContDiffOn ℝ 2 f U) (hf_lip : LipschitzOnWith L (gradient f) U) (π : E d → E d) (hπ_on_U : ∀ x ∈ U, π x ∈ S ∧ dist x (π x) = Metric.infDist x S) (hπ_fix : ∀ x ∈ S, π x = x) (hπ_in_S : ∀ (x : E d), π x ∈ S) (hgrad_zero : ∀ x ∈ S, gradient f x = 0) (mstar : E d) (hmstar : mstar ∈ S) : have η := 1 / ↑L; have ρ := (1 - √(μ_minus * η)) / (1 + √(μ_minus * η)); have P := fderiv ℝ π mstar; ∃ (Ω : Set (E d)) (δ : ℝ) (r_ball : ℝ) (C_coer : ℝ), IsOpen Ω ∧ mstar ∈ Ω ∧ Ω ⊆ U ∧ 0 < δ ∧ 0 < r_ball ∧ 0 < C_coer ∧ Metric.ball mstar r_ball ⊆ Ω ∧ (∀ (x : E d), P (P x) = P x) ∧ (∀ (v : E d), ‖P v‖ ≤ ‖v‖) ∧ μ_minus * η < 1 ∧ (∀ (s : NesterovState d), s.x ∈ Ω → s.lookahead η ∈ Ω → ‖s.v‖ ^ 2 + μ_minus * ‖normalDispOfState π η s‖ ^ 2 ≤ C_coer * lyapunovOfState P μ_minus π f η s) ∧ ∀ (s₀ : NesterovState d), s₀.x ∈ Metric.ball mstar δ → s₀.lookahead η ∈ Metric.ball mstar δ → lyapunovOfState P μ_minus π f η s₀ ≤ δ ^ 2 → (∀ (n : ℕ), (nesterovSeqGen f η ρ s₀ n).x ∈ Ω ∧ (nesterovSeqGen f η ρ s₀ n).lookahead η ∈ Ω) ∧ (∀ (n : ℕ), (nesterovSeqGen f η ρ s₀ n).x ∈ Metric.ball mstar r_ball ∧ (nesterovSeqGen f η ρ s₀ n).lookahead η ∈ Metric.ball mstar r_ball) ∧ (∀ (n : ℕ), lyapunovOfState P μ_minus π f η (nesterovSeqGen f η ρ s₀ (n + 1)) ≤ (1 - (1 - θ) * √(μ_minus * η)) ^ (n + 1) * lyapunovOfState P μ_minus π f η s₀) ∧ ∀ (j : ℕ) (t : ℝ), 0 ≤ t → t ≤ 1 → π ((nesterovSeqGen f η ρ s₀ j).lookahead η) + t • ((nesterovSeqGen f η ρ s₀ j).lookahead η - π ((nesterovSeqGen f η ρ s₀ j).lookahead η)) ∈ U

Public theorem wrapper for localConvergenceAtBasePointGenProof.