A uniform double-factorial construction for consecutive-pattern packings
Zoltán Nagy
math.CO
Oct 26, 2026 · v1
TL;DR
The main counting theorem, that the packings of the constructed pattern number (2j-1)!!, is formalized in Lean 4/Mathlib in an accompanying archive.
Abstract
For every overlap $m\geq 3$ and every pattern length $K\geq 2m+1$, we construct an explicit permutation $p\in\mathfrak{S}_K$ such that the number of permutations containing $j$ prescribed occurrences of $p$, with successive starts separated by $K-m$, is $(2j-1)!!$ for every $j\geq 1$. Additional occurrences are permitted. We prove that the corresponding occurrence poset is the ordinal sum of a chain on $m+j(K-m-2)$ elements and a comb on $2j$ elements. An insertion bijection counts the linear extensions of the comb. This gives the uniform representatives requested in the double-factorial part of Question 6 in Section 7 of Blitvić, Kammoun and Steingrímsson, arXiv:2610.29846v1. A Lean 4 formalization and its recorded verification data accompany the paper.
Problem
Blitvić, Kammoun and Steingrímsson asked for uniform pattern representatives whose consecutive-pattern packing counts are double factorials. The question covers every overlap m≥3 and pattern length K≥2m+1.
Approach
An explicit permutation p in S_K is constructed for each m and K. The associated occurrence poset is shown to be the ordinal sum of a chain and a comb on 2j elements. An insertion bijection counts the linear extensions of the comb. The main theorem is formalized in Lean 4 with Mathlib, with the toolchain and Mathlib revision pinned.
Results
For every j≥1, the number of permutations containing j prescribed occurrences of p, with starts separated by K−m, is (2j−1)!!. This answers the double-factorial part of the question. Recorded verification data report successful builds, and the main theorem depends only on the standard axioms propext, Classical.choice and Quot.sound.
