Kimberling's linear complementary equations: automatic structure and exact bounds

In 2018 Kimberling added to the On-Line Encyclopedia of Integer Sequences the solutions of complementary equations such as a(n) = 2b(n−1) − b(n−2) + 2n, where a(0) = 1, a(1) = 2, b(0) = 3, b(1) = 4, and b is the increasing sequence of positive integers not in a. For 21 of these sequences he conjectured bounds of the form L < x(n) − ρn < U for n ≥ 1, where ρ is the growth constant of x. The 11 equations behind these conjectures have the form a(n) = 2b(n−s) − b(n−s−1) + kn + c with s ∈ {0,1} and k ∈ {2,3,4}. For each of them we show that a(n) − (k+1)n and b(n) − n are sums of an explicit shift function and an automatic sequence in the Ostrowski numeration system of [0; k, k, k, …], and we verify this with the Walnut prover. From this we compute the exact infimum and supremum of x(n) − ρn for all 22 sequences; they lie in Q(√(k²+4)). Twenty of the 21 conjectures are true, three of them after a misprint is corrected. The conjecture for A297836 is false: it fails at n = 2 and for infinitely many n. We also prove a conjecture of Kimberling and Moses (2019) on three sequences defined by a mex rule, by showing that the first of them is ⌊(1+√2)n + 1 + √2/2⌋.Version 2: the supplementary checker now exits with a nonzero status when any check fails, decides every sign exactly (an undecidable sign is an error), and compares each verdict and the least counterexample of A297836 with the new fields verdict and first_counterexample added to certificates.json (no certificate value changed); it also checks the display fields and that no record or conjecture is missing. A test script with deliberately corrupted certificates is added. The paper is unchanged.