refine preserves reachability from an ancestor node's state: it
permutes labels within cells of its own finer partition, and the
ancestor's boundaries persist, so cell-content equivalence coarsens and
composes. The node-relative form of refine_cellsReach.
breakout preserves reachability from an ancestor node's state:
individualization permutes within one cell of the current partition,
which refines the ancestor's. The node-relative form of
breakout_cellsReach.
A scatter joining two labellings reachable from a node stabilizes
the node's cells: on every cell the scatter carries the first
labelling's contents to the second's, and both agree with the node's
own contents up to permutation, so the node labelling mapped through
the scatter is cell-wise a permutation of itself. This is how an
admitted generator (the scatter of a leaf labelling over firstlab or
canonlab) satisfies the CellStab hypothesis of
childKey_of_orbPruned at every node above both leaves.
A checked automorphism stabilizing a node's cells still stabilizes
them after refinement: refine depends on the labelling only through
cell contents (refine_perm) and commutes with the automorphism's
renaming (refine_map), and the two transports meet at the refined
state. The descent-propagation clause of the stabilization
invariant.
A cell-stabilizing map fixing the individualized vertex still
stabilizes the cells after individualization: the singleton is fixed
outright, the remainder cell's stability follows from the target
cell's by head cancellation, and every other cell is untouched. The
individualization arm of descent propagation, paired with
cellStab_refine.