theorem Hex.GraphIso.Nauty.Sparse.traceFrame_advance {n k : Nat} (G : Sparse.Colored n k) {base cells : Nat} {root : State n} (hp : Ready G base cells root) (hn : 0 < n) (hb : 1 ≤ base) {fuel cfuel : Nat} {next : Generic.SweepFn (State n) n} (hnext : (traceFrameContract G base root).sweepValid fuel cfuel next) (first : Bool) (level numcells tc tv1 tv index : Nat) (cell : VSet n) (st out : State n) (exit : Exit) (hl : 1 ≤ level) (hi : Ready G level numcells st) (ht : Generic.Target State.frame level tc cell st) (he : FrameOut G level level st out) (hlevel : base ≤ level) (h : TraceFrame G base root out) : TraceFrame G base root (Generic.advance (n + 2) next first level numcells tc tv1 tv cell index out exit).snd.snd

A returned child's frozen frame survives every native continuation: both target filters, parent recovery, and a nonlocal return past the caller.

theorem Hex.GraphIso.Nauty.Sparse.traceFrame_sweep {n k : Nat} (G : Sparse.Colored n k) {base cells : Nat} {root : State n} (hp : Ready G base cells root) (hn : 0 < n) (hb : 1 ≤ base) {fuel cfuel : Nat} {descend : Generic.NodeFn (State n)} {next : Generic.SweepFn (State n) n} (hd : (traceFrameContract G base root).nodeValid fuel descend) (hnext : (traceFrameContract G base root).sweepValid fuel cfuel next) (first : Bool) (level numcells tc tv1 tv index : Nat) (cell : VSet n) (st : State n) (hl : 1 ≤ level) (hi : Ready G level numcells st) (ht : Generic.Target State.frame level tc cell st) (hv : cell.mem tv = true) (hlevel : base ≤ level) (h : TraceFrame G base root st) : TraceFrame G base root (Generic.sweepStep (n + 2) descend next first level numcells tc tv1 tv cell index st).snd.snd

The literal child call and the remaining sibling sweep preserve the suspended first-path cells and all trace generators stabilizing them.