theorem Hex.GraphIso.Nauty.Sparse.codes_sweep {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) (tcLevel fuel : Nat) (hd : ∀ (cs bs fs : List Nat) (numcells : Nat) (st : State n), CodeEntry G tcLevel (cs.length + 1) numcells st → n ≤ cs.length + fuel → Comparison G.graph cs bs fs st → have out := (Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (cs.length + 1) numcells st).snd; ∃ (bs' : List Nat), ReturnCodes G.graph cs bs' fs out ∧ Grows (State.key G.graph bs st) (State.key G.graph bs' out)) (cfuel : Nat) (first : Bool) (cs bs fs : List Nat) (numcells tc tv1 index : Nat) (cursor : Option Nat) (cell : VSet n) (st : State n) (hl : 1 ≤ cs.length) (h : CodeReady G tcLevel cs.length numcells st) (ht : Generic.Target State.frame cs.length tc cell st) (hv : ∀ (v : Nat), cursor = some v → cell.mem v = true) (hpast : Generic.Past first tv1 cursor) (hrecord : CheapRecorded cs.length tc st) (hroute : RouteRecorded G.graph tcLevel cs.length tc st) (hfuel : n ≤ cs.length + fuel) (hcursor : Generic.CursorFuel n cfuel cursor) (hc : Comparison G.graph cs bs fs st) (hphase : st.compCanon ≤ 0 ∨ first = false ∧ cursor.isSome = true) : have out := (Generic.sweep first (Graph.ofGraph G.graph) (n + 2) tcLevel fuel cfuel cs.length numcells tc tv1 cursor cell index st).snd.snd; ∃ (bs' : List Nat), ReturnCodes G.graph cs bs' fs out ∧ Grows (State.key G.graph bs st) (State.key G.graph bs' out)

Later native siblings compose incumbent growth and return settled comparisons on an extension of the parent's code path. The proof follows the actual short/long filters, nonlocal returns, and partition recovery.