HEXAGONbeta

An Intrinsic Formula for the Ray–West Correction Term

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

Contributed by Donald Poindexter ↗

Version 1 / Oct 15, 2026 / CC BY 4.0

Abstract

For a nonempty permutation β\beta of length mm, let g2(β)g_2(\beta) denote the number of distinct permutations of length m+2m+2 containing β\beta. Ray and West showed that $$ g_2(\beta)=\frac{m^4+2m^3+m^2+4m+4-2j(\beta)}{2}, \qquad 0\le j(\beta)\le m-1, $$ but their correction term was not expressed as a statistic of β\beta. This was posed explicitly as Problem 3.7 by Vatter. We give a polynomial-time formula defined entirely from β\beta: j(β)=L(β)+R(β)j(\beta)=L(\beta)+R(\beta), where LL counts licensed gaps and RR counts anchor-free two-deletion classes containing a collision whose canonical alignment support is a permutation interval. We also derive the Ray–West bound intrinsically and characterize its upper-bound equality cases as precisely the layered or reverse-layered permutations. The proof is combinatorial. Exact computation is used only for independent corroboration; the accompanying proof-and-replay archive contains the full proof supplement and bounded verification. This preliminary technical report was first deposited on Zenodo on August 9, 2026: https://doi.org/10.5281/zenodo.21857882.

Provenance statement

This work was developed within the conjecture-prover and autoformalization project led by Donald D. Poindexter, Jr. for Stanford Lean Club. OpenAI GPT-5.6 Sol Ultra was used extensively for conjecture generation, exact computation, proof development, adversarial repair, and preparation of the initial proof artifacts. Codex assisted with independent reconstruction, simplification, and preparation of the preliminary technical report. The human author directed the project, selected the claims for release, and assumes responsibility for the manuscript. The manuscript and its integral companion proof supplement together constitute the claimed combinatorial proof. Exact Python computations provide independent corroboration on bounded ranges and are not used as proof steps. No complete machine-checked formalization is included or claimed. Automated audits and exact replay are not substitutes for external peer review. This submission cross-posts preliminary technical report version 0.1, first publicly deposited on August 9, 2026, with its proof-and-replay archive at https://doi.org/10.5281/zenodo.21857882.

Tools used

OpenAI
ChatGPTVersion 5.6 Sol Ultra
OpenAI
Codex

References

  1. Nigel Ray and Julian West. Posets of matrices, and permutations with forbidden subsequences. Annals of Combinatorics , 7(1):55--88, 2003.
  2. Vincent Vatter. Problems and conjectures. In Permutation Patterns , volume 376 of London Mathematical Society Lecture Note Series , pages 339--345. Cambridge University Press, 2010.
  3. Vincent Vatter. An assortment of problems in permutation patterns: Unimodality, equivalence, derangements, and sorting, 2026. arXiv:2602.16355.arXiv

Version history

  1. v1Submitted by Donald PoindexterInitial depositCurrentOct 15, 2026