Stanley–Wilf conjecture

A symbolic-method presentation and Lean 4 formalization

The Stanley–Wilf conjecture is a theorem of Marcus and Tardos (2004). The following is a presentation of the established argument, with Arratia's limit-existence step organized through the symbolic method, together with a Lean 4 formalization. No mathematical priority is claimed.

Fix a pattern $\beta\in S_k$ and write $c_n=|S_n(\beta)|$, with $c_0=1$. If $k=1$, then $c_n=0$ for every $n\geq1$, and both assertions are immediate. Assume $k\geq2$.

A permutation cannot have both a nontrivial direct-sum decomposition and a nontrivial skew-sum decomposition: the former places its smallest entry before its largest, while the latter places its largest before its smallest. Thus $\beta$ is indecomposable for at least one of these two operations.

Choose such an operation. The avoidance class $\mathcal C=\operatorname{Av}(\beta)$ is closed under it. Indeed, an occurrence in a sum of two avoiders cannot lie entirely in either block, and an occurrence meeting both blocks would give a nontrivial decomposition of $\beta$ for the chosen operation.

Let $\mathcal I$ consist of the nonempty indecomposable members of $\mathcal C$. Components of an avoider again avoid $\beta$, and closure reconstructs an avoider from such components. The unique indecomposable decomposition gives the symbolic specification

$$\mathcal C=\operatorname{SEQ}(\mathcal I),\qquad C(z)=\frac{1}{1-I(z)},$$

where $C(z)=\sum_{n\geq0}c_nz^n$ and $I(z)=\sum_{n\geq1}i_nz^n$ are formal ordinary generating functions. Concatenation of component sequences of fixed sizes $m,n$ is injective: positive component sizes uniquely determine the cut at cumulative size $m$. Consequently,

$$c_{m+n}\geq c_mc_n.$$

The singleton avoids $\beta$, so repeated use of the chosen operation gives $c_n\geq1$. Fekete's lemma applied to $\log c_n$ therefore gives

$$\lim_{n\to\infty}c_n^{1/n}=\sup_{n\geq1}c_n^{1/n},$$

initially allowing $+\infty$. The Marcus–Tardos theorem supplies a finite exponential bound $c_n\leq K_\beta^n$. This proves the first assertion and bounds the displayed supremum by $K_\beta$, proving that the limit exists and is finite.

The accompanying Lean development also formalizes the extremal-matrix and matrix-counting steps underlying the exponential bound. It uses an attributed Lean 4.29 adaptation of Yaël Dillies and contributors' Apache-2.0 ForbiddenMatrix development for the Marcus–Tardos layer. The permutation bridge, Klazar counting recurrence, dyadic estimate, symbolic route, and unconditional endpoint are assembled in this repository. The explicit bound is

$$c_n\leq\bigl(2\cdot15^{2M_k}\bigr)^n,\qquad M_k=2k^4\binom{k^2}{k}.$$

The public endpoint is StanleyWilf.stanleyWilf {k : Nat} (tau : Perm k) : GrowthTarget tau. It has no supplied exponential-bound hypothesis; GrowthTarget asserts convergence to a finite nonnegative real number. Lean obtains supermultiplicativity from the first-component bijection and its convolution. The complete size-wise SEQ equivalence uses Fintype.equivOfCardEq; no executable whole-factor-list decomposition is claimed.

• Two-page proof note, v1.0.2
• Source at release commit dbcfd47
• Successful Lean 4.29.0 build, regression tests, and kernel-axiom audit. The audit of 48 declarations reports only propext, Classical.choice, and Quot.sound.
• Upstream ForbiddenMatrix at the adapted revision

References: R. Arratia, On the Stanley–Wilf conjecture for the number of permutations avoiding a given pattern, Electronic Journal of Combinatorics 6 (1999), N1; A. Marcus and G. Tardos, Excluded permutation matrices and the Stanley–Wilf conjecture, Journal of Combinatorial Theory A 107 (2004), 153–160; M. Klazar, The Füredi–Hajnal conjecture implies the Stanley–Wilf conjecture, Formal Power Series and Algebraic Combinatorics (2000), 250–255, DOI 10.1007/978-3-662-04166-6_22; P. Flajolet and R. Sedgewick, Analytic Combinatorics, Cambridge University Press, 2009. Marcus–Tardos §3 reproduces Klazar's counting reduction.