Restricted Mertens sum over primes with $n\bmod p\in(p/2,p)$: is it $\sim\tfrac12\log\log n$? (Erdős #726)

For a positive integer $n$ and prime $p$, say that $n\in(p/2,p)\pmod p$ if $n\equiv r\pmod p$ for some integer $r$ with $p/2<r<p$ (equivalently, the least nonnegative residue of $n$ modulo $p$ exceeds $p/2$). Erdős, Graham, Ruzsa and Straus conjectured that, as $n\to\infty$, $$\sum_{\substack{p\le n\\ n\in(p/2,p)\!\!\pmod p}}\frac1p\;\sim\;\frac{\log\log n}{2}.$$ That is, restricting Mertens' sum $\sum_{p\le n}1/p\sim\log\log n$ to the primes whose residue class of $n$ lands in the upper half $(p/2,p)$ captures asymptotically exactly half of its total mass.

Acceptance. FULLY RESOLVES: a complete proof (Lean/Coq machine-checkable preferred, else a full written proof) that the restricted sum satisfies $\sum_{p\le n,\,n\bmod p>p/2}\tfrac1p=\tfrac12\log\log n+o(\log\log n)$, or a proof that it does not (a different limiting constant, or no limiting ratio). ADVANCES: a proof that the asymptotic $\tfrac12\log\log n$ holds for a density-one set of $n$; a proven separation pinning $\liminf$ and $\limsup$ of $\big(\sum_{p\le n,\,n\bmod p>p/2}\tfrac1p\big)/\log\log n$ strictly inside $(0,1)$, improving on anything in the background; or a reproducible numerical study over a certified range of $n$ with the evaluation code and a fitted constant reported with an uncertainty. Deliver the proof, the improved proven bound, or the numerical evidence with code and a fitted constant plus error bars.