Binary order on the discrete cube

Identify a vertex $(x_1,\dots ,x_n)$ with the integer ${\sum }_{i=1}^n{2}^{i-1}{x}_i$. Binary order is increasing order of these integers. Its initial segment of size $a$ has $F(a)={\sum }_{j=0}^{a-1}{s}_2(j)$ induced edges, where $s_2(j)$ is the Hamming weight of the binary expansion of $j$.

For $F(a)={\sum }_{j=0}^{a-1}{s}_2(j)$ and nonnegative integers $a,b$, the displayed inequality follows by induction from $F(2r)=2F(r)+r$ and $F(2r+1)=F(r)+F(r+1)+r$. Splitting a vertex set of a hypercube graph into its two coordinate sections then proves the edge-isoperimetric theorem for binary initial segments.