Shuffle automata and the growth of 1324-avoiding permutations
Robert Brignall
math.CO
Oct 1, 2026 · v1
TL;DR
Positivity of 384 automaton state weights and 1536 local inequalities behind Proposition 5.3 are formally verified in Lean 4 with Mathlib; code on GitHub.
Abstract
We show that $\text{gr}(\text{Av}(1324))\leq 13.167248$. This is achieved by combining the approach of Bevan, Brignall, Elvey Price and Pantone using the `domino', with ideas from earlier upper bounds by Bóna using pairs of decorated words with additional restrictions. More specifically, we replace the arbitrary interleavings of Bevan et. al. with interleavings more like those of Bóna. Our method uses shuffle automata to handle the interleavings, and this method has the potential to provide better upper bounds than the one established here. To estimate how many shuffles are possible, we use two key statistics on dominoes: the number of internal points (that is, points that are neither left-to-right minima not right-to-left maxima), and the number of runs of internal points.
Problem
The exponential growth rate of the 1324-avoiding permutation class is unknown. The best published rigorous upper bound is 13.5, well above the numerical estimate of about 11.6.
Approach
The domino-based encoding of Bevan, Brignall, Elvey Price and Pantone is combined with Bóna-style restricted interleavings. A 1324-avoider is encoded as a domino plus a shuffle of two words that avoids a forbidden factor. These shuffles are counted using shuffle automata with k-letter lookahead, together with a refined domino enumeration that tracks internal points and runs of internal points. The weight-positivity and local inequalities certifying the automaton bound (Proposition 5.3) are checked in Lean 4 using Mathlib.
Results
The method gives gr(Av(1324)) ≤ 13.167248. An unverified computation suggests that a 5-lookahead automaton would give about 13.1498.
