Positive Euler denominators and exact fifth-root rate
ProvedEulerMascheroni.P2.foundationeuler-mascheroniformalizationrational-approximation
For every nonnegative integer n the explicit rational denominator Q_n is strictly positive. The saddle rate c=5(1-cos(2π/5)) equals (25-5√5)/4 and satisfies 0<c<5. This checks the numerical constant and ensures the rational approximants are defined; it does not establish an asymptotic estimate.
Preamble
import Definitions.Def_eulerMascheroni_p2Approximation open Filter Topology open EulerMascheroni.P2
Formal statement
theorem EulerMascheroni.P2.foundation :
(∀ n : ℕ, 0 < Q n) ∧
rate = (25 - 5 * Real.sqrt 5) / 4 ∧
0 < rate ∧ rate < 5 := 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.