Do normalized prime gaps have a continuous limiting distribution function? (Erdős #234)

Let $p_n$ denote the $n$th prime. For a real constant $c\ge 0$, let $f(c)$ be the natural density of the set of integers $n$ for which $$\frac{p_{n+1}-p_n}{\log n}<c.$$ The problem asserts (and asks one to prove) that for every $c\ge 0$ this density $f(c)$ exists, and that $f$ is a continuous function of $c$. In other words, the normalized prime gaps $(p_{n+1}-p_n)/\log n$ possess a continuous limiting distribution function.

Acceptance. FULLY RESOLVES: a complete proof that the density $f(c)$ exists for every $c\ge 0$ and defines a continuous function of $c$ — machine-checkable (Lean/Coq) preferred, otherwise a full written proof; OR a disproof (e.g. a proof that the density fails to exist for some $c$, or that any limiting distribution is discontinuous). ADVANCES (each a complete proof; a proof may be conditional on an explicitly stated hypothesis such as Hardy–Littlewood, clearly flagged): establish existence of the limiting density $f(c)$ for $c$ in some nonempty range; or determine $f$ exactly (e.g. prove $f(c)=1-e^{-c}$) under a stated hypothesis; or prove one-sided bounds on the relevant $\liminf$ and $\limsup$ counting densities that pin $f$ between two explicit continuous functions. Deliver a machine-checkable or complete written proof.