theorem Hex.GraphIso.Nauty.Sparse.canon_advance {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) {fuel cfuel : Nat} {next : Generic.SweepFn (State n) n} (hnext : (canonContract G).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) (hf : FrameOut G level level st out) (hc : CanonOut level st out) : CanonOut level st (Generic.advance (n + 2) next first level numcells tc tv1 tv cell index out exit).snd.snd

A native child return retains provenance when passed outward or composed with the recovered parent's remaining siblings.

theorem Hex.GraphIso.Nauty.Sparse.canon_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 : (canonContract G).nodeValid fuel descend) (hnext : (canonContract 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) : CanonOut level st (Generic.sweepStep (n + 2) descend next first level numcells tc tv1 tv cell index st).snd.snd

The actual individualized child and following sweep compose their canonical provenance, including first-child bookkeeping and skipped orbits.