The prime-sandwich property of OEIS A373698

Abstract

Let a(1) = 1, a(2) = 2, and a(3) = 3. Thereafter choose the least unused positive integer sharing an odd prime factor with the preceding term. I present a computer-assisted proof that every prime p > 3 appears in the consecutive block 3p, p, 2p, a property conjectured in the entry for OEIS A373698. The proof adapts the threshold-crossing method of Hofman and Pilipczuk for the EKG sequence. An explicit prime-counting bound excludes exceptions for p >= 200000; exact computation verifies all 17982 relevant smaller primes. A separate verifier checks the defining greedy rule throughout the computed prefix. The accompanying reproducibility files contain the LaTeX source, Lean 4 source and build documentation, JavaScript verification code, a finite certificate, and verification summaries. The Lean development constructs the canonical infinite sequence and proves the prime-sandwich and immediate-neighbor statements. It uses Lean v4.30.0-rc2 and mathlib revision 9977002c3c9492b622fb469b0d18acc7e73aed3e. The reported build completed without sorry placeholders. Formal verification trust boundary: each final Lean theorem depends on propext, Classical.choice, and Quot.sound, together with nine computation axioms generated by native_decide in the pinned toolchain. These finite computations therefore also trust Lean's compiler and runtime; they were not evaluated entirely within Lean's small kernel. No computation axiom is declared manually in the source. The project README and build report record the exact dependencies and reproduction instructions. AI tools assisted with proof development, Lean formalization, verification code, and manuscript preparation. The tool used was OpenAI Codex. The sequence and conjectured pattern are credited to Scott R. Shannon's OEIS entry. The crossing method is adapted from Hofman and Pilipczuk's work on the EKG sequence. This is a preprint for mathematical review. No claim of priority or external peer review is made.