Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Erdős 699: index nine is effective
P699 research · Erdős problem 699 · Unequal Padé blocks · Coprime kernel polynomials
Theorem. There is an effectively computable integer such that any bad triple with satisfies . Here badness means
This uses the original prime threshold. The subsequent numerical proof gives , while a separate finite certificate excludes a lower range. The new interval covers join both ranges and complete the case. The theorem supplies a terminating procedure to enumerate the possible exceptional triples.
The complete checker and compressed proof data cover all labeled root cases. The finite case division concerns prime positions and cofactor inequalities, rather than rows .
Complete result. The combined proof excludes every admissible bad triple at nine. The estimates below are retained as components of that proof.
Cofactor variables and the complete root partition
For choose maximizing , and set
Every selected is at least . Admissibility gives , so and
The retained pair estimates give 16 componentwise minimal lower vectors for . The baseline checker reconstructs these vectors from their exact rational source endpoints and enumerates every position assignment, preserving prime labels. Its 70 integer polynomial certificates cover 104,059 root cases. The remaining 917 cases are listed explicitly in the baseline data.
Twelve remaining cases have coinciding positions. They are exactly , with a permutation of , and lower vector
They are included in the final proof trees. No collision case is inferred from a distinct-position calculation.
Polynomial inequalities, including collisions
Let have multiplicity at least at every nonnegative integer point . The Kummer divisibility argument and the bound on the unselected small-prime powers give, under badness,
provided . At a row occupied by several selected primes, their product divides and is at most . Let be the occupied rows, and let be the primes that are alone at their selected row. If has degree at most , then, above its computable coefficient threshold, badness necessarily implies
Thus a collision group has total capacity one and contributes no cofactor term to the left side of (1). This deliberately uses only that capacity bound. In addition, a group at a common position satisfies
and hence
For the twelve collision cases, (2) is . Equations (1) and (2), with the occupied-row constant in (1), are the exact inequalities used by the checker.
The polynomials have explicit coordinate, row, and diagonal factors, followed by a residual symmetric interpolation problem. The additional polynomial checker and data retain their integer multiplicities, modular ranks, and coefficient bounds. The proof uses 58 of these additional certificates together with the 70 baseline certificates. All required ranks were computed over ; the largest matrix is .
Two nonvanishing constructions are used. A surjective degree- jet map provides the established degree- family. Alternatively, two full-degree kernel polynomials whose reductions are coprime lift to coprime rational polynomials of degree . Their common zero set has an explicit resultant height bound. This second construction saves one degree and is essential for the tightest retained certificates. The coprime-kernel lemma supplies the integer lift and resultant bounds; the actual modular kernel vectors and gcd checks are retained.
Diagonal factors are permitted because the central column is impossible. If were bad, each of would have all prime factors in : any prime at least 11 in one of these odd factors creates a central Kummer carry. Each of 5 and 7 divides at most one of the four factors, since their pairwise distances are 2, 4, or 6. At least two would therefore be powers of 3 exceeding 12 and at distance at most 6. Distinct such powers differ by at least 54, a contradiction.
All coefficient and coprime-basepoint bounds used in the proof are satisfied once
This is the numerical bound for the polynomial part, not the full bound : the effective analytic source thresholds must also be included.
Analytic alternatives and exact linear contradictions
The source checker and compressed source data retain 790 directed interval certificates from the unequal-block Padé argument. They have the form
with exact rational . Each certificate reserves a strict analytic margin. Its coefficient-gcd lower bound is a finite rational sum, so the starting height is effectively computable. Pair estimates apply independently of the other positions; product estimates are used only when the checker verifies their required integer position identity. Four previously retained ordinary cofactor alternatives are also used.
To branch on (4), choose the nonempty set of its nonnegative summands. The sign conditions and their sum give rational linear inequalities. Every branch is retained, including equality boundaries. At each leaf, positive rational multipliers annihilate every variable coefficient while making the combined right side strictly negative. Thus the leaf would imply . These are exact Farkas certificates, checked using integer and rational arithmetic. Floating point linear programs were used only to find candidates.
The final forest has 31,615 nodes and 23,973 Farkas leaves. It closes every one of the 917 residual roots, including all twelve collision cases. Together with the independently reconstructed baseline partition, this covers all 104,976 root cases. Every input estimate has a computable threshold, and only finitely many are used. Taking their maximum, the polynomial threshold (3), and the elementary initial bounds proves the theorem.
The ordinary checker run reconstructs the directed sources and verifies
all exact coverage identities. Its optional --ranks flag repeats the
modular rank calculations already performed during construction. The
compressed artifacts are ordinary gzip files read by Python's standard
library. The remaining dependencies are pinned in the retained
interpolation requirements.