Candidate P2 arithmetic obligation: phase-compatible primitive saving

Open

EulerMascheroni.P2.phase_compatible_primitive_saving

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

diophantine-approximationirrationalityopen-problemresearch-obligation

This is a falsifiable, method-specific research obligation, not a known theorem. Determine whether the reduced P2 approximants satisfy the following assertion. With $b_n/a_n=P_n/Q_n$ in lowest terms, $a_n>0$ , and $c_n=a_n/Q_n$ , for every $\varepsilon>0$ and $N\in\mathbb N$ there exists $n\ge N$ such that

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

Together with the separate oscillatory asymptotic, this assertion is sufficient to produce nonzero integer linear forms tending to zero. No whole-sequence limit is required, but the phase and the arithmetic bound must hold at the same indices.

Research status. There is currently no proof or positive asymptotic evidence for this assertion. Exact rational computations at $n=320,640,1280$ instead give approximately $853.54,1893.26,4150.88$ for $\log_{10}(c_n\operatorname{fModel}(n))$ . These finite samples neither prove nor disprove the displayed subsequence assertion; they are adverse evidence. A disproof would rule out this particular sufficient P2 route, not prove rationality of Euler's constant or exclude other approximation families.

The proposed arithmetic investigation is prime-power control of the exact reduced denominator, using the factorial-binomial identity and finite modular truncations. Those identities are separate elementary theorems. They do not by themselves establish the saving demanded here.

Supporting arithmetic interfaces. See the exact primitive normalization, factorial-binomial denominator identity, factorial truncation modulo a divisor of a factorial, and prime-digit congruence. These concern exact normalization and local residues; they do not establish the global saving or its compatibility with the phase condition.

Preamble

import Definitions.Def_eulerMascheroni_p2PrimitiveNormalization
open Filter Topology
open EulerMascheroni.P2

Formal statement

theorem EulerMascheroni.P2.phase_compatible_primitive_saving : PrimitiveSaving := by sorry

Source

Exploratory obligation formulated for this mission, 12 September 2026; not a claim in the source paper. 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