theorem Hex.GraphIso.Nauty.Sparse.ReturnCodes.afterChild {n : Nat} {G : SparseGraph n} {cs bs fs : List Nat} {st : State n} (h : ReturnCodes G cs bs fs st) (level tv : Nat) : ReturnCodes G cs bs fs (afterChildFirst level tv st)

First-child bookkeeping retains the actual settled comparisons.

theorem Hex.GraphIso.Nauty.Sparse.codes_advance {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) (tcLevel fuel cfuel numcells tc tv1 tv index : Nat) (first : Bool) (cs bs fs : List Nat) (cell : VSet n) (st : State n) (exit : Generic.Exit) (hl : 1 ≤ cs.length) (hr : ReturnCodes G.graph cs bs fs st) (h : CodeReady G tcLevel cs.length numcells (Generic.Policy.recover (n + 2) cs.length st)) (ht : Generic.Target State.frame cs.length tc cell (Generic.Policy.recover (n + 2) cs.length st)) (hrecord : CheapRecorded cs.length tc (Generic.Policy.recover (n + 2) cs.length st)) (hroute : RouteRecorded G.graph tcLevel cs.length tc (Generic.Policy.recover (n + 2) cs.length st)) (hpast : ∀ (smaller : VSet n), Generic.Past first tv1 (smaller.nextElem (some tv))) (hfuel : n ≤ cs.length + fuel) (hcursor : n ≤ tv + (cfuel + 1)) : have out := (Generic.advance (n + 2) (fun (first : Bool) (level numcells tc tv1 : Nat) (cursor : Option Nat) (cell : VSet n) (index : Nat) (st : State n) => Generic.sweep first (Graph.ofGraph G.graph) (n + 2) tcLevel fuel cfuel level numcells tc tv1 cursor cell index st) first cs.length numcells tc tv1 tv cell index st exit).snd.snd; ∃ (ds : List Nat), ReturnCodes G.graph cs ds fs out ∧ Grows (State.key G.graph bs st) (State.key G.graph ds out)

Resuming any completed child composes its comparison result with all remaining native siblings. The actual exit determines whether to propagate the result, consume short pruning, or restore the parent before continuing.