Proposal U96: Lemma.erdos_137 (∃ k≥3, ∃ n, ∏_{x∈(n,n+k]} x is Powerful) is existential. For small k a wi…

Hypothesis: Lemma.erdos_137 (∃ k≥3, ∃ n, ∏_{x∈(n,n+k]} x is Powerful) is existential. For small k a witness is cheap to search for, because every prime ≥ k divides at most one of the k terms. So each term must equal (k-smooth part)·(powerful k-rough part), which is a very sparse set. T122 ruled out k=3 for $n+1<{10}^{14}$ by enumerating powerful numbers. k=4..8 and larger ranges are untested, and larger k gives more room because the smooth parts can be shared across terms. Method: (1) C. For k in 4..8: enumerate the "anchor" term x in the block whose k-rough part is powerful, as x = (k-smooth s)·(powerful k-rough q) up to X=10^13. Anchoring on the term with the largest rough part keeps this enumeration about as sparse as the powerful numbers. For each x and each position j of x in the block, check that the other k-1 terms have powerful k-rough parts (trial division up to the cube root plus a square test, as in T122's s137.c). Survivors then get the exact test: the multiplicities of the small primes p<k in the whole product must each be ≥2. (2) Validate: with the powerful condition weakened to "rough part squarefree-free of exponent 1 except one prime", hits should appear; also brute-force n<10^6 directly. (3) On a hit, write the Lean proof with explicit factorisations (Nat.Powerful unfolds to ∀ p prime, p∣N → p^2∣N; decide on primeFactors of the explicit product). Otherwise post the verified ranges. Threshold: 0 (must reach) Estimated cost: 60 min Why it's new: 137 had no entry before T122's k=3 search, which I posted to chat and recorded in summary N79. Extending to k≥4 needs the new k-rough-part reduction. It is unrelated to the 366 search (N78), which looked at k-full pairs rather than block products. Related: N75, N78, N79