2.3 Four certificates

(a) If the lemma forces distinct primes \(p_1,\ldots,p_r\) to divide \(d\), then

(b) Combining this observation with \(q\geq7\) proves the following:

| \(k\) | interval primes \(p\leq k\leq2p\) | their product | certified bound on \(M\) |

|---:|---|---:|---:|

| 35 | \(19,23,29,31\) | \(392863\) | \(M\geq 13357343\) |

| 36 | \(19,23,29,31\) | \(392863\) | \(M\geq 13750206\) |

| 37 | \(19,23,29,31,37\) | \(14535931\) | \(M\geq 47045881=19^6\) |

| 38 | \(19,23,29,31,37\) | \(14535931\) | \(M\geq 47045881=19^6\) |

Proof of the certificates (a/b).

• For \(k=35\), assume \(M<13357343\). This is less than \(19^6\), hence less than every \(p^6\) in the row. The lemma with \(q\geq7\) forces all four primes into \(d\), giving

\[ M\geq1+34(392863)=13357343, \]

contradiction.

• For \(k=36\), the identical argument gives

\[ M\geq1+35(392863)=13750206. \]

• For \(k=37\), assume \(M<19^6\). All five primes are forced into \(d\), whence

\[ M\geq1+36(14535931)=523293517>19^6, \]

contradiction.

• For \(k=38\), the corresponding forced lower bound is

\[ 1+37(14535931)=537829448>19^6. \]

Thus the inequalities in the table are uniform in both \(n,d\), not outcomes of sampling.

2.4 Exact size of the excluded finite regimes

(a) For step \(s=k-1\), the number of all positive pairs \((n,d)\) with \(n+sd \[ R_s(B)=D(B-1)-s\frac{D(D+1)}2,\qquad D=\left\lfloor\frac{B-2}{s}\right\rfloor. \]

Möbius inversion gives the exact number of primitive pairs:

(d) A from-scratch linear Möbius sieve evaluated this formula. The certificates therefore exclude exactly the following many primitive \((n,d)\) pairs in their respective triangular height regimes:

| \(k\) | \(B\) (all \(M

|---:|---:|---:|

| 35 | 13,357,343 | 1,595,080,842,488 |

| 36 | 13,750,206 | 1,641,995,050,554 |

| 37 | 47,045,881 | 18,687,973,255,143 |

| 38 | 47,045,881 | 18,182,892,896,208 |

The pair counts are computational-only; the exclusion itself is (b) because it is an elementary proof conditional only on the three named exponent theorems.

3. Reproducible checker and run

The standalone checker is runs/erdos672_wave7f_reverify.py. It uses only the Python standard library. It:

• (a/d) generates the interval primes by trial division and recomputes every product and inequality;
• (d) exhausts the normalized residues modulo \(p^2\) to verify the one-or-two-multiple structure used in the lemma;
• (a/d) recomputes the primitive-pair counts by Möbius inversion and cross-checks the formula against literal enumeration on a small instance;
• (d) factors any supplied progression term-by-term from scratch and takes the gcd of all prime exponents to decide whether its product is a perfect power;
• (d) uses \(1,25,49\), whose product is \(35^2\), as a positive control.

Core certificate code:

from functools import reduce
from operator import mul

for p in interval_primes(k):
    assert bound <= p ** (q - 1)
    verify_residue_structure(k, p)

prime_product = reduce(mul, interval_primes(k), 1)
forced_height = 1 + (k - 1) * prime_product
assert forced_height >= bound

Commands actually run:

$ python3 runs/erdos672_wave7f_reverify.py
...
k=35 ... certified M >= 13357343 ... primitive_pairs_below=1595080842488
k=36 ... certified M >= 13750206 ... primitive_pairs_below=1641995050554
k=37 ... certified M >= 47045881 ... primitive_pairs_below=18687973255143
k=38 ... certified M >= 47045881 ... primitive_pairs_below=18182892896208
PASS: all independent arithmetic and structural checks succeeded.

$ python3 runs/erdos672_wave7f_reverify.py --box 100 100
Finite box: checked=24348 primitive triples, hits=0
PASS: all independent arithmetic and structural checks succeeded.

The finite box is merely a (d) sanity check; it is not used in the proof.

4. Exact remaining wall

(b) What remains at the first unresolved lengths is now explicit:

• \(k=35,36,37,38\);
• a prime exponent \(q\geq7\);
• largest term at least the corresponding bound in the table.

(a) The interval-prime lemma cannot automatically go farther. At or beyond \(M=p^{q-1}\), two terms divisible by \(p\) may contribute valuations \(1+(q-1)=q\), which is compatible with a \(q\)-th power. Even below that threshold, forcing the four primes \(19,23,29,31\) into \(d\) gives only \(d\geq392863\), which is compatible with \(M\geq13357343\); the divisibility argument has spent all of its contradiction.

(c) The missing lemma is therefore a way to exclude the surviving \(q=7\) valuation/kernel patterns (or to force additional independent primes into \(d\)). In the standard approach one writes

with the \(a_i\) supported on primes below \(k\), then must eliminate the resulting coupled ternary generalized-Fermat equations. Győry–Hajdu–Pintér report that their \(k=32,33,34\) cases already took about a week each after substantial Magma/Maple sieving; extending that system to \(k=35\) is the concrete missing computation/theorem, not a routine brute-force loop.

(c/d) For scale, between the new \(k=35\) bound and \(19^6\) there are exactly

primitive parameter pairs. Even an optimistic direct tester sustaining \(10^6\) fully factored progressions per second would require about \(5053.38\) core-hours (roughly \$200–\$500 at \$0.04–\$0.10/core-hour, before overhead). The supplied pure-Python checker is much slower than that optimistic rate. Such a scan was not run; a modular/ternary sieve is required.

(c) No counterexample, uniform proof, or effective enumeration of Bennett's finite set was obtained. The global problem remains open.

PARTIAL: Modulo verified square/cube/fifth-power theorems, any counterexample at the first unresolved lengths k=35..38 has prime exponent at least 7 and largest term at least 13,357,343; 13,750,206; 47,045,881; 47,045,881 respectively, with all arithmetic and exact excluded-pair counts independently checked.