Complex-saddle asymptotic for the explicit Euler remainder
OpenEulerMascheroni.P2.f_saddle_limitasymptoticseuler-mascheroniresearch-target
The explicit remainder F_n=Q_n gamma−P_n has the stated oscillatory asymptotic with an additive error tending to zero after division by fModel. This is the substantive analytic target of sections 1–3 of the local draft. The contour argument is under review; this is not presented as a verified theorem or as a theorem proved in the cited paper.
Preamble
import Definitions.Def_eulerMascheroni_p2Approximation open Filter Topology open EulerMascheroni.P2
Formal statement
theorem EulerMascheroni.P2.f_saddle_limit : Tendsto (fun n : ℕ => F (n+1) / fModel (n+1) - Real.sin (phase (n+1))) atTop (nhds 0) := by sorry
Source
Explicit family: Van Assche–Wolfs, https://arxiv.org/html/2404.09799v3, section 5. Proposed p=2 refinement: local SADDLE_DRAFT.md, 11 September 2026. Proof-under-review research target; NOT attributed to an established theorem in the source.