Is $\mathrm{lcm}(1,\ldots,p_{k+1}-1) < p_k\cdot\mathrm{lcm}(1,\ldots,p_k)$ for every $k$? (Erdős #458)

Let $[1,\ldots,n]$ denote the least common multiple of $\{1,\ldots,n\}$, and let $p_k$ denote the $k$-th prime. Is it true that, for all $k\geq 1$, $$[1,\ldots,p_{k+1}-1]< p_k\,[1,\ldots,p_k]\,?$$ Since $\mathrm{lcm}(1,\ldots,n)$ increases exactly at prime powers, the ratio $[1,\ldots,p_{k+1}-1]/[1,\ldots,p_k]$ equals the product of $q$ over all prime powers $q^j$ (with $j\geq 2$, $q$ prime) lying in the interval $(p_k,\,p_{k+1}-1]$ — so the question is whether that product of new prime-power contributions in a prime gap can ever reach $p_k$. A single explicit $k$ violating the inequality would disprove it.

Acceptance. FULLY RESOLVES (disproof): an explicit $k$ with the consecutive primes $p_k,p_{k+1}$ (primality certificates for both, compositeness witnesses for everything between), the complete list of prime powers $q^j\in(p_k,p_{k+1}-1]$ with $j\geq 2$, and a verification that the product of their bases $q$ is $\geq p_k$ — this certifies $[1,\ldots,p_{k+1}-1]\geq p_k[1,\ldots,p_k]$ without computing the lcms, and is fully machine-checkable. FULLY RESOLVES (proof): a proof of the inequality for all $k\geq 1$; machine-checkable (Lean — a formal statement already exists in google-deepmind/formal-conjectures) preferred, else a complete written proof (note it must inherently control prime gaps at Legendre strength; a computation alone cannot close it). ADVANCES: (a) a certified exhaustive verification for all $k$ with $p_k\leq N$, for an $N$ stated by the submission and strictly beyond any previously published verification it can identify (the source page records none), delivered via the prime-power-in-gaps reduction with code and an exhaustiveness argument; or (b) a conditional proof under an explicitly stated prime-gap hypothesis (e.g. $p_{k+1}-p_k<p_k^{1/2}$), handling the small-prime-power obstruction unconditionally, clearly flagged as conditional. Deliver the counterexample certificate, or the verification code + attained bound, or the proof file.