Restricted prime-factor counts over consecutive integers: a liminf bound and a limsup law (Erdős #890)

For an integer $n$ and a threshold $k\geq 1$, let $\omega_k(n)$ denote the number of distinct prime factors of $n$ that are $>k$, and let $\omega(n)$ denote the number of distinct prime factors of $n$ with no restriction. Two questions of Erdős and Selfridge. (1) Is it true that for every $k\geq 1$, $$\liminf_{n\to\infty}\sum_{0\leq i<k}\omega_k(n+i)\leq k?$$ (2) Is it true that $$\limsup_{n\to\infty}\left(\sum_{0\leq i<k}\omega(n+i)\right)\frac{\log\log n}{\log n}=1?$$

Acceptance. FULLY RESOLVES: a complete proof (machine-checkable in Lean/Coq preferred, else a full written proof) settling both claims — that $\liminf_{n\to\infty}\sum_{0\leq i<k}\omega_k(n+i)\leq k$ for every $k\geq 1$, and that the stated limsup equals $1$. A proof of either claim in isolation is acceptable if clearly delimited. ADVANCES: prove the liminf bound for a specified infinite family of $k$, or for a new individual $k$ beyond the trivial cases, or improve the classical $\geq k-1$ lower bound to a strictly stronger statement; establish rigorous one-sided bounds on the limsup expression sharper than those implied by the classical maximal-order fact stated in background; or provide a reproducible computation over a stated range certifying the observed liminf/limsup behaviour, delivered with the exact search program and the attained record range. Deliver the proof (or machine-checkable formalisation) and/or the search code plus the attained range and the observed extremal values.