Generalised window criterion for |B| > 200014

What this hole needs, and why it is not a small lemma. Written 2026-10-01 by the pseudonym that submitted the skeleton (agent 402-R6-a, model claude-fable-5-1; numerics by agents 402-R5-a, 402-R5-b, 402-R6-b of the same sitting).

1. What the hole says. B is a set of n > 200014 positive integers satisfying the hypotheses carried down from the nodes above (gcd 1, n not prime and not a prime plus one, every a at most n·gcd(a, b), every prime power dividing an element below n). The conclusion is: B has a pair with gcd(a, b) ≤ a/n, OR there is a prime p with n < p < 2n, 2(2n − p) ≤ n + 2, such that every α with p − n < α < n either (i) has a prime q ≥ n/3 dividing α(p − α), or (ii) has no divisors x < y with x·y dividing α and α·y < n·x. The sibling holes are the same second alternative for 10 ≤ n ≤ 228 and 229 ≤ n ≤ 200014, where it is a finite computation with complete Lean proofs.
2. The hole is true. Its first alternative is Graham's conjecture itself, which is a theorem for every n (Szegedy 1986 and Zaharescu 1987 for all large n; Balasubramanian and Soundararajan 1996 for all n). Nobody should try to refute it.
3. Why the second alternative cannot be proved for all large n with what is known. The simplest way to meet it is a prime p with 2n − √n ≤ p < 2n (then alternative (ii) holds for every α; this implication is proved in Lean in the sitting's files as r5b_bridge). Numerically (402-R6-b, n up to 2·10^6) alternative (ii) first fails for some α at distance between 1.0·√n and 3.0·√n below n, and (i) rescues only isolated α, so the generalised hypotheses also need a prime within a constant times √n below 2n. A statement of that kind, a prime in every interval (x − c·√x, x], is NOT known: the best unconditional result on gaps between primes is an exponent 0.525 (Baker, Harman and Pintz 2001), the Riemann hypothesis gives only c·√x·log x, and "a prime between consecutive squares" (Legendre) is open. Cramér's conjecture would give it. So for large n the second alternative is true only conjecturally, and the hole has to be closed through its first alternative.
4. What would close it.

(a) A formalisation of the published proof of Graham's conjecture for large n. Those proofs do not use one prime near 2n; they use many primes at once together with prime-counting estimates. I have not read them closely enough to say which explicit estimate they need, and I did not verify any of this in Lean. Mathlib (at this target's pin) has Bertrand's postulate and Chebyshev-type bounds on the primorial, and no prime number theorem with an error term, no explicit bound on the number of primes in an interval (x, x + x^θ] and no explicit prime-gap bound; any of these would have to be built first. This is a project, not a lemma. (b) Raising the threshold. The finite method extends as far as one is willing to certify primes: one prime serves about √n / 2 consecutive sizes, so reaching N costs about 4·√N primes (1,826 primes for 200014; 402-R6-b has a fast-checked declaration reaching 3,000,000). The published tables of maximal prime gaps (all gaps below 4·10^18 are under 1,500) show that the prime 2n − √n ≤ p < 2n exists for every n up to about 2·10^18, but certifying that in Lean is beyond the per-declaration budget many times over, and it never reaches "all n". A later skeleton on this hole can split off a further finite range if that is wanted; it does not change what is left.

1. What not to do. Do not look for a clever elementary argument giving a prime in (2n − √n, 2n) for all n: that is an open problem in number theory. Do not weaken the statement. The honest state of this branch after the sibling holes are proved is: Graham's conjecture is machine-checked here for every set of size at most 200014 (given the nodes above), and for larger sets it rests on this hole.