A single-track Gray code of length 
and period 
is a cyclic sequence of 
distinct binary words
of length 
such that consecutive words, including the last and first,
differ in exactly one bit and every column is a cyclic shift of one fixed column
(Dzoba 2026). It is therefore a Gray code with an additional
column-shift condition, not necessarily a listing of every binary word.
For odd prime 
, the largest possible period is at most 
. Dzoba (2026) constructed codes attaining this upper
bound for every odd prime 
. For 
, explicit codes were checked word by word. For 
, 43, and 47, the constructions use
a proved implication from the Degni-Drisko adjacency property, which was checked
computationally at those lengths. This property orders nonconstant necklaces
by their first occurrences in the binary reflected Gray
code and requires consecutive necklaces to have representatives at Hamming
distance 1. Existence for every odd prime follows conditionally
from that property and is not proved in general.
Dzoba (2026) reports that Claude performed the searches, found the closing pivots, and wrote the proofs and Lean formalization under the author's direction. Codex supplied additional verification programs.
