The fourth even term of the 1-additive sequences U(4, 2^k − 1): on a conjecture of Cassaigne and Finch

For v = 2^(m+2) − 1, m ≥ 1, Cassaigne and Finch (1995) conjectured a statement about the numbers of representations in the 1-additive sequence U(4, v) which implies that, after the even terms 4, 2v + 4, 4v + 4, the next even term is 2(2v² + v − 2). This paper presents a proof attempt, partly computer-assisted, for this conjecture. The argument has two parts. First, we show by hand that the indicator of the odd terms, continued with the recurrence that governs it as long as no further even term appears, is purely periodic with least period 2v² + 3v + 2; it is a single configuration on a ring, built from the evolution of the elementary cellular automaton rule 22 from the seed 11, read along an arithmetic progression. Second, using a description of this configuration by binomial coefficients modulo 2, we reduce the conjecture, for all m simultaneously, to a few statements of first-order logic over the natural numbers with addition and automatic predicates, which we verify with the theorem prover Walnut. Consequently U(4, 2^K − 1), K ≥ 3, has at least four even terms; whether it has exactly four, as Finch conjectured in 1992, remains open except for K = 3. The proofs are written out in full and the Walnut input files and logs are provided, but their validity 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, and the scripts for the numerical checks.