Simplicial section compression (source code)

= Simplicial section compression
{title2=$C_i^{\mathrm{simp}}$}

Split a <set family> in the <hypercube graph> according to whether coordinate $i$ is present, and delete that coordinate from the present section. Replace both sections by <initial segments> of the <simplicial order on the discrete cube> with the same respective sizes. Induction and nesting of initial-segment <closed graph neighbourhoods> show that this operation cannot enlarge the original <closed graph neighbourhood>. Repeated nontrivial compressions terminate because the sum of simplicial positions strictly decreases.