One recurrence behind two families of 1-additive sequences: crystals for all even terms, and the next even term

For a 1-additive sequence with one even initial term e and one odd initial term o, Finch predicted the even terms e + 2po, 0 ≤ p ≤ e/2, both for U(e, o) with e < o and for U(o, e) with o < e (for e ≥ 6, respectively o ≥ 7), and Kuca proved that these numbers are terms in all cases. As long as these are the even terms, the odd part of both sequences is one and the same sequence: a single 1 followed by a recurrence of "exactly one" type with the shifts e/2 + po. We give a proof attempt that this sequence is purely periodic from the start, for all even e ≥ 4 prime to o at once, in two infinite families of o: for o ≡ 1 (mod 4), with least period (e/2)·2^t·(o + 1), where 2^t is the least power of 2 above o, and an explicit closed form of Pascal-triangle type; and for o = 2^k − 1, with least period (e/2)(o + 1)^2 − o, given by an "exactly one of e/2 + 1" cellular automaton read along an arithmetic progression on a ring, with (e/2 + 2)·3^(k−1) − 1 ones per period. The first proof reduces the recurrence to five statements that do not involve e and are verified by the automatic prover Walnut; the second is by hand. For o ≡ 1 (mod 4) and e ≥ 6 we also show, by a hand count of representations in lattice coordinates, that the crystal produces exactly the next even term (2e + 4)o predicted by Finch, with no other even term before it, and that the odd part leaves the crystal at the odd number (2e + 5)o. For the odd part, these results contain earlier ones for e = 4 (Cassaigne and Finch; the author) and for fixed small o, each of which fixes one of the two parameters. The validity of the proofs is left open to external verification; see the note at the end of the paper. The accompanying archive contains the Walnut command files and logs (with a second run on a separately built copy of Walnut and a program that checks the command files against the definitions), the programs for the numerical checks with their outputs, earlier Walnut verifications for single e, and the programs for the scans of initial pairs.