HEXAGONbeta

On a counting conjecture for binary rich words

Primarily AI-generated textHuman understanding: no partsmath.CO — Combinatorics

Contributed by Max Glass

Version 2 / Nov 06, 2026 / CC BY 4.0

Abstract

Let R2(n)R_2(n) denote the number of binary rich words of length nn. We prove that lim sup⁡n→∞log⁡R2(n)nlog⁡n=∞\limsup_{n\to\infty}\frac{\log R_2(n)}{\sqrt{n}\log n}=\infty. Consequently, R2(n)R_2(n) is not O(nCn)O(n^{C\sqrt{n}}) for any fixed C>0C>0, disproving the conjectured upper bound O((n/g(n))n)O((n/g(n))^{\sqrt{n}}) with g(n)→∞g(n)\to\infty. The proof combines independent permutation families through an ordered concatenation construction and a binary gap encoding.

Author comments: Formatting correction to the web abstract: repaired math delimiters and removed hard line breaks. The paper and mathematical results are unchanged. 4 pages. Lean 4 formalization and paper source: https://github.com/glasss13/rich-word-counting.

Provenance statement

GPT-6 Astra (OpenAI) was used for the main proof construction and drafting of this paper. Max Glass directed the project. The submitting contributor reports that none of the contribution has been personally checked and understood by him. The main theorem has an end-to-end Lean 4 formalization using Mathlib; the included 291 theorem declarations were audited with transitive axioms restricted to propext, Classical.choice, and Quot.sound. This is machine verification of the formal statements, not human review of the paper. Paper source and formalization: https://github.com/glasss13/rich-word-counting.

References

  1. A. Glen, J. Justin, S. Widmer, and L. Q. Zamboni, Palindromic richness, European Journal of Combinatorics 30 (2) (2009), 510--531. doi:10.1016/j.ejc.2008.04.006 (https://doi.org/10.1016/j.ejc.2008.04.006).DOI
  2. C. Guo, J. Shallit, and A. M. Shur, On the combinatorics of palindromes and antipalindromes, arXiv preprint arXiv:1503.09112v1 (https://arxiv.org/abs/1503.09112v1) (2015).arXiv
  3. C. Guo, J. Shallit, and A. M. Shur, Palindromic rich words and run-length encodings, Information Processing Letters 116 (12) (2016), 735--738. doi:10.1016/j.ipl.2016.07.001 (https://doi.org/10.1016/j.ipl.2016.07.001).DOI
  4. J. Rukavicka, Subexponential upper bound on the number of rich words, arXiv preprint arXiv:2511.11069v3 (https://arxiv.org/abs/2511.11069v3) (2026).arXiv

Version history

  1. v1 · 4 pagesSubmitted by Max Glass4 pages. Lean 4 formalization and paper source: https://github.com/glasss13/rich-word-counting.SupersededNov 06, 2026
  2. v2 · 4 pagesSubmitted by Max GlassFormatting correction to the web abstract: repaired math delimiters and removed hard line breaks. The paper and mathematical results are unchanged. 4 pages. Lean 4 formalization and paper source: https://github.com/glasss13/rich-word-counting.CurrentNov 06, 2026