The counting recurrences for the patterns 1342 and 12453 are verified in the Lean 4 proof assistant.
Abstract
We give an exact algorithm counting the permutations that avoid a fixed pattern from the following family: the direct sum of an increasing pattern and the pattern 231. The first members of the family are 1342 and 12453. For each member, the algorithm computes the number of avoiding permutations of every length up to a given bound using polynomially many arithmetic operations and polynomially many stored integers, with degrees that grow linearly in the length of the pattern. We first obtain an exact recurrence by reading a permutation from left to right and recording, at each step, the constraints that the letters read so far impose on those still unread. Its state space grows exponentially, so evaluating it directly takes exponential time. We then show that part of the state is protected: later steps carry it along unchanged and do not depend on it. Factoring the protected part out turns the recurrence into a dynamic program with polynomially many stored transfer entries, and this gives the polynomial bounds for every member of the family. For the pattern 12453, a translation symmetry sharpens the bounds to degree seven for the operations and degree four for the storage. Separately written implementations and exact Chinese-remainder certification determine the number of 12453-avoiding permutations of every length up to 150. The previously published series reached length 38. The same tables also generate uniformly random avoiders in polynomial time. We illustrate this with a heatmap of one million 12453-avoiding permutations of length 300 sampled with floating-point tables. The counting recurrences for 1342 and 12453 are verified in the Lean 4 proof assistant.
Problem
Counting permutations that avoid a fixed pattern from the family β_d = ι_d ⊕ 231 (e.g., 1342, 12453) requires polynomial-time exact enumeration, whereas direct evaluation of the natural recurrence takes exponential time due to an exponentially large state space.
Approach
A recurrence is obtained by scanning a permutation left to right, recording constraints via patience-sorting thresholds and an interval-stack representation of 231-avoidance obligations. Part of the state is shown to be 'protected' (carried unchanged), allowing it to be factored out into transfer kernels, turning the recurrence into a polynomial-size dynamic program. The counting recurrences for the patterns 1342 and 12453 are verified in the Lean 4 proof assistant, and computations are certified via Chinese-remainder reconstruction.
Results
The algorithm computes exact counts with polynomially many arithmetic operations and stored integers. For 12453 the bounds sharpen to degree seven operations and degree four storage, and exact values of |Av_n(12453)| are computed for all n up to 150 (previous series reached 38); uniform random avoiders are sampled and visualized.
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
