Proofs of some OEIS conjectures on Wythoff sums, Fibonacci and Lucas words

We prove several conjectures from the On-Line Encyclopedia of Integer Sequences about the lower and upper Wythoff sequences and the Fibonacci word. Among them are two of Kimberling's three conjectures on the number of ways to write n = ⌊hφ⌋ + ⌊kφ²⌋ with h, k ≥ 1 (A259598): exactly one way if and only if n + 1 = 2F for a Fibonacci number F ≥ 2, and exactly two ways if and only if n + 1 ≥ 7 is a Lucas number. The third conjecture, that no way exists if and only if n + 1 is a Fibonacci number, was proved earlier by Kawsumarng et al. We also observe that Kimberling's conjecture on the gaps of the sums of two distinct terms of A003622 and of their complement (A333308, A333309) follows, after a shift by 2, from earlier Walnut results of Shallit and of Bosma et al. on A260317, and we re-verify it. Next, we prove Kimberling's five 2025 conjectures on the gaps between positions where the Fibonacci word and the "Lucas word" take prescribed values (A383423–A383427). Finally, we prove a conjecture of Mathar on A285383, and we point out that a conjecture of Schmidt on A003250 follows from theorems of Carlitz, Scoville and Vaughan (1973); we also confirm it with Walnut. Most proofs are decision procedures run in the free prover Walnut, and we supply the complete command file.