Newman-Conway and its cousin

The Hofstadter–Conway sequence c(n) = c(c(n-1)) + c(n-c(n-1)) (OEIS A004001) and Alkan’s companion s(n) = n - s(s(n-1)) - s(n-s(n-1)) (OEIS A287422) both start 1, 1, and on each dyadic block [2^k, 2^(k+1)] both c(n) - n/2 and s(n) - n/2 trace an arch; the arches of c are positive, those of s alternate in sign. Alkan conjectured on MathOverflow (question 366772), after checking every n ≤ 2^32, that the arches of s never rise above those of c:

|s(n) - n/2| ≤ c(n) - n/2   for every n ≥ 1.

The paper proves this. On each block both sequences are encoded by Dyck words, and the words for the next block come from the previous ones by two explicit threshold operators, F for c and F or G (alternating with k) for s. Plain induction fails, because G can overtake F in one step; the proof instead carries a stronger hypothesis through two steps at once, using a domination lemma for Dyck words that are symmetric under reversal and complement. As by-products, s is slow (its increments are 0 or 1), s(2^k) = 2^(k-1), and the sign of s(n) - n/2 on each block is (-1)^k.

Preprint v1, 8 October 2026, not peer reviewed. Every result of the paper is formally verified in Lean 4 (lean/, standard axioms only). The exposition has not yet been independently reviewed. The author used AI tools (Claude, Anthropic; Codex, OpenAI) in this work, as described in the paper’s acknowledgement, and is responsible for its content.