A uniform double-factorial construction for consecutive-pattern packings

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.