theorem Hex.GraphIso.Nauty.Sparse.node_pairs {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) (tcLevel fuel level numcells : Nat) (st : State n) : 1 ≤ level → PairsEntry G tcLevel level numcells st → PairsOk G (Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel fuel level numcells st).snd

Every complete or truncated off-path call preserves the root pruning workspace. Native boundary, path and trace invariants justify each admission before the node/sibling induction proceeds through the actual filters.