Sharp exponential error rate for the explicit second-order Euler approximants

For the explicit p=2 rational Euler approximants, every exponential upper bound with constant c−epsilon holds eventually, and the lower bound with c+epsilon holds infinitely often, where c=(25−5 sqrt(5))/4. This is a proposed refinement under review. Its accepted Lean sketch has exactly two open analytic leaves: the denominator saddle limit and the oscillatory remainder saddle limit. The phase noncancellation and the deductions from the saddle estimates have accepted proofs. The claimed saddle estimates remain unproved.

Connection to the Euler tree (12 September 2026). The refexplicit p=2 approximation branch studies the size of rational approximation errors. The proved refconditional irrationality bridge shows that its numerator asymptotic, the proved refphase noncancellation, and a successful integer normalization would imply refirrationality of Euler’s constant. The required normalization consists of nonzero scalars c_n making both c_n P_(n+1) and c_n Q_(n+1) integers while c_n fModel_(n+1) tends to zero. No such scalars have been constructed. This is an explicit candidate route to the refvanishing integer linear forms leaf: one would select the infinitely many nonzero forms and normalize denominator signs. That connection is explanatory; it is not a submitted proof discharging the existence leaf. The mixed E/Gevrey lifting obligations in the reftranscendence tree remain open. Irrationality alone would not prove transcendence.