Do most integers n have a large prime factor within a bounded window n,...,n+k? (Erdős #1201)

For a positive integer $m$ let $P(m)$ denote its greatest prime divisor. Is it true that for every $\epsilon,\eta>0$ there exists a $k$ (depending only on $\epsilon,\eta$) such that the set of integers $n$ for which $$P\big(n(n+1)\cdots(n+k)\big)>n^{1-\epsilon}$$ has lower density at least $1-\eta$? Informally: by taking a long enough consecutive window $n,n+1,\ldots,n+k$, can one force almost all $n$ to have a prime factor nearly as large as $n$ somewhere in the window?

Acceptance. FULLY RESOLVES: a complete proof (Lean/Coq preferred, else a full written proof) that for every $\epsilon,\eta>0$ a valid $k=k(\epsilon,\eta)$ exists, with an explicit or effective bound on $k$ — OR a disproof exhibiting $\epsilon,\eta>0$ for which no finite $k$ achieves density $\geq 1-\eta$, with proof. ADVANCES: a proof of the statement for a specific exponent strictly beyond Erdős's $\epsilon=1/2$ stated in background — i.e. establishing, with proof, that some fixed $\epsilon<1/2$ works for all $\eta>0$ (equivalently forcing $P>n^{1-\epsilon}$ with $1-\epsilon>1/2$), or a reduction of the full conjecture to a stated standard hypothesis; a reproducible large-scale density computation (factoring windows up to a record $X$ across a range of $k$) is admissible only as flagged numerical evidence, never as a resolution. Anchor any bound-improvement claim to the $\epsilon=1/2$ result stated in background. Deliver the proof, or the improved exponent with proof, or the density-computation code plus tables as evidence.