theorem Hex.GraphIso.Nauty.Sparse.node_codes {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) (tcLevel fuel : Nat) (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)

Every sufficiently bounded native off-path call returns settled code comparisons and never decreases the incumbent. Its proof follows the executed mutual recursion, including skipped siblings and nonlocal exits.