HEXAGONbeta

Pattern-avoiding binary arrays and a Stirling-type table: explicit formulas, exact recurrence orders, and non-D-finiteness

Primarily AI-generated textHuman understanding: some partsmath.CO — Combinatoricscs.SC — Symbolic Computation

Contributed by Yunkun Song ↗

Version 1 / Oct 16, 2026 / CC BY 4.0

Abstract

Let ak(n)a_k(n) be the number of n×kn\times k binary arrays in which no row contains 001001 or 010010 and no column contains 001001 or 011011 as three consecutive entries (OEIS A207123). Splitting the rows by parity gives ak(n)=Uk(⌈n/2⌉) Uk(⌊n/2⌋)a_k(n)=U_k(\lceil n/2\rceil)\,U_k(\lfloor n/2\rfloor), where Uk(m)U_k(m) counts sequences in {0,…,m}k\{0,\dots,m\}^k in which every three consecutive entries (a,b,c)(a,b,c) satisfy b=cb=c or a≥max⁡(b,c)a\ge\max(b,c); equivalently, Uk(m)U_k(m) counts the multichains of length mm in a subposet Λk\Lambda_k of the Boolean lattice. We prove three main results. First, for each mm the minimal order of a linear recurrence in kk is exactly 3m+13m+1, and a unique factorization into blocks gives a positive double-sum formula for Uk(m)U_k(m) in terms of Stirling and rr-Stirling numbers. Second, the bivariate generating function is not D-finite, and every polynomial-coefficient recurrence that holds on a quadrant is a left multiple of the defining four-term recurrence; the same holds for an associated Stirling-type triangle N(k,q)N(k,q), and UU is not Stirling-like in the sense of Kauers. Third, the numerators hk(t)h_k(t) of ∑mUk(m)tm=hk(t)/(1−t)k+1\sum_mU_k(m)t^m=h_k(t)/(1-t)^{k+1}, analogues of the Eulerian polynomials, have only simple real zeros; equivalently, the chain polynomials of the posets Λk\Lambda_k are real-rooted, and the rows of NN are log-concave. We also determine all binomial shapes with nonnegative parameters in which Uk(m)U_k(m) is a single sum, and show that the near-diagonal entries N(k,k−d)N(k,k-d) are polynomials in kk starting exactly at k=2d+2k=2d+2. The reduction, the exact orders, the explicit formula, the non-D-finiteness, the description of the quadrant recurrences and the near-diagonal theorem are formalized in Lean 4 with Mathlib.

Provenance statement

This work was produced with substantial use of generative AI. The author posed the problem (OEIS A207123) and directed the work. The large language models Claude Opus 5.5 and Claude Sonnet 5.5 (Anthropic), used through the Claude Code tool in October 2026, explored the problem, wrote the proofs, the verification programs and the Lean formalization, and drafted the manuscript. For most proofs, the author supplied the mathematical ideas and proof strategies, the models developed these into detailed arguments and proof drafts, and the author reviewed the resulting proofs. The proofs, the transcription of the Lean definitions and the manuscript were also reviewed by further runs of these models and by GPT-6.1 Sol (OpenAI), used through the Codex tool, and the manuscript was revised in response to these reviews; these AI reviews do not replace refereeing by human experts. The author has personally checked and understood the proofs in Sections 2, 5, 6 and 7; for the computer-assisted certificate of Proposition 6.10, this means checking what the script verifies, not each computed case. For the remaining proofs (Sections 3, 4 and 8 and Appendix B), the author relies on the Lean formalization where it exists, on the computer checks and on the AI reviews described here. The author compared the basic Lean definitions with the statements in the paper (Appendix A). The further definitions used by some entries of Tables 5 and 6, and the agreement of the Lean definitions of three OEIS entries with the OEIS, have so far been checked only by AI (Section 9). Machine verification. The results listed in Section 9 (Tables 5 and 6) are formalized in Lean 4 (v4.34.1) with Mathlib, starting from the definitions of a_k(n) and U_k(m). The development consists of 80 files, and its 6235 declarations use only the axioms propext, Classical.choice and Quot.sound. Lean checks the proofs, not the faithfulness of the formal statements to the statements in the paper. Not formalized: the explicit bijection of Proposition 4.7, the construction of the Ore algebra O(k,m), the step in Remark 5.8 from Kauers' definition, Section 6.2 (including the computer-assisted certificate of Proposition 6.10, which is checked by a script), and the last two sentences of Remark 6.4. Separately written Python 3.14 programs perform 414 automated checks, mostly in exact arithmetic (the high-precision numerical checks are labelled), and a script recomputes every number printed in the paper from the definitions, apart from the computations quoted in Section 10, which have their own scripts. Scripts, Lean development, verification logs and notes: https://github.com/r5x8ksva-del/a207123-explicit-formulas (commit e71d0f18b4faabf4bebb34c3eb0993744dc43681 corresponds to this version).

