Terminal families for simplicial section compression (source code)

= Terminal families for simplicial section compression

A family fixed by every <simplicial section compression> is either an <initial segment> of the <simplicial order on the discrete cube> or that segment with its last vertex exchanged for the next vertex, where the exchanged vertices are complementary. Indeed, an earlier absent vertex and a later present vertex must differ in every coordinate, and cannot have another vertex between them. Complementary consecutive vertices occur only across the two central ranks in odd dimension, or at the transition from middle-rank sets containing coordinate one to those avoiding it in even dimension. Direct <closed graph neighbourhood> comparison resolves these exceptions in the proof of <Harper theorem>.