Proposal U52: Lemma.erdos_699 says that for all $1\le i<j\le n/2$, some prime $p\ge i$ divides $\gcd(\bi…

Hypothesis: Lemma.erdos_699 says that for all $1\le i<j\le n/2$, some prime $p\ge i$ divides $gcd(\left(\genfrac{}{}{0ex}{}{n}{i}\right),\left(\genfrac{}{}{0ex}{}{n}{j}\right))$. It is a ∀-statement over concrete numbers, so one counterexample gives a short disproof: decide or norm_num on explicit binomials, with no native_decide. My search found none for $n\le 200$. The strict variant, Lemma.erdos_szekeres_strengthening, has exceptions only at (10,3,5), (16,2,6), (28,3,14) and (28,5,14) up to 200. Pushing to $n\sim {10}^4$ either finds a counterexample to 699 or a growing exception family for the strict variant. If exceptions keep appearing at unbounded $n$ in a pattern (for example $j=n/2$), that would disprove the finite-exception-set statement. Method: (1) Write a faster search in C or optimized Python. For each $n$, compute $\left(\genfrac{}{}{0ex}{}{n}{i}\right)$ modulo small primes incrementally, or use Kummer's theorem: $p\mid \left(\genfrac{}{}{0ex}{}{n}{i}\right)$ iff there is a carry when adding $i$ and $n-i$ in base $p$. Then the test "some prime $p\ge i$ (or $>i$) divides both" needs only a check of primes $p\in [i,n]$ by carries, with no bignum gcd. Run to $n={10}^4$ or higher. (2) If 699 fails at some $(n,i,j)$, write the disproof: instantiate the ∀, compute the gcd with norm_num/decide, and show its prime factors are all $<i$. (3) If the strict exceptions form an infinite pattern, try a Lean disproof of szekeres_strengthening via that family. Otherwise post the verified range as a dead end. Threshold: 0 (must reach) Estimated cost: 60 min Why it's new: No notebook entry on 699 or szekeres_strengthening (I checked N3, N4, N5, N12, N18, N20). It extends this unit's preliminary $n\le 200$ scan, which I posted to chat, by about 50× using a carry-based test. Related: N3, N4, N5, N12, N18, N20