The literal and kernel recurrences for counting 1342- and 12453-avoiding permutations are formally verified in Lean 4.
Abstract
We give an algorithm counting the permutations that avoid a fixed pattern of the following form: the direct sum of an increasing pattern and 231. The first members of the family are 1342 and 12453. For each member the algorithm uses polynomially many operations and stored integers, with degrees that grow linearly in the length of the pattern. It comes from a recurrence that reads a permutation from left to right and records the constraints that the letters read so far impose on those still unread. This recurrence has exponentially many states, but part of each state is protected: later steps carry it along unchanged and do not depend on it, and factoring the protected part out leaves a dynamic program of polynomial size. For 12453 a translation symmetry sharpens the bounds to degree seven for the operations and degree four for the storage. We also compute the number of 12453-avoiding permutations of every length up to 150. The previously published series, due to Biers-Ariel (2019), reached length 38. We also give a sampler of uniformly random avoiders. A floating-point implementation of it, proved to be within total variation distance $3.5\cdot10^{-5}$ of uniform for ideal random bits, draws the one million 12453-avoiding permutations of length 300 shown in a heatmap. The literal and kernel recurrences for 1342 and 12453 are verified in the Lean 4 proof assistant.
Problem
Counting permutations that avoid a pattern of the form ι_d ⊕ 231 (e.g. 1342, 12453) had no known polynomial-time algorithm for the whole family. The published series for 12453 reached only length 38.
Approach
A left-to-right recurrence records the constraints that a scanned prefix places on unread letters, using patience-sorting thresholds and a stack of 231-avoidance intervals. The protected tail of each state is carried along unchanged and is factored out, which turns the exponential-state recurrence into transfer kernels and a polynomial-size dynamic program. For 12453 a translation symmetry reduces the complexity further. Computations use multi-modular arithmetic with Chinese-remainder reconstruction, and the literal and kernel recurrences for 1342 and 12453 are verified in Lean 4.
Results
The algorithm uses polynomially many operations and stored integers, with degrees growing linearly in the pattern length; for 12453 the bounds are O(N^7) operations and O(N^4) storage. Exact counts of 12453-avoiders are computed up to length 150. A uniform sampler, proved within total variation distance 3.5e-5 of uniform for ideal random bits, draws one million avoiders of length 300.
Figure 2. Left: position–value heatmap of one million elements of \operatorname{Av}_{300}(12453) drawn by the floating-point implementation of the uniform sampler of section 8.1 . The cell at position i (left to right) and value v (bottom to top) is shaded by the square root of the number of samples with \pi_{i}=v , from white (no sample) to black (the largest cell count, 70\,204 ). Right: one of
