Primitive integer normalization of the P2 rational approximants

Definition

eulerMascheroni_p2PrimitiveNormalization

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

diophantine-approximationformalizationirrationality

For the rational approximants $P_n,Q_n$ of the P2 family, write the reduced fraction

P_n/Q_n=b_n/a_n,\qquad a_n>0,\quad \gcd(a_n,b_n)=1.

Define the integer numerator $b_n$ , positive natural denominator $a_n$ , and real multiplier

c_n=a_n/Q_n.

The predicate PrimitiveSaving records the following candidate condition on these explicit sequences: for every $\varepsilon>0$ and every $N\in\mathbb N$ , some $n\ge N$ satisfies

|\sin(\operatorname{phase}(n+1))|\ge\tfrac12, \qquad c_{n+1}\operatorname{fModel}(n+1)<\varepsilon.

The two inequalities must hold at the same indices. This definition does not assert the predicate. Its truth is an open, method-specific research question; the elementary normalization and its conditional consequences can be proved without assuming that this question has a positive answer.

Definition code

import Definitions.Def_eulerMascheroni_p2Approximation

namespace EulerMascheroni.P2

def primitiveP (n : ℕ) : ℤ := (P n / Q n).num
def primitiveQ (n : ℕ) : ℕ := (P n / Q n).den
noncomputable def primitiveScale (n : ℕ) : ℝ := (primitiveQ n : ℝ) / (Q n : ℝ)

/-- A candidate arithmetic obligation, not an asserted theorem. The phase and
small primitive envelope must occur at the same arbitrarily large indices. -/
def PrimitiveSaving : Prop := ∀ ε : ℝ, 0 < ε → ∀ N : ℕ,
  ∃ n : ℕ, N ≤ n ∧ (1/2 : ℝ) ≤ |Real.sin (phase (n+1))| ∧
    primitiveScale (n+1) * fModel (n+1) < ε

end EulerMascheroni.P2

Source

Derived auxiliary results for the p=2, x=1 family in Van Assche–Wolfs, Rational approximation of Euler’s constant using multiple orthogonal polynomials, arXiv:2404.09799v3, Section 5, displayed binomial formula for F_(n;2)^(I|p), https://arxiv.org/html/2404.09799v3#S5. The reduced-fraction normalization and conditional subsequence criterion are elementary deductions supplied here, not named statements or arithmetic-saving claims in that paper.

View graph