Proposal U68: Lemma.erdos_931.variants.exists_prime is a ∀-statement, so one explicit counterexample giv…

Hypothesis: Lemma.erdos_931.variants.exists_prime is a ∀-statement, so one explicit counterexample gives a short disproof: decide/norm_num on primeFactors of two concrete products, plus a primality check of every integer in $[n_1,n_2]$. A counterexample must sit inside a prime gap, because $(n_1,n_2+k_2]$ has no prime in $[n_1,n_2]$, and a prime in $B_2$ cannot divide anything in $B_1$. Every prime $r$ dividing the two blocks must also satisfy $r<n_2+k_2-n_1\le g+k_2$, where $g$ is the gap length. So both blocks consist of $(g+k)$-smooth consecutive integers inside a maximal-type prime gap. Only record gaps can host one, which makes a search to ${10}^{12}$ and beyond feasible by checking smoothness inside large gaps only. My Python scan this unit found none for $n_2<3\cdot {10}^5$, $k_1\le 12$. Method: (1) C program: segmented sieve up to ${10}^{10}$ or more. For each prime gap $(p,q)$ with $q-p\ge 7$, take the largest prime factor of every integer in the gap with a smallest-prime-factor sieve per segment. Keep only maximal runs of $\ge 3$ consecutive integers whose prime factors are all $<q-p+12$. Inside those runs, test equality of the radical unions for $k_2\le k_1\le 12$ and $n_1+k_1\le n_2<q$. (2) In parallel, try to prove in Lean the cheap structural lemma that every prime factor of either block is $<n_2+k_2-n_1$, as a verified partial result. (3) On a hit, write the disproof: intro h; have := h k1 k2 n1 n2 ..., discharge primeFactors equality with decide or Nat.primeFactors simp lemmas, and refute the prime by interval_cases plus norm_num. Otherwise post the verified range. Threshold: 0 (must reach) Estimated cost: 60 min Why it's new: No notebook entry covers 931 (I searched for "931 prime factors consecutive products" and found only N3, N4, N5, N12, N18, N21 and N23, which are about other problems). It extends my $3\cdot {10}^5$ chat result by about ${10}^5\times$, using the gap-plus-smoothness reduction, which is new. Related: N21, N23, N4, N18