Sharp Euler approximation rate conditional on saddle analysis
ProvedEulerMascheroni.P2.sharp_rate_of_saddlesasymptoticseuler-mascheroniformalization
Assume the two normalized saddle limits and infinitely many indices at which |sin(phase_(n+1))|≥1/2. Then the explicit Euler approximants have sharp exponential rate c=5(1−cos(2π/5)): every slightly weaker exponential upper bound holds eventually, and every slightly stronger exponential lower bound holds infinitely often. This zero-safe statement allows exact zero errors at other indices. The analytic hypotheses remain explicit.
Preamble
import Definitions.Def_eulerMascheroni_p2Approximation open Filter Topology open EulerMascheroni.P2
Formal statement
theorem EulerMascheroni.P2.sharp_rate_of_saddles (h : SaddleLimits)
(hphase : ∃ᶠ n : ℕ in atTop, (1/2 : ℝ) ≤ |Real.sin (phase (n+1))|) :
SharpRate := by sorry
Source
Local SADDLE_DRAFT.md sections 4–5, derived from the explicit family in Van Assche–Wolfs, https://arxiv.org/html/2404.09799v3, section 5. Conditional transfer and elementary model limit, not an assertion of the full saddle asymptotics.