Erdős 699: a numerical stopping bound for index nine

This is a retained earlier research note. The current reading guide gives the latest status and distinguishes completed proofs from remaining cases.

P699 research · The original effective proof · Joint Padé constants

Theorem. Every bad triple $(n,9,j)$ for the original prime threshold $p\ge9$ satisfies

Every source threshold is numerical. This is a stopping bound; the finite range below it is not excluded by this note. The separate finite proof excludes $n\le10^{241547629}$. The numerical-tail checker and data combine the analytic sources with complete coverage of the root cases.

Complete result. The combined proof excludes every admissible bad triple at nine. The estimates below are retained as components of that proof.

Initial cofactor bounds

Write $h=n-8$. For each $p\in\{2,3,5,7\}$ choose a position $r_p\in\{0,\ldots,8\}$ maximizing $v_p(n-r_p)$, and put

The proof lowers each endpoint of the original nineteen pair alternatives by exactly $1/10000$. This modest change allows larger strict analytic margins. Eleven numerical pair certificates imply all nineteen weakened alternatives; the four ordinary arithmetic-progression sources used in the original forest retain their targets.

The initial-source checker verifies every implication with rational arithmetic and matches the nineteen edges against the relaxed baseline. Its data give the common uniform bound

The largest threshold comes from the $(2,5)$ alternative with targets $(.2675,.2710)$. For comparison, the symmetric $(2,5)$ target $(.2678,.2678)$ uses seed $128-125=3$ and directions $(79,18,79)$, with exponent $2790743305738$.

The complete initial-source interval covers lower this requirement to $h\ge10^{241547627}$. They retain 299324 witnesses for all eleven pair sources and four ordinary product sources, joining their explicit cofactor boxes to the numerical tails above.

Coincident positions are included. The joint integer argument permits actual gap zero; alternatively $r_p=r_q$ gives $u_pu_q\ge h$, which rules out two cofactor upper bounds whose exponents sum to less than one. The four ordinary AP sources have nonzero position step of absolute value at most four, hence product gap at most sixteen.

Joint cofactor bounds

All 790 joint sources have numerical thresholds from the finite-constant argument. The source thresholds $R$ are weakened individually, leaving every positive-part intercept and sign condition unchanged. The exact forest verifies these weakenings simultaneously.

The joint-source checker uses 739 uniform coefficient-gcd certificates. They combine BFT's prime intervals with the retained global Chebyshev bounds of Broadbent et al. and the finite-range bound of Johnston–Yang, patched by global estimates. The numerical source data give the common height

This maximum comes from source_0406, with directions $(32,25,45)$, block parameter $1352650/866762331$, and uniform gcd starting index $m_0=10^{11}$. Every factorial prefactor, integral maximum, residual denominator cost, and exponential decay margin is included numerically.

Adjusting the joint witness blocks

The block adjustment lemma keeps every source intercept and weakened threshold fixed while reducing the denominator cost for a smaller witness block. The adjusted numerical checker and certificates cover all 790 clauses using 647 uniform gcd bounds. The full replay checks every numerical clause and every uniform gcd certificate.

Their new common joint-source height is

The largest threshold now comes from source_0647. Altogether 595 individual source bounds improve. At the polynomial height $h\ge10^{241547627}$, 440 clauses already hold directly; lowering the other source heights is a separate finite-cover calculation.

Complete polynomial coverage

The relaxed baseline uses all 128 retained polynomial certificates. It checks $9^4\cdot16=104976$ labeled position and cofactor cases, including prime-position collisions. Polynomial inequalities directly cover 104148 of them, leaving 828 cases.

The relaxed forest and proof data close all 828 remaining cases. They retain 32165 nodes and 24322 exact Farkas leaves. Each leaf uses positive rational multipliers canceling every cofactor variable. The checker verifies a strictly negative combined right side.

The polynomial constants are bounded using the retained Newton basis. The arithmetic nonvanishing certificates remove the two largest common-zero height requirements. Combining the remaining common-zero bounds, the baseline coefficient bounds, and the exact weighted leaf bound

gives the polynomial starting height $h\ge10^{241547627}$. The interpolation ranks are unchanged; this calculation uses the existing rank and kernel certificates.

Combining the bounds

The initial-source interval covers and polynomial argument both apply from $h\ge10^{241547627}$. The adjusted joint bound (4) is larger. Thus every hypothetical bad triple has $n-8<10^{11514327437547}$. Adding one decimal power absorbs the row shift and proves (1).

The numerical-tail checker matches the initial pair list, all source identifiers, all individual threshold weakenings, and the full relaxed forest. It names its inputs by basename, checks that each named file is present, replays the exact coverage without recomputing ranks, and lists its inputs by basename in its own output as a run record, not as a condition for running.

With the retained interpolation dependencies installed, run:

.venv/bin/python wiki/research/erdos_699/computations/erdos_699_index_9_numerical_tail.py

The additional --sources option regenerates the numerical analytic constants as well, including the adjusted joint sources. Neither command enumerates binomial rows.