Binary initial segment (source code)

= Binary initial segment
{title2=$I_m=\{S:\sum_{i\in S}2^{i-1}<m\}$}

An <initial segment> of the <binary order on the discrete cube> contains the vertices whose integer encodings are $0,\ldots,m-1$. It is a <down-set>, so its internal edges and two-dimensional <cube faces> can be counted at their unique upper vertices by $\sum_{j<m}\operatorname{wt}(j)$ and $\sum_{j<m}\binom{\operatorname{wt}(j)}2$.