The lag-two EKG sequence A121217 is a permutation, and its primes appear in increasing order

Let a(1), a(2), a(3) = 1, 2, 3, and for n >= 4 let a(n) be the least positive integer that has not yet appeared and is not coprime to a(n-2). This is sequence A121217 of the OEIS. We prove that it is a permutation of the positive integers and that its primes appear in increasing order, which settles two conjectures recorded in the OEIS by R. Zumkeller in 2015 (A121217, A256414). Every prime p >= 5 appears inside a block of five consecutive terms 2p, X, p, Y, 3p, where p divides neither X nor Y, and a(n) = n + O(n/log n) for all n outside the sparse sets where a(n) is a prime or three times a prime, so that liminf a(n)/n = 1/2 and limsup a(n)/n = 3/2. The proofs are elementary and adapt the methods of Lagarias, Rains and Sloane and of Hofman and Pilipczuk for the EKG sequence. A short program checks all statements on the first 10^6 terms. Manuscript; not submitted to a journal. The results were developed with an AI system (Anthropic Claude) and checked by independent AI referee agents; no human peer review has taken place.