This submission formalizes Jitsuro Nagura's 1952 theorem that every natural number $x \ge 25$ has a prime $r$ with $x < r < 6x/5$. It then applies that theorem to classify the "interesting numbers" from mathlib4 issue #6091, item 91: the only natural numbers satisfying the stated neighboring-prime factorization condition are $14$ and $21$.

The analytic argument is combined with explicit, kernel-checked prime chains below $5{,}000{,}000$. The complete proof was produced with substantial language-model assistance. OpenAI Codex performed the decisive proof development and integration; Leanstral was used in earlier exploratory and module-level attempts; Anthropic Claude independently audited the resulting source and verification evidence. The publisher does not claim personal authorship or independent expert understanding of the proof.