theorem Hex.GraphIso.Nauty.Sparse.store_advance {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) {fuel cfuel : Nat} {next : Generic.SweepFn (State n) n} (hnext : (storeContract G).sweepValid fuel cfuel next) (first : Bool) (level numcells tc tv1 tv index : Nat) (cell : VSet n) (st out : State n) (exit : Generic.Exit) (hl : 1 ≤ level) (h : Ready G level numcells st) (ht : Generic.Target State.frame level tc cell st) (hx : FrameOut G level level st out) (hs : Store G.graph out) : Store G.graph (Generic.advance (n + 2) next first level numcells tc tv1 tv cell index out exit).snd.snd

Once a child returns a valid store, every recovery, filter and surviving sibling retains it. The child's frame justifies the recovered parent.

theorem Hex.GraphIso.Nauty.Sparse.store_sweep {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) {fuel cfuel : Nat} {descend : Generic.NodeFn (State n)} {next : Generic.SweepFn (State n) n} (hd : (storeContract G).nodeValid fuel descend) (hnext : (storeContract G).sweepValid fuel cfuel next) (first : Bool) (level numcells tc tv1 tv index : Nat) (cell : VSet n) (st : State n) (hl : 1 ≤ level) (h : Ready G level numcells st) (ht : Generic.Target State.frame level tc cell st) (hv : cell.mem tv = true) (hs : Store G.graph st) : Store G.graph (Generic.sweepStep (n + 2) descend next first level numcells tc tv1 tv cell index st).snd.snd

Each actual child and later sibling preserves the installed canonical store, including orbit-skipped vertices and returns past this sweep.