PROVED (LEAN), on the site's label, which credits Cédric Pilatte's observation that the answer follows from Shiu's theorem on runs of consecutive primes in one residue class [Sh00], and records Lean proofs of the statement outside this corpus; the deduction, the credit and the Lean developments are on the claim page (Pilatte, 2024). None of the Lean proofs is built here.