 Binary initial segment

An initial segment of the binary order on the discrete cube contains the vertices whose integer encodings are $0,\dots ,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}\mathrm{wt}(j)$ and ${\sum }_{j<m}\left(\genfrac{}{}{0ex}{}{\mathrm{wt}(j)}{2}\right)$.