Tools used

Anthropic
Claude OpusVersion 5.5
Anthropic
Claude SonnetVersion 5.5
Anthropic
Claude Code
OpenAI
CodexVersion GPT-6.1 Sol
Lean
LeanVersion v4.34.1 (with Mathlib)
Python Software Foundation
PythonVersion 3.14

References

  1. C. A. Athanasiadis, T. Douvropoulos, K. Kalampogia-Evangelinou, Two classes of posets with real-rooted chain polynomials, Electron. J. Combin. 31 (4) (2024), #P4.16, https://doi.org/10.37236/12218.DOI
  2. C. A. Athanasiadis, K. Kalampogia-Evangelinou, Chain enumeration, partition lattices and polynomials with only real roots, Combin. Theory 3 (1) (2023), https://doi.org/10.5070/C63160425.DOI
  3. P. Brändén, Unimodality, log-concavity, real-rootedness and beyond, in: Handbook of Enumerative Combinatorics (M. Bóna, ed.), Chapman and Hall/CRC, Boca Raton, FL, 2015, pp. 461--508, https://doi.org/10.1201/b18255-13; arXiv:1410.6601.arXivDOI
  4. P. Brändén, L. Saud Maia Leite, Totally nonnegative matrices, chain enumeration and zeros of polynomials, Adv. Math. 487 (2026), Paper No. 110760, https://doi.org/10.1016/j.aim.2025.110760; arXiv:2412.06595.arXivDOI
  5. A. Z. Broder, The rr-Stirling numbers, Discrete Math. 49 (1984), no. 3, 241--259, https://doi.org/10.1016/0012-365X(84)90161-4.DOI
  6. F. Chyzak, M. Kauers, B. Salvy, A non-holonomic systems approach to special function identities, in: Proceedings of the 2009 International Symposium on Symbolic and Algebraic Computation (ISSAC 2009) , ACM, 2009, pp. 111--118, https://doi.org/10.1145/1576702.1576720; arXiv:0904.2761.arXivDOI
  7. R. Dougherty-Bliss, M. Kauers, Hardinian arrays, Electron. J. Combin. 31 (2) (2024), #P2.9, https://doi.org/10.37236/12358.DOI
  8. R. Dougherty-Bliss, C. Koutschan, N. Ter-Saakov, D. Zeilberger, The (symbolic and numeric) computational challenges of counting 0-1 balanced matrices, preprint, arXiv:2410.07435v2, 2025.arXiv
  9. R. Dougherty-Bliss, G. Spahn, Rectangular Hardinian arrays, ACM Commun. Comput. Algebra 58 (2024), no. 3, 81--84, https://doi.org/10.1145/3717582.3717589.DOI
  10. S. Fisk, Polynomials, roots, and interlacing, preprint, arXiv:math/0612833, 2006.arXiv
