Solution (source code)

= Solution

Write $N[A]$ for the <closed graph neighbourhood> of $A$. Since $|N[A]|=|A|+|\partial_vA|$, 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 $t$-vertex subsets of $[k]^n$, the first $t$ vertices in the <simplicial order on a grid> minimize this quantity.

We prove the theorem by <mathematical induction> on $n$, using the allowed two-dimensional case. Fix a coordinate $i$ and write $A_j\subseteq[k]^{n-1}$ for the section in which that coordinate equals $j$. Replace each $A_j$ by the equally large initial simplicial segment $B_j$. By induction, $|N[B_j]|\leq|N[A_j]|$. The <section formula for a grid neighbourhood> gives
$$
N[A]_j=N[A_j]\cup A_{j-1}\cup A_{j+1},
\qquad A_0=A_{k+1}=\varnothing.
$$
For the compressed family, $N[B_j],B_{j-1},B_{j+1}$ 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 $j$ 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 $[k]^2$ 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 $Q_2$ in the <Gray code> order
$$
00,\ 01,\ 11,\ 10.
$$
The three consecutive edges form a copy of the four-vertex path $P_4$. Pairing the $2n$ binary coordinates and applying this identification in each pair realizes
$$
[4]^n=P_4^n
$$
as a <spanning subgraph> of the <hypercube graph> $Q_{2n}$. For any fixed vertex set, adding graph edges can only enlarge its <external vertex boundary>. Hence a $t$-set in $Q_{2n}$ has boundary at least that of the same $t$ vertices in $[4]^n$, which by hypothesis is at least $s$. Therefore
$$
\boxed{|\partial_{Q_{2n}}A|\geq s\quad\text{whenever }|A|=t.}
$$