A proof of a conjecture of H. Gruber: finite unary languages by the alphabetic width of their regular expressions

We prove a statement recorded by H. Gruber in 2012 in the OEIS entry A000079 (the powers of 2), verified by him up to n = 17: for n >= 1, the number of distinct finite languages over a one-letter alphabet whose minimum regular expression has alphabetic width n is 2^n. The alphabetic width of a regular expression is the number of occurrences of alphabet symbols in it, one of the standard measures of the size of an expression. The proof shows that, for a nonempty finite unary language, the minimum alphabetic width of a regular expression for it is exactly the length of its longest word. The lower bound (no expression for a finite language has fewer letters than the length of its longest word) is a proposition of Ellul, Krawetz, Shallit and Wang (2005), valid over any alphabet, and is proved again in the note by a short structural induction. The upper bound is given by a nested expression in the manner of Horner's rule, a^{s_1}(e + a^{s_2 - s_1}(e + ... (e + a^{s_k - s_{k-1}}) ... )), where s_1 < ... < s_k are the lengths of the words and e is the empty word: it denotes the language and uses exactly s_k letters. Hence the finite unary languages of minimum width n are those whose longest word is a^n, and there are 2^n of them, one for each subset of {0, ..., n-1}; for n = 0 there are two (the empty language and {e}), which is why the statement starts at n = 1. A remark shows that the unary alphabet is essential: over two letters the language {ab, ba} has longest word of length 2 but no expression of width 2. The proof is elementary and its two halves were, separately, known or standard; the contribution of the note is to put them together and to record the count. As of October 6, 2026 the statement was still marked as conjectural ("apparently") in the entry. The note also explains the methodology of the author's project on open statements in the OEIS (translation of the statements into formulas for the reasoning engine SyntheticMind, with time budgets by type of computation; a log of obstacles that decides which methods to implement next; recursive splitting into subgoals; independent verification; a review by a second AI system) and the steps that led to this proof. The use of AI is described in the paper. Files: Blanco_Gomez_2026_Gruber_unary_width_EN.pdf is the paper; Blanco_Gomez_2026_Gruber_unary_width_ES.pdf is the Spanish version (same content); verify_gruber.py is the independent verification script (Python, no external libraries; it enumerates the languages of all star-free expressions by width for width up to 14 and finds exactly 2^n languages of minimum width n, tests the lower bound on 200000 random expressions with stars, and checks the nested expressions through an independent parser; it runs in a few seconds and prints ALL CHECKS PASSED).