For the primorial $P=p_1\cdots p_n$, is there always a prime $p_n<p<P$ with $P+p$ prime? (Erdős #779)

Let $n>1$ and let $p_1<\cdots<p_n$ denote the first $n$ primes. Let $P=\prod_{1\leq i\leq n}p_i$ (the $n$-th primorial). Does there always exist some prime $p$ with $p_n<p<P$ such that $P+p$ is prime? Note that the window is natural: if $P+m$ is prime for some $1<m<P$ then $m$ must be coprime to $P$, so every prime factor of $m$ exceeds $p_n$; primes in $(p_n,P)$ are the simplest candidates.

Acceptance. FULLY RESOLVES: a proof that for every $n>1$ there is a prime $p\in(p_n,P)$ with $P+p$ prime — machine-checkable (Lean/Coq; a formal statement already exists) preferred, else a complete written proof; results conditional on a stated hypothesis must be clearly flagged and do not fully resolve. OR a counterexample: an explicit $n$ together with a verifiable demonstration that $P+p$ is composite for every prime $p$ with $p_n<p<P$ — note this window contains on the order of $P/\log P$ primes with $P=n^{(1+o(1))n}$, so a brute-force certificate is only realistic with structural pruning, and all $n\leq 1000$ are already ruled out. ADVANCES: extend the verified range strictly beyond the $n\leq 1000$ record stated in the background, publishing the search code and, for each new $n$, the least prime $p$ found together with a primality certificate for $P+p$; or empirical + theoretical progress on Erdős's stronger prediction that the least such $p$ is at most $n^{O(1)}$ (e.g. a proof under a clearly stated standard conjecture). Deliver the proof file, or the search code plus a per-$n$ witness table with primality certificates and the attained range.