A Complete Dichotomy for $L_\infty$ Permutation Removal
Viet Hung Le, Ruilin Shi, Fan Wei
math.CO
Oct 20, 2026 · v1
TL;DR
All theorems, lemmas and constructions are formalized in Lean 4 with Mathlib, with the Lean code produced by an AI (Claude) formalize-paper workflow; repository provided.
Abstract
We study the removal problem for permutation patterns under the normalized $L_\infty$ earth mover's distance. We prove a complete dichotomy. Let \[ \mathcal E =\{(12),(21),(132),(213),(231),(312)\}. \] If $σ\in\mathcal E$, then every permutation of length $n$ that is $\varepsilon$-far from being $σ$-free contains at least $\varepsilon(n-1)$ copies of $σ$; for $0<\varepsilon\le 1/16$, this is sharp up to a constant factor for all sufficiently large $n$. If $σ\in S_k\setminus\mathcal E$, then for every sufficiently large $n$ there is a permutation of length $n$ that is $1/(8k)$-far from being $σ$-free and contains exactly one copy of $σ$. Thus the usual positive-density removal conclusion fails for every nontrivial permutation pattern, but the sparse behavior is completely characterized: the minimum number of copies is linear for exactly six patterns and is one for all others. Consequently, no canonical one-sided tester that rejects only after finding a forbidden copy can have query complexity independent of the permutation length.
Problem
The paper asks whether a removal lemma holds for permutation patterns under the normalized L_infinity earth mover's distance: must a permutation that is epsilon-far from being sigma-free contain many copies of sigma?
Approach
Lemma 3.1 handles six small patterns by an explicit bijection on point sets. Each step strictly reduces the number of sigma-copies, and a bound relates that reduction to the distance moved. The triangle inequality then sums these steps. For all other patterns, line-segment constructions in the plane give far-from-free permutations that contain exactly one copy of sigma. All results were formalized in Lean 4 with Mathlib, using an AI-driven formalization workflow with statement audits.
Results
The dichotomy is complete. For the six patterns 12, 21, 132, 213, 231 and 312, the minimum number of copies is linear in n, and this is sharp up to a constant factor. For every other pattern, a permutation that is 1/(8k)-far from sigma-free can contain exactly one copy. Consequently, canonical one-sided testers cannot have query complexity independent of n. The Lean formalization contains no unproved steps.
