Exponential rate of the explicit fifth-root saddle models

Proved

EulerMascheroni.P2.model_rate

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

asymptoticseuler-mascheroniformalization

For the explicit positive saddle models, log(fModel_(n+1)/qModel_(n+1))/scale_(n+1) tends to −c, where c=5(1−cos(2π/5)). This concerns the models themselves and makes no claim that the binomial sums have these asymptotics.

Preamble

import Definitions.Def_eulerMascheroni_p2Approximation
open Filter Topology
open EulerMascheroni.P2

Formal statement

theorem EulerMascheroni.P2.model_rate :
    Tendsto (fun n : ℕ => Real.log (fModel (n+1) / qModel (n+1)) / scale (n+1))
      atTop (nhds (-rate)) := 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.

View graph