 Edge-isoperimetric theorem for binary initial segments

Among subsets of the $n$-dimensional hypercube graph with $a$ vertices, initial segments of the binary order on the discrete cube minimize the edge boundary. Its exact minimum is $na-2{\sum }_{j=0}^{a-1}{s}_2(j)$. This strengthens the entropy lower bound on the same boundary.