The state complexity of Y=nX in Zeckendorf representation: exact values, the OEIS A372846 bound, and the reachable states of the Moradi–Rampersad–Shallit automaton

Abstract

Let a(n) be the number of states of the smallest deterministic finite automaton that reads two Zeckendorf representations in parallel and accepts exactly the pairs (x,y) with val(y)=nval(x), the dead state not counted; this is sequence A372846 of the OEIS. Moradi, Rampersad and Shallit build an automaton M_(n,c) with 36n² states for the relation Y=nX+c, print a(1),…,a(10) as computed by Walnut, write that the quantity "is roughly 2n²+α²n, but we do not know how to prove this", and close the remark with "A better understanding of the reachable states of M_(n,c) might help reduce the bound." The OEIS entry sharpens the guess to the conjecture a(n) ≤ 2n²+φ²n+1. We prove a(n) exactly for 1 ≤ n ≤ 16 and a(32)=2132 — to our knowledge the first proofs of any term — by an explicit automaton whose correctness is certified by integer arithmetic alone (two forward-closed half-planes in the plane of two consecutive differences replace the irrational estimate of the source) together with a Myhill–Nerode table for partial acceptors, in which liveness of the prefixes is an essential hypothesis. We show that the OEIS inequality, stated over the reals with sqrt5, is equivalent to an integer inequality, and prove it at the nineteen values n ∈ {1,…,16,32,49,50}; outside the formal development it is verified for every n ≤ 601, where the smallest slack is 0.652476 at n=14 — not at n=32, as the 48 published terms suggest — exactly two n have slack below 1, both proved here one state from the edge, and beyond n ≈ 40 the slack grows like 0.10 n. We answer the closing sentence: the part of M_(n,c) reachable from the initial state has exactly 6n²+6n-4 states for every c, certified for n ≤ 100 and computed to n=601, a factor 6 below the printed count. Past the 48 terms of the OEIS entry we certify a(49) ≤ 4926 and a(50) ≤ 5128, and two independent implementations agree on a(49),…,a(60) and continue to a(601)=723916. All theorems are machine-checked in Lean 4.

Open review

This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.

Archived files

1. Version 1 · current (opens in a new tab)

   Source snapshot 2026-09-07 03:53 UTC

   File fingerprint

   cfd8e57137222f428fa15730a7b20ea0d30be552076704ba7a24561379e3761d