An asymptotically optimal lower bound on the OBDD size of the middle bit of multiplication for the pairwise ascending variable order

We prove that each OBDD (ordered binary decision diagram) for the middle bit of n-bit integer multiplication for one of the variable orders which so far achieve the smallest OBDD sizes with respect to asymptotic order of growth, namely the pairwise ascending order x₀,y₀,…,x_n−1,y_n−1, requires a size of Ω(2^(6/5)n). This is asymptotically optimal due to a bound of the same order by Amano and Maruoka (2007) 1].