Write for the closed graph neighbourhood of . Since , minimizing the external vertex boundary at fixed cardinality is equivalent to minimizing the closed neighbourhood. The vertex-isoperimetric inequality in a grid says that, among all -vertex subsets of , the first vertices in the simplicial order on a grid minimize this quantity.
We prove the theorem by mathematical induction on , using the allowed two-dimensional case. Fix a coordinate and write for the section in which that coordinate equals . Replace each by the equally large initial simplicial segment . By induction, . The section formula for a grid neighbourhood gives
For the compressed family, are nested initial segments, so the size of their union is the maximum of their sizes. That maximum is no larger than the size of the corresponding uncompressed union. Summing over proves that coordinate compression in a product of paths does not enlarge the boundary.
Apply these compressions in every coordinate, choosing among boundary-minimizing outcomes one with least coordinate-sum weight. If the result were not an initial simplicial segment, it would contain a later vertex while omitting an earlier one. After cancelling coordinates in which they agree, this gives an inversion in a two-coordinate face. Replacing the occupied portion of that face by the equal-size initial segment in does not increase its neighbourhood by the assumed two-dimensional theorem, while it strictly lowers the weight. This contradiction is the local-to-global lemma for simplicial grid order, and completes the induction.
For the second assertion, list the vertices of in the Gray code order
The three consecutive edges form a copy of the four-vertex path . Pairing the binary coordinates and applying this identification in each pair realizes
as a spanning subgraph of the hypercube graph . For any fixed vertex set, adding graph edges can only enlarge its external vertex boundary. Hence a -set in has boundary at least that of the same vertices in , which by hypothesis is at least . Therefore
Let be the section of with one coordinate fixed at , and put . The corresponding section of its closed graph neighbourhood is
After coordinate compression, the three sets on the right are nested initial simplicial segments. Their union therefore has the largest of their three cardinalities, which is no larger than the original union.