Permutation patterns

Classical, consecutive, mesh and signed patterns in permutations and in inversion and ascent sequences, pattern-avoidance counts, pattern-replacement classes, stack sorting, and king and separable permutations.

TheoremFibonacci count of parity-preserving permutations avoiding \(312\) and \(231\)#✓fully proved

For every integer \(n \ge 1\), the number of permutations \(\pi\) of \(\{0, 1, \dots, n-1\}\) such that \(\pi(i) \equiv i \pmod 2\) for every \(i\) and that avoid the patterns \(312\) and \(231\) equals the Fibonacci number \(F_n\), where \(F_1 = F_2 = 1\). Here \(\pi\) contains \(312\) if there are \(i < j < k\) with \(\pi(j) < \pi(k) < \pi(i)\), and contains \(231\) if there are \(i < j < k\) with \(\pi(k) < \pi(i) < \pi(j)\).

Equivalently, these are the parity-alternating permutations of \(\{1, \dots, n\}\) that start with an odd entry and avoid \(312\) and \(231\).

theorem fibonacci_card_parity_alternating_avoiding_312_231 (n : ℕ) (hn : 0 < n) :
    Fintype.card { π : Equiv.Perm (Fin n) //
        (∀ i, (π i).val % 2 = i.val % 2) ∧
        (∀ i j k : Fin n, i.val < j.val → j.val < k.val →
          ¬ ((π j).val < (π k).val ∧ (π k).val < (π i).val)) ∧
        (∀ i j k : Fin n, i.val < j.val → j.val < k.val →
          ¬ ((π k).val < (π i).val ∧ (π i).val < (π j).val)) } = Nat.fib n
Sources

TheoremNontrivial classes under {1234, 3412}-pattern replacement#✓fully proved

Let \(n \ge 7\) and let \(S_n\) be the group of permutations of \(\{0, 1, \dots, n - 1\}\). A move takes \(\sigma \in S_n\) with positions \(i_1 < i_2 < i_3 < i_4\) such that \(\sigma(i_1) < \sigma(i_2) < \sigma(i_3) < \sigma(i_4)\) to the permutation \(\tau\) with \(\tau(i_1) = \sigma(i_3)\), \(\tau(i_2) = \sigma(i_4)\), \(\tau(i_3) = \sigma(i_1)\), \(\tau(i_4) = \sigma(i_2)\) and \(\tau(j) = \sigma(j)\) for every other position \(j\); that is, it replaces an occurrence of the pattern \(1234\) by one of \(3412\). Call two permutations equivalent when one is reached from the other by a finite sequence of moves and reverse moves. Then the number of equivalence classes with more than one element is \((n^3 + 6n^2 - 55n + 54)/6\).

This formula was conjectured by Ma; its values form sequence A330395 in the OEIS. The proof decomposes the exceptional set into swap classes and a generic part. Kernel-checked finite certificates handle the \(S_5\) and \(S_6\) classes, reachability in \(S_7\) and the deletion boundary in \(S_8\). Point insertion then gives a recurrence, whose solution is the displayed polynomial.

public theorem card_nontrivial_1234_3412_classes :
    ∀ (n : ℕ), 7 ≤ n →
      let OneMove : Equiv.Perm (Fin n) → Equiv.Perm (Fin n) → Prop :=
        fun σ τ => ∃ i1 i2 i3 i4 : Fin n,
          i1.val < i2.val ∧ i2.val < i3.val ∧ i3.val < i4.val ∧
            σ i1 < σ i2 ∧ σ i2 < σ i3 ∧ σ i3 < σ i4 ∧
            τ i1 = σ i3 ∧ τ i2 = σ i4 ∧ τ i3 = σ i1 ∧ τ i4 = σ i2 ∧
            ∀ j : Fin n, j ≠ i1 → j ≠ i2 → j ≠ i3 → j ≠ i4 → τ j = σ j;
      Nat.card { C : Set (Equiv.Perm (Fin n)) //
          ∃ σ, C = { τ | Relation.EqvGen OneMove σ τ } ∧ 1 < Nat.card ↥C } =
        (n ^ 3 + 6 * n ^ 2 - 55 * n + 54) / 6
Sources
  • Quinn Perian, Bella Xu, and Alexander Lu Zhang, "Counting the Nontrivial Equivalence Classes of Sn Under {1234,3412}-Pattern-Replacement", Journal of Integer Sequences 23 (2020), Article 20.10.2, Theorem thm:nontrivial, lines 172-175, https://cs.uwaterloo.ca/journals/JIS/VOL23/Zhang/zhang6.tex.

TheoremPeaks of 231-avoiding permutations#✓fully proved

Let \(n \ge 1\) and \(k\) be natural numbers. A permutation \(\sigma\) of \(\{0, \dots, n-1\}\) avoids \(231\) if there are no positions \(i < j < l\) with \(\sigma(l) < \sigma(i) < \sigma(j)\), and \(\sigma\) has a peak at a position \(i\) with \(0 < i < n - 1\) if \(\sigma(i-1) < \sigma(i)\) and \(\sigma(i+1) < \sigma(i)\). The number of 231-avoiding permutations of \(\{0, \dots, n-1\}\) with exactly \(k\) peaks is \(2^{n-2k-1} \binom{n-1}{2k} \binom{2k}{k} / (k+1)\), computed in the natural numbers: the exponent \(n - 2k - 1\) is truncated at \(0\) and the division rounds down.

theorem card_permutations_avoiding_231_with_peak_count
    (n k : ℕ) (hn : 1 ≤ n) :
    (Finset.univ.filter (fun σ : Equiv.Perm (Fin n) =>
      (∀ i j l : Fin n, i < j → j < l → ¬ (σ l < σ i ∧ σ i < σ j)) ∧
      (Finset.univ.filter (fun i : Fin n =>
        ∃ iPrev iNext : Fin n,
          iPrev.val + 1 = i.val ∧ i.val + 1 = iNext.val ∧
          σ iPrev < σ i ∧ σ iNext < σ i)).card = k)).card =
      2 ^ (n - 2 * k - 1) * Nat.choose (n - 1) (2 * k) * Nat.choose (2 * k) k /
        (k + 1)
Sources
3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.