Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Erdős 699: index 7 is effective
P699 research · Erdős problem 699
Theorem. There is an effectively computable integer such that no bad triple has , for the original threshold .
The checker and certificate retain a complete finite proof. Its coefficient and Padé thresholds are effective. The subsequent numerical proof gives , and a separate finite certificate excludes a lower range. The new interval covers now join these ranges and give complete exclusion.
The retained proof uses polynomial certificates and joint source inequalities. Its initial cases have tree nodes and exact rational infeasibility certificates. The largest jet matrix has rows.
The main change is to use joint restrictions on the three cofactors. Replacing every analytic estimate by a separate alternative between two individual cofactor bounds discards information needed at this index.
Complete result. The combined proof excludes every admissible bad triple at seven. The source and polynomial estimates below are retained as components of that proof.
Reducing the positions
For choose maximizing , and put
Every admissible row has . Since each small prime occurs among the seven numerator factors, . Hence and .
The fixed-slope proposition shows that every bad triple satisfies
In particular, at least one selected position is zero. The main checker repeats that proposition's 780 exact slope-and-residue cases.
Coincident selected positions are handled by one polynomial certificate: the product of the selected prime powers at a common position divides , so the whole group has capacity one. With three primes and a coincidence, there are at most two such capacities. Rearrangement and nonincreasing row multiplicities cover every repeated-position assignment.
For distinct positions, there are assignments containing zero. The five retained old pair alternatives have six componentwise minimal witness vectors:
At least one vector gives coordinatewise lower bounds for . The exact proof covers all resulting cases.
The central column and polynomial factors
The central column is always good at index seven. Suppose is even. The three odd integers are pairwise coprime and exceed seven. If one has a prime factor at least eleven, that prime is active in . Otherwise one of the three integers is a power with , so seven is active. In either case, for an odd offset and an active prime power ,
Kummer therefore supplies a common prime at the central column. Thus a bad triple has .
This permits coordinate factors, row factors, and a diagonal factor in the interpolation certificates:
All are nonzero at in the remaining domain. The residual multiplicity at a grid point is
Each retained symmetric jet matrix has full row rank modulo . The nonvanishing lemma then gives an integer polynomial family, of the stated degree, with the prescribed row multiplicities and at least one nonzero value at . One certificate uses two coprime degree- kernel polynomials to save the extra degree in the general nonvanishing construction. Their full row rank, two actual modular kernel vectors, bivariate gcd equal to one, and a full-degree member are all checked. The coprime-kernel lemma lifts them to coprime integer polynomials and bounds their common zeros. For this certificate, every common zero has .
Factoring the row and diagonal lines is useful here: some otherwise plausible degree counts have forced line factors and do not give surjective jet maps.
Joint Padé inequalities
The source estimates come from the unequal-block Padé construction. For a selected seed and positive integer directions , let be its two certified decay rates. A positive rational parameter chooses the common approximation index .
For a prime component of seed exponent , multiplicity , and block length , the denominator-clearing cost is
The integer Padé inequality implies that, above an effective height,
where for two individual factors and for an AP product identity. The latter is used only when the actual selected positions satisfy ; its nonzero product gap is at most .
Every source uses a finite rational prime-interval sum with a strictly smaller rational coefficient-gcd rate. Directed interval arithmetic then rounds the positive-part intercepts upward and the right side of (1) downward, retaining a positive margin. Consequently the proof uses only rational inequalities
The source-clause helper recomputes these rational bounds. All analytic approximations have already been removed before the final linear-algebra verification.
Exact polynomial cuts and finite separation
Let be a nonvanishing polynomial supplied by a retained certificate, with total degree and row multiplicities . Badness, Kummer localization, and the selected cofactor bounds give
Here is explicitly computable. One may take
The factorial accounts for the small-prime factors away from their selected positions and for the possible cancellation of one factor of seven in . The coefficient norm is bounded effectively by maximal minors of the verified jet matrix.
Fix the exact slack . Beyond the computable height , (3) gives the necessary rational linear inequality
The proof includes the positive slack in every polynomial cut. It never replaces the limiting inequality by an unjustified strict boundary.
For each of the 540 initial cases, the certificate gives a finite tree. An internal node selects an applicable instance of (2) and branches over all nonempty sign sets. In each branch the signs and (2) become ordinary rational linear inequalities. At a leaf, the exact Farkas checker verifies positive rational weights such that
for the leaf's inequalities . Their weighted sum is impossible. Every leaf uses at most four inequalities.
Every child of every branch is present, all source position conditions are checked, and every initial position-and-vector case occurs exactly once. The coefficient and common-zero bounds together give the evaluated polynomial height threshold . This original proof left some source thresholds unevaluated; the linked numerical follow-up evaluates all of them using relaxed clauses and sharper polynomial bounds. Taking the maximum of the source and polynomial thresholds proves the theorem. Numerical optimization was used to discover the certificate; no numerical optimizer is used to verify its rational separation argument.