Show all 31 referencesShow fewer references
  1. I. Gessel, R. P. Stanley, Stirling polynomials, J. Combin. Theory Ser. A 24 (1978), 24--33, https://doi.org/10.1016/0097-3165(78)90042-0.DOI
  2. L. H. Harper, Stirling behavior is asymptotically normal, Ann. Math. Statist. 38 (1967), 410--414, https://doi.org/10.1214/aoms/1177698956.DOI
  3. M. Kauers, Summation algorithms for Stirling number identities, J. Symbolic Comput. 42 (2007), no. 10, 948--970, https://doi.org/10.1016/j.jsc.2007.08.002.DOI
  4. M. Kauers, D-Finite Functions , Algorithms and Computation in Mathematics 30, Springer, Cham, 2023, https://doi.org/10.1007/978-3-031-34652-1.DOI
  5. S. Kitaev, Patterns in Permutations and Words , Monographs in Theoretical Computer Science, Springer, Heidelberg, 2011, https://doi.org/10.1007/978-3-642-17333-2.DOI
  6. S. Kitaev, T. Mansour, A. Vella, Pattern avoidance in matrices, J. Integer Seq. 8 (2005), Article 05.2.2.
  7. M. Klazar, Bell numbers, their relatives, and algebraic differential equations, J. Combin. Theory Ser. A 102 (2003), 63--87, https://doi.org/10.1016/S0097-3165(03)00014-1.DOI
  8. C. Krause, Proof of formula, attachment to OEIS A202093, 26 June 2026, https://oeis.org/A202093/a202093.txt, accessed 7 October 2026.link
  9. L. de Moura, S. Ullrich, The Lean 4 theorem prover and programming language, in: Automated Deduction -- CADE 28 , Lecture Notes in Comput. Sci. 12699, Springer, 2021, pp. 625--635, https://doi.org/10.1007/978-3-030-79876-5_37.DOI
  10. L. Lipshitz, D-finite power series, J. Algebra 122 (1989), 353--373, https://doi.org/10.1016/0021-8693(89)90222-6.DOI
  11. A. Mahboubi, T. Sibut-Pinote, A formal proof of the irrationality of ζ(3)\zeta(3), Log. Methods Comput. Sci. 17 (2021), no. 1, Paper No. 16, https://doi.org/10.23638/LMCS-17(1:16)2021.DOI
  12. The mathlib Community, The Lean mathematical library, in: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020) , ACM, 2020, pp. 367--381, https://doi.org/10.1145/3372885.3373824.DOI
  13. OEIS Foundation Inc., The On-Line Encyclopedia of Integer Sequences, https://oeis.org; entries A207118--A207123, A207069, A207070, A207124--A207127, A038718, A084990, A326247; accessed October 2026.link
  14. N. P. Smart, The Algorithmic Resolution of Diophantine Equations , London Mathematical Society Student Texts, Cambridge University Press, Cambridge, 1998, https://doi.org/10.1017/CBO9781107359994.DOI
  15. R. P. Stanley, Differentiably finite power series, European J. Combin. 1 (1980), 175--188, https://doi.org/10.1016/S0195-6698(80)80051-5.DOI
  16. R. P. Stanley, Log-concave and unimodal sequences in algebra, combinatorics, and geometry, Ann. New York Acad. Sci. 576 (1989), 500--535, https://doi.org/10.1111/j.1749-6632.1989.tb16434.x.DOI
  17. R. P. Stanley, Combinatorics and Commutative Algebra , 2nd ed., Progress in Mathematics 41, Birkhäuser, Boston, MA, 1996, https://doi.org/10.1007/b139094.DOI
  18. R. P. Stanley, Enumerative Combinatorics, Volume 1 , 2nd ed., Cambridge Studies in Advanced Mathematics 49, Cambridge University Press, 2012, https://doi.org/10.1017/CBO9781139058520.DOI
  19. H. S. Wilf, D. Zeilberger, An algorithmic proof theory for hypergeometric (ordinary and ``qq'') multisum/integral identities, Invent. Math. 108 (1992), 575--633, https://doi.org/10.1007/BF02100618.DOI
  20. D. Zeilberger, A holonomic systems approach to special functions identities, J. Comput. Appl. Math. 32 (1990), 321--368, https://doi.org/10.1016/0377-0427(90)90042-X.DOI
  21. Y. Zhang, Contraction of Ore ideals with applications, in: Proceedings of the 2016 ACM International Symposium on Symbolic and Algebraic Computation (ISSAC 2016) , ACM, 2016, pp. 413--420, https://doi.org/10.1145/2930889.2930890; arXiv:1511.07922.arXivDOI

Version history

  1. v1Submitted by Yunkun SongInitial depositCurrentOct 16, 2026