Relative Euler error from two explicit saddle limits

Proved

EulerMascheroni.P2.relative_asymptotic

by shivm · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

euler-mascheroniformalizationrational-approximation

Assume the two normalized saddle limits for the explicit p=2 Euler approximants. Then there exists a real sequence w_n tending to zero such that, eventually, γ−P_(n+1)/Q_(n+1)=(fModel_(n+1)/qModel_(n+1))(sin(phase_(n+1))+w_n). The analytic saddle limits are explicit hypotheses; this theorem proves the stability and division step, not those limits.

Preamble

import Definitions.Def_eulerMascheroni_p2Approximation
open Filter Topology
open EulerMascheroni.P2

Formal statement

theorem EulerMascheroni.P2.relative_asymptotic (h : SaddleLimits) :
    ∃ w : ℕ → ℝ, Tendsto w atTop (nhds 0) ∧
      ∀ᶠ n : ℕ in atTop,
        Real.eulerMascheroniConstant - (P (n+1) : ℝ) / (Q (n+1) : ℝ) =
          (fModel (n+1) / qModel (n+1)) * (Real.sin (phase (n+1)) + w n) := by sorry

Source

Van Assche–Wolfs, https://arxiv.org/html/2404.09799v3, section 5 for the family. Local p=2 proof draft SADDLE_DRAFT.md, sections 4–5. These are elementary supporting results and a conditional reduction, not novelty claims.

View